© 1993 by Oxford University Press
Original Articles |
Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
Dipartimento di Matematica Pura ed Applicata Via Belzoni 7, 1-35131 Padova, Italy
Departamento de Matematica, IST Av Rovisco Pais, P-1096 Lisboa, Portugal
The framework underlying CTL* is extended in order to include past operators. Recent developments in areas related to concurrent program specification and verification, as well as database and information systems specification, justify the interest of such extension. The semantics for the language so obtained is defined according to the ockhamist approach to non-deterministic time. The differences between this semantics and the original semantics for CTL* are analysed. A sound axiomatization is proposed for such logic and its completeness is proved.
Keywords: Computational logic; branching-time logic; completeness.