A resolution method for CTL branching-time temporal logic
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We extend our clausal resolution method for linear temporal logics to a branching-time framework. The branching-time temporal logics considered are computation tree logic (CTL), often regarded as the simplest useful logic of this class, and extended CTL (ECTL), which is CTL extended with fairness operators. The key elements of the resolution method, namely the normal form, the concept of step resolution and a novel temporal resolution rule, are introduced and justified with respect to both these logics. A completeness argument is provided, together with an example of the use of the temporal resolution method. Finally, we consider future work, in particular extension of the method yet further, to CTL*, and implementation of the approach by utilising techniques developed for linear-time temporal resolution.Keywords
This publication has 9 references indexed in Scilit:
- Design and synthesis of synchronization skeletons using branching time temporal logicPublished by Springer Nature ,2005
- A resolution-based proof method for temporal logics of knowledge and beliefPublished by Springer Nature ,1996
- Search strategies for resolution in temporal logicsPublished by Springer Nature ,1996
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986
- Deciding full branching time logicInformation and Control, 1984
- Decision procedures and expressiveness in the temporal logic of branching timePublished by Association for Computing Machinery (ACM) ,1982
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977
- Past, Present and FuturePublished by Oxford University Press (OUP) ,1967