Decision procedures and expressiveness in the temporal logic of branching time. (English) Zbl 0559.68051

E. A. Emerson and E. M. Clarke [Sci. Comput. Program. 2, 241- 266 (1982; Zbl 0514.68032)] have proposed the computation tree logic (CTL), which is the unified branching time logic (UB) of M. Ben- Ari, Z. Manna and A. Pnueli [8th ACM Symp. on Principles of Programming Languages, 164-176 (1981)] augmented with an until operator. This paper gives an exponential decision procedure for deciding satisfiability in CTL with the small model theorem and its complete axiomatization. The relative expressive power of temporal logics obtained by extending or restricting the syntax of UB and CTL is also studied.
Reviewer: H.Nishimura


68Q65 Abstract data types; algebraic specification
03B45 Modal logic (including the logic of norms)
03B25 Decidability of theories and sets of sentences
03D15 Complexity of computation (including implicit computational complexity)


Zbl 0514.68032
Full Text: DOI


[1] Abrahamson, K., Decidability and Expressiveness of Logics of Processes, (PhD thesis (1980), Univ. of Washington)
[2] M. Ben-Ari, personal communication.; M. Ben-Ari, personal communication.
[3] Ben-Ari, M.; Halpern, J. Y.; Pnueli, A., Deterministic propositional dynamic logic: Finite models, complexity, and completeness, J. Comput. System Sci., 25, No. 3, 402-417 (1982) · Zbl 0512.03013
[4] Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, (Proc. Ann. ACM Sympos. Principles of Programming Languages (1981)), 164-176
[5] Emerson, E. A.; Clarke, E. M., Using branching time logic to synthesize synchronization skeletons, Sci. Comput. Programming, 2, 241-266 (1982) · Zbl 0514.68032
[6] Emerson, E. A.; Clarke, E. M., Characterizing correctness properties of parallel programs as fixpoints, (Int. Colloq. Automata Lang. and Programming (1980)), 169-181 · Zbl 0456.68016
[7] Emerson, E. A.; Halpern, J. Y., “Sometimes” and “Not Never” revisited: On branching versus linear time, (Proc. Ann. ACM Sympos. Principles of Programming Languages (1983)), 127-140
[8] Emerson, E. A., Theor. Comput. Science, 26, Nos 1, 2, 121-130 (1983) · Zbl 0559.68050
[9] Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, No. 2, 194-211 (1979) · Zbl 0408.03014
[10] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (Proc. Annual ACM Sympos. Principles of Programming Languages (1980)), 163-173
[11] Kamp, H. W., Tense Logic and the Theory of Linear Order, (PhD thesis (1968), UCLA)
[12] Kozen, D.; Parikh, R., An elementary proof of the completeness of PDL, Theor. Comput. Science, 14, No. 1, 113-118 (1981) · Zbl 0451.03006
[13] Lamport, L., “Sometimes” is sometimes “not never,”, (Proc. Annual ACM Sympos. Principles of Programming Languages (1980)), 174-183
[14] Manna, Z.; Pnueli, A., The modal logic of programs, (Int. Colloq. Automata Lang. and Programming (1979)), 385-410 · Zbl 0404.68011
[15] Pnueli, A., The temporal logic of programs, (Proc. IEEE Annual Sympos. Forind. Comput. Sci (1977)), 46-57
[16] Pratt, V. R., Applications of Modal Logic to Programming, MIT LCS TM-116 (1978) · Zbl 1283.03066
[17] Pratt, V. R., Models of program logics, (Proc. IEEE Annual Sympos. Found. Comput. Sci. (1979)), 15-122
[18] Smullyan, R. M., First-Order Logic (1967), Springer-Verlag: Springer-Verlag Berlin · Zbl 0172.28901
[19] Streett, R. S., Propositional Dynamic Logic of Looping and Converse, (PhD thesis (1981), MIT) · Zbl 0515.68062
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.