Abstract
We classify the complexity of the satisfiability problem for extensions of CTL and UB. The extensions we consider are Boolean combinations of path formulas, fairness properties, past modalities, and forgettable past. Our main result shows that satisfiability for CTL with all these extensions is still in 2EXPTIME, which strongly contrasts with the nonelementary complexity of CTL*. with forgettable past. We give a complete classification of combinations of these extensions, yielding a dichotomy between extensions with 2EXPTIME-complete and those with EXPTIME-complete complexity. In particular, we show that satisfiability for the extension of UB with forgettable past is complete for 2EXPTIME, contradicting a claim for a stronger logic in the literature. The upper bounds are established with the help of a new kind of pebble automata.
Keywords
Supported by DFG grant SCHW 678/4-1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)
Bozzelli, L.: The complexity of CTL* + linear past. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 186–200. Springer, Heidelberg (2008)
Chlebus, B.S.: Domino-tiling games. J. Comput. Syst. Sci. 32(3), 374–392 (1986)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, MIT Press (1990)
Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)
Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. of the 32nd FOCS 1991, pp. 368–377. IEEE, Los Alamitos (1991)
Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132–158 (1999)
Gabbay, D.M.: The declarative past and imperative future: Executable temporal logic for interactive systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989)
Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)
Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987)
Johannsen, J., Lange, M.: CTL + is complete for double exponential time. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 767–775. Springer, Heidelberg (2003)
Kupferman, O., Pnueli, A.: Once and for all. In: Proc. of the 10th LICS 1995, pp. 25–35. IEEE, Los Alamitos (1995)
Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proc. of the 21st LICS 2006, pp. 265–274. IEEE, Los Alamitos (2006)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)
Lamport, L.: “Sometimes” is sometimes “not never”. In: Proc. of the7th POPL 1980, pp. 174–185. ACM Press, New York (1980)
Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303–324 (1995)
Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for verification in CTL. Inf. Comput. 156(1-2), 236–263 (2000)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1–35 (1969)
ten Cate, B., Segoufin, L.: XPath, transitive closure logic, and nested tree walking automata. In: Proc. of the 27th PODS 2008, pp. 251–260. ACM Press, New York (2008)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–192. Elsevier, MIT Press (1990)
Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)
Vardi, M.Y., Stockmeyer, L.J.: Improved upper and lower bounds for modal logics of programs. In: Proc. of the 17th STOC 1985, pp. 240–251. ACM Press, New York (1985)
Weber, V.: On the complexity of branching-time logics. Available from arXiv:0906.2521 [cs.LO]
Weber, V.: Branching-time logics repeatedly referring to states. Accepted to JoLLI (2009); An extended abstract appered in the procedings of HyLo (2007)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata and infinite trees. Theoretical Computer Science 200, 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weber, V. (2009). On the Complexity of Branching-Time Logics. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)