Skip to main content
SpringerLink
Log in

Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

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

Included in the following conference series:

Abstract

We show that Branching-time temporal logics CTL and \(\mathbf{CTL}^*\), as well as Alternating-time temporal logics ATL and \(\mathbf{ATL}^*\), are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, while satisfiability for \(\mathbf{CTL}^*\), as well as for \(\mathbf{ATL}^\mathbf{*}\), with a single variable is 2EXPTIME-complete,—i.e., for these logics, the satisfiability for formulas with only one variable is as hard as satisfiability for arbitrary formulas.

This work has been supported by Russian Foundation for Basic Research, projects 16-07-01272 and 17-03-00818.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    To avoid ambiguity, we emphasise that we use the standard complexity-theoretic convention of measuring the complexity of the input as its size; in our case, this is the length of the input formula. In other words, we do not measure the complexity of the input according to how many distinct variables it contains; limiting the number of variables simply provides a restriction on the languages we consider.

References

  1. Alur, R., Henzinger, T.A., Kuperman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270

    Article  MathSciNet  MATH  Google Scholar 

  2. Blackburn, P., Spaan, E.: A modal perspective on the computational complexity of attribute value grammar. J. Log. Lang. Inf. 2, 129–169 (1993). https://doi.org/10.1007/bf01050635

    Article  MathSciNet  MATH  Google Scholar 

  3. Chagrov, A., Rybakov, M.: How many variables does one need to prove PSPACE-hardness of modal logics? In: Advances in Modal Logic, vol. 4, pp. 71–82. King’s College Publications (2003)

    Google Scholar 

  4. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981). https://doi.org/10.1007/bfb0025774

    Chapter  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  6. David, A.: Deciding \(\sf ATL^*\) satisfiability by tableaux. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 214–228. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_14

    Chapter  Google Scholar 

  7. Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science, vol. 58. Cambridge University Press, Cambridge (2016). https://doi.org/10.1017/cbo9781139236119

    Book  MATH  Google Scholar 

  8. Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84–103 (2002). https://doi.org/10.1006/inco.2001.3094

    Article  MathSciNet  MATH  Google Scholar 

  9. van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Studies In Epistemology, Logic, Methodology, and Philosophy of Science, vol. 337. Springer, Heidelberg (2008). https://doi.org/10.1007/978-1-4020-5839-4

    Book  MATH  Google Scholar 

  10. Emerson, E.A., Halpern, J.: Decision procedures and expressiveness in temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985). https://doi.org/10.1016/0022-0000(85)90001-7

    Article  MathSciNet  MATH  Google Scholar 

  11. 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). https://doi.org/10.1145/4904.4999

    Article  MathSciNet  MATH  Google Scholar 

  12. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  13. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979). https://doi.org/10.1016/0022-0000(79)90046-1

    Article  MathSciNet  MATH  Google Scholar 

  14. Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of the alternating-time temporal logic. Theor. Comput. Sci. 353(1–3), 93–117 (2006). https://doi.org/10.1016/j.tcs.2005.07.043

    Article  MathSciNet  MATH  Google Scholar 

  15. Goranko, V., Passy, S.: Using the universal modality: gains and questions. J. Log. Comput. 2(1), 5–30 (1989). https://doi.org/10.1093/logcom/2.1.5

    Article  MathSciNet  MATH  Google Scholar 

  16. Goranko, V., Shkatov, D.: Tableau-based decision procedure for multi-agent epistemic logic with operators of common and distributed knowledge. In: Proceedings of 6th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, November 2008, pp. 237–246. IEEE CS Press, Washington, DC (2008). https://doi.org/10.1109/sefm.2008.27

  17. Goranko, V., Shkatov, D.: Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time. In: Sierra, C., Castelfranchi, C., Decker, K.S., Sichman, J.S. (eds.) Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2009, Budapest, May 2009, vol. 2, pp. 969–976. International Federation AAMAS (2009). https://dl.acm.org/citation.cfm?id=1558147

  18. Goranko, V., Shkatov, D.: Tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of branching time. In: Baldoni, M., et al. (eds.) Proceedings of 2nd Multi-Agent Logics, Languages, and Organisations Federated Workshops, Turin, September 2009, CEUR Workshop Proceedings, vol. 494, CEUR-WS.org (2009). http://ceur-ws.org/Vol-494/famaspaper7.pdf

  19. Goranko, V., Shkatov, D.: Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log. 11(1) (2009). https://doi.org/10.1145/1614431.1614434. Article 3

    Article  MathSciNet  Google Scholar 

  20. Goranko, V., Shkatov, D.: Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 197–213. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92687-0_14

    Chapter  Google Scholar 

  21. Halpern, J.Y.: The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artif. Intell. 75(2), 361–372 (1995). https://doi.org/10.1016/0004-3702(95)00018-a

    Article  MathSciNet  MATH  Google Scholar 

  22. Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time I: lower bounds. J. Comput. Syst. Sci. 38(1), 195–237 (1989). https://doi.org/10.1016/0022-0000(89)90039-1

    Article  MathSciNet  MATH  Google Scholar 

  23. Hemaspaandra, E.: The complexity of poor man’s logic. J. Log. Comput. 11(4), 609–622 (2001). https://doi.org/10.1093/logcom/11.4.609

    Article  MathSciNet  MATH  Google Scholar 

  24. van der Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Studia Logica 75(1), 125–157 (2003). https://doi.org/10.1023/a:1026185103185

    Article  MathSciNet  MATH  Google Scholar 

  25. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, Cambridge (2004). https://doi.org/10.1017/cbo9780511810275

    Book  MATH  Google Scholar 

  26. Lutz, C.: Complexity and succinctness of public announcement logic. In: Nakashima, H., Wellman, M.P., Weiss, G., Stone, P. (eds.) Proceedings of 5th International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2006, Hakodate, May 2006, pp. 137–143. ACM Press (2006). https://doi.org/10.1145/1160633.1160657

  27. Nagle, M.C., Thomason, S.K.: The extensions of the modal logic K5. J. Symb. Log. 50(1), 102–109 (1975). https://doi.org/10.2307/2273793

    Article  MATH  Google Scholar 

  28. Nishimura, I.: On formulas of one variable in intuitionistic propositional calculus. J. Symb. Log. 25(4), 327–331 (1960). https://doi.org/10.2307/2963526

    Article  MathSciNet  MATH  Google Scholar 

  29. Plaza, J.A.: Logics of public communications. In: Emrich, M.L., Pfeifer, M.S., Hadzikadic, M., Ras, Z.W. (eds.) Proceedings of 4th International Symposium on Methodologies for Intelligent Systems: Poster Session Program, pp. 201–216, Oak Ridge National Laboratory (1989). (Reprinted as: Synthese 158(2), 165–179 (2007). https://doi.org/10.1007/s11229-007-9168-7)

    Article  MathSciNet  Google Scholar 

  30. Reynolds, M.: A tableau for CTL*. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 403–418. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_26

    Chapter  Google Scholar 

  31. Rybakov, M., Shkatov, D.: Complexity and expressivity of propositional dynamic logics with finitely many variables. Log. J. IGPL 26(5), 539–547 (2018). https://doi.org/10.1093/jigpal/jzy014

    Article  MathSciNet  Google Scholar 

  32. Rybakov, M., Shkatov, D.: Complexity of finite-variable fragments of propositional modal logics of symmetric frames. Log. J. IGPL (to appear). https://doi.org/10.1093/jigpal/jzy018

  33. Rybakov, M., Shkatov, D.: Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter. Studia Logica (to appear). https://doi.org/10.1007/s11225-018-9815-7

  34. Schewe, S.: ATL* satisfiability Is 2EXPTIME-complete. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 373–385. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_31

    Chapter  Google Scholar 

  35. Shoham, Y., Leyton-Brown, K.: Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, Cambridge (2008). https://doi.org/10.1017/cbo9780511811654

    Book  MATH  Google Scholar 

  36. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985). https://doi.org/10.1145/3828.3837

    Article  MathSciNet  MATH  Google Scholar 

  37. Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs (preliminary report). In: Proceedings of 17th Annual ACM Symposium on Theory of Computing, STOC 1985, Providence, RI, May 1985, pp. 240–251. ACM Press, New York (1985). https://doi.org/10.1145/22145.22173

  38. Švejdar, V.: The decision problem of provability logic with only one atom. Arch. Math. Log. 42(8), 763–768 (2003). https://doi.org/10.1007/s00153-003-0180-4

    Article  MathSciNet  MATH  Google Scholar 

  39. Walther, D.: ATEL with common and distributed knowledge is ExpTime-complete. In: Schlingloff, H. (ed.) Methods for Modalities 4. Informatik-Berichte, vol. 194, pp. 173–186. Humboldt-Universität zu Berlin (2005)

    Google Scholar 

  40. Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: ATL satisfiability is indeed EXPTIME-complete. J. Log. Comput. 16(6), 765–787 (2006). https://doi.org/10.1093/logcom/exl009

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tver State University, Tver, Russia

    Mikhail Rybakov

  2. University of the Witwatersrand, Johannesburg, South Africa

    Mikhail Rybakov & Dmitry Shkatov

Authors
  1. Mikhail Rybakov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dmitry Shkatov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dmitry Shkatov .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Rybakov, M., Shkatov, D. (2018). Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02507-6

  • Online ISBN: 978-3-030-02508-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation