Abstract
In this paper we study the expressive power of the full branching time logic CTL* (of Clarke, Emerson, Halpern and Sistla), by comparing it with fragments of monadic second-order logic over the binary tree. We show that over binary tree models the system CTL* has the same expressive power as monadic second-order logic in which set quantification is restricted to infinite paths (in particular, the full strength of first-order logic is captured here by CTL*). This generalizes Kamp's theorem on the equivalence between propositional linear time logic and first-order logic over the ordering of the natural numbers. For the proof an extension of CTL* by past operators is introduced. The transition from monadic formulas to CTL* rests on a model-theoretic decomposition lemma for trees that is justified by an application of the Ehrenfeucht-Fraissé game. The paper concludes by discussing variants of the main result, dealing for example with trees of higher branching index and the extended branching time logic ECTL*.
The first author was supported by the Deutsche Forschungsgemeinschaft.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Browne, M.C., An improved algorithm for the automatic verification of finite state systems using temporal logic, 1st IEEE Sympos. Logic in Computer Science, 1986, pp. 260–266.
Clarke, E.M., Emerson, E.A., Using branching time temporal logic to synthesize synchronization skeletons, Science of Computer Pogramming 2 (1982), 241–266.
Clarke, E.M., Emerson, E.A., Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach, Proc. 10th Ann. ACM Sympos. on Principles of Programming Languages, 1983, pp. 117–126.
Emerson, E.A., Halpern, J.Y., 'sometimes’ and ‘notnever’ revisited: On branching versus linear time temporal logic, Journal of the ACM 33 (1986), 151–178.
Emerson, E.A., Sistla, A.P., Deciding (full) branching time logic, Information and Control 61 (1984), 175–201.
Gabbay, D., Pnueli, A., Shelah, A., Stavi, J., The temporal analysis of fairness, Proc. 7th Ann. ACM Sympos. on Principles of Programming Languages, 1980, pp. 163–173.
Gurevich, Y., Shelah, S., Rabin's uniformization problem, Journal of Symbolic Logic 48 (1983), 1105–1119.
Hafer, Th., On the expressive completeness of CTL*, Schriften zur Informatik und angewandten Mathematik 123, RWTH Aachen, 1986.
Heuter, U., Baumsprachen in der Logik erster Stufe: Eine Charakterisierung durch reguläre Ausdrücke, Schriften zur Informatik und angewandten Mathematik 122, RWTH Aachen, 1986.
Harel, D., Kozen, D., Parikh, R., Process logic: expressiveness, decidability and completeness, Journal of Computer and System Sciences 18 (1982), 144–170.
Kamp, H.W., Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968.
Kozen, D., Parikh, R., A decision procedure for the propositional μ-calculus, Second Workshop on Logics of Programs, Lecture Notes in Computer Science 164 (1983), 313–325.
Lichtenstein, O., Pnueli, A., Zuck, L., The glory of the past, Proc. Logics of Programs, New York, Lecture Notes in Computer Science 193 (1985), 196–218.
Rabin, M.O., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc. 141 (1969), 1–35.
Rabin, M.O., Weakly definable relations and special automata, in "Math. Logic and Found. of Set Theory", Y. Bar-Hillel, Ed., North-Holland, 1970, pp. 1–23.
Rosenstein, J.G., Linear orderings, Academic Press, New York, 1982.
Thomas, W., Logical aspects in the study of tree languages, in "9th Coll. on Trees in Algebra and Programming", B. Courcelle, Ed., Cambridge University Press, 1984, pp. 31–49.
Thomas, W., On chain logic, path logic, and first-order logic over infinite trees, 2nd IEEE Sympos. Logic in Computer Science, 1987.
Wolper, P., Temporal logic can be more expressive, Information and Control 56 (1983), 72–99.
Vardi, M.Y., Stockmeyer, L., Improved upper and lower bounds for modal logics of programs: Preliminary report, Proc. 17th ACM Sympos. on Theory of Computing, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hafer, T., Thomas, W. (1987). Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (eds) Automata, Languages and Programming. ICALP 1987. Lecture Notes in Computer Science, vol 267. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18088-5_22
Download citation
DOI: https://doi.org/10.1007/3-540-18088-5_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-18088-3
Online ISBN: 978-3-540-47747-1
eBook Packages: Springer Book Archive