A clausal resolution method for CTL branching-time temporal logic
- 1 January 1999
- journal article
- research article
- Published by Taylor & Francis in Journal of Experimental & Theoretical Artificial Intelligence
- Vol. 11 (1) , 77-93
- https://doi.org/10.1080/095281399146625
Abstract
In this paper we extend our clausal resolution method for linear time temporal logics to a branching-time framework. Thus, we propose an efficient deductive method useful in a variety of applications requiring an expressive branching-time temporal logic in AI. The branching-time temporal logic considered is Computation Tree Logic (CTL), often regarded as the simplest useful logic of this class. 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 this logic. A completeness argument is provided, together with some examples of the use of the temporal resolution method. Finally, we consider future work, in particular the extension of the method yet further, to Extended CTL (ECTL), which is CTL extended with fairness operators, and CTL*, the most powerful logic of this class. We will also outline possible implementation of the approach by adapting techniques developed for linear-time temporal resolution.Keywords
This publication has 13 references indexed in Scilit:
- A resolution method for CTL branching-time temporal logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Normal Form for Temporal Logics and its Applications in Theorem-Proving and ExecutionJournal of Logic and Computation, 1997
- Search strategies for resolution in temporal logicsPublished by Springer Nature ,1996
- Automated temporal reasoning about reactive systemsPublished by Springer Nature ,1996
- Modalities for model checking: branching time logic strikes backScience of Computer Programming, 1987
- 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