Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
- 1 June 1993
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 3 (3) , 249-268
- https://doi.org/10.1093/logcom/3.3.249
Abstract
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
This publication has 0 references indexed in Scilit: