×

A clausal resolution method for CTL branching-time temporal logic. (English) Zbl 1054.68666

Summary: 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 also outline possible implementation of the approach by adapting techniques developed for linear-time temporal resolution.

MSC:

68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bolotov, A. and Fisher, M. A resolution method for CTL branching time temporal logic. IV International Workshop on Temporal Representation and Reasoning (TIME’97). pp.20–27. Los Alamitos: IEEE.
[2] Clarke, E. M. and Emerson, E. A. Design and synthesis of synchronisation skeletons using branching time temporal logic. Proceedings of the Workshop on Logic of Programs. Lecture Notes in Computer Science, Vol. 131, pp.52–71.
[3] DOI: 10.1145/5397.5399 · Zbl 0591.68027 · doi:10.1145/5397.5399
[4] Dixon D., Strategies for temporal resolution (1995)
[5] Dixon, C. Search strategies for resolution in temporal logics. Proceedings of the Thirteenth International Conference on Automated Deduction. pp.672–687. July 30–August 3
[6] Emerson E. A., Handbook of Theoretical Computer Science pp 996– (1990)
[7] Emerson E. A., Logics for Concurrency: Structures Versus Automata, Lecture Notes in Computer Science 1043 pp 41– (1996)
[8] Emerson, E. A. and Halpern, J. Y. Decision procedures and expressiveness in the temporal logic of branching time. Proceedings of the Fourteenth ACM Symposium on the Theory of Computing (STOC). May5–7, San Francisco. pp.169–180. · Zbl 0559.68051
[9] DOI: 10.1145/4904.4999 · Zbl 0629.68020 · doi:10.1145/4904.4999
[10] DOI: 10.1016/0167-6423(87)90036-0 · Zbl 0615.68019 · doi:10.1016/0167-6423(87)90036-0
[11] DOI: 10.1016/S0019-9958(84)80047-9 · Zbl 0593.03007 · doi:10.1016/S0019-9958(84)80047-9
[12] Fisher, M. A resolution method for temporal logic. Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI). August, Sydney, Australia. pp.99–104. · Zbl 0745.68091
[13] DOI: 10.1093/logcom/7.4.429 · Zbl 0893.03003 · doi:10.1093/logcom/7.4.429
[14] Genesereth M. R., Logical Foundations of Artificial Intelligence (1988) · Zbl 0645.68104
[15] Pnueli, A. The temporal logic of programs. Proceedings of the Eighteenth Symposium on the Foundations of Computer Science. October 31–November 2, Providence, USA. pp.46–57.
[16] Prior A., Past, Present and Future (1967) · Zbl 0169.29802
[17] Rao, A. S. and Georgeff, M. P. modeling rational agents within a BDI-architecture. International Conference on Principles of Knowledge Representation and Reasoning (KR). April22–25, Cambridge, Massachusetts. pp.473–484.
[18] Vardi M. Y., Logics for Concurrency: Structures Versus Automata, Lecture Notes in Computer Science 1043 pp 238– (1996)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.