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, ()
[2] M. {\scBen-Ari}, personal communication.
[3] Ben-Ari, M.; Halpern, J.Y.; Pnueli, A.; 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), revised version · Zbl 0512.03013
[4] Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, (), 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, (), 169-181
[7] Emerson, E.A.; Halpern, J.Y., “sometimes“ and “not never” revisited: on branching versus linear time, (), 127-140
[8] Emerson, E.A.; Emerson, E.A., Alternative semantics for temporal logics, (), 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, (), 163-173
[11] Kamp, H.W., Tense logic and the theory of linear order, ()
[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,”, (), 174-183
[14] Manna, Z.; Pnueli, A., The modal logic of programs, (), 385-410
[15] Pnueli, A., The temporal logic of programs, (), 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, (), 15-122
[18] Smullyan, R.M., First-order logic, (1967), Springer-Verlag Berlin · Zbl 0172.28901
[19] Streett, R.S., Propositional dynamic logic of looping and converse, () · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.