Decision procedures and expressiveness in the temporal logic of branching time

ABSTRACT

In this paper we consider the Computation Tree Logic (CTL) proposed in [CE] which extends the Unified Branching Time Logic (UB) of [BMP] by adding an until operator. We establish that CTL has the small property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from a small -&-ldquo;pseudo-model-&-rdquo; resulting from the Fischer Ladner quotient construction. We then give an exponential time algorithm for deciding satisfiability in CTL, and extend the axiomatization of UB given in [BMP] to a complete axiomatization for CTL. Lastly, we study the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL.

REFERENCES

• 1: M. Ben-Ari, personal communication.
• 2: Mordechai Ben-Ari , Joseph Y. Halpern , Amir Pnueli, Finite Models for Deterministic Propositional Dynamic Logic, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.249-263, July 13-17, 1981
• 3: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 4: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 5: E. Allen Emerson , Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.169-181, July 14-18, 1980
• 6: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 7: H. W. Kamp, Tense logic and the theory of linear order, Ph.D. thesis, UCLA, 1968.
• 8: D. Kozen and R. Parikh, An elementary proof of the completeness of PDL, Theoretical Computer Science, 14:1, pp. 113-118, 1981.
• 9: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 10: Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
• 11: A. Pnueli, The temporal logic of programs, FOCS 1977, pp. 46-57.
• 12: V. R. Pratt, Applications of modal logic to programming, MIT/LCS/TM-116, 1978.
• 13: V. R. Pratt, Models of program logics, FOCS 1979, pp. 115-122.
• 14: R. S. Streett, Propositional dynamic logic of looping and converse, Ph.D. thesis, M.I.T., 1981.