Skip to main content
SpringerLink
Log in

On the Complexity of Branching-Time Logics

  • Conference paper
Computer Science Logic (CSL 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5771))

Included in the following conference series:

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.

Supported by DFG grant SCHW 678/4-1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bozzelli, L.: The complexity of CTL* + linear past. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 186–200. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Chlebus, B.S.: Domino-tiling games. J. Comput. Syst. Sci. 32(3), 374–392 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. 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)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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)

    Article  MathSciNet  MATH  Google Scholar 

  10. 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)

    Google Scholar 

  11. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132–158 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol. 5000. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Kupferman, O., Pnueli, A.: Once and for all. In: Proc. of the 10th LICS 1995, pp. 25–35. IEEE, Los Alamitos (1995)

    Google Scholar 

  17. Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proc. of the 21st LICS 2006, pp. 265–274. IEEE, Los Alamitos (2006)

    Google Scholar 

  18. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  19. Lamport, L.: “Sometimes” is sometimes “not never”. In: Proc. of the7th POPL 1980, pp. 174–185. ACM Press, New York (1980)

    Google Scholar 

  20. Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303–324 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  21. Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for verification in CTL. Inf. Comput. 156(1-2), 236–263 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  22. Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  23. 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)

    Google Scholar 

  24. 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)

    Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. 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)

    Google Scholar 

  27. Weber, V.: On the complexity of branching-time logics. Available from arXiv:0906.2521 [cs.LO]

    Google Scholar 

  28. Weber, V.: Branching-time logics repeatedly referring to states. Accepted to JoLLI (2009); An extended abstract appered in the procedings of HyLo (2007)

    Google Scholar 

  29. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata and infinite trees. Theoretical Computer Science 200, 135–183 (1998)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität Dortmund, 44221, Dortmund, Germany

    Volker Weber

Authors
  1. Volker Weber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematische Grundlagen der Informatik, RWTH Aachen, 52056, Aachen, Germany

    Erich Grädel

  2. CENTRIA and Departamento de Matemática, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    Reinhard Kahle

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation