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

  • Mikhail Rybakov
  • Dmitry ShkatovEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


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.


Branching-time temporal logics Alternating-time temporal logics Finite-variable fragments Computational complexity Semantic expressivity Satisfiability problem 


  1. 1.
    Alur, R., Henzinger, T.A., Kuperman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). Scholar
  2. 2.
    Blackburn, P., Spaan, E.: A modal perspective on the computational complexity of attribute value grammar. J. Log. Lang. Inf. 2, 129–169 (1993). Scholar
  3. 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. 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). Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  6. 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). Scholar
  7. 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). Scholar
  8. 8.
    Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84–103 (2002). Scholar
  9. 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). Scholar
  10. 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). Scholar
  11. 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). Scholar
  12. 12.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  13. 13.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979). Scholar
  14. 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). Scholar
  15. 15.
    Goranko, V., Passy, S.: Using the universal modality: gains and questions. J. Log. Comput. 2(1), 5–30 (1989). Scholar
  16. 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).
  17. 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).
  18. 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, (2009).
  19. 19.
    Goranko, V., Shkatov, D.: Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log. 11(1) (2009). Article 3MathSciNetCrossRefGoogle Scholar
  20. 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). Scholar
  21. 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). Scholar
  22. 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). Scholar
  23. 23.
    Hemaspaandra, E.: The complexity of poor man’s logic. J. Log. Comput. 11(4), 609–622 (2001). Scholar
  24. 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). Scholar
  25. 25.
    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, Cambridge (2004). Scholar
  26. 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).
  27. 27.
    Nagle, M.C., Thomason, S.K.: The extensions of the modal logic K5. J. Symb. Log. 50(1), 102–109 (1975). Scholar
  28. 28.
    Nishimura, I.: On formulas of one variable in intuitionistic propositional calculus. J. Symb. Log. 25(4), 327–331 (1960). Scholar
  29. 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). Scholar
  30. 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). Scholar
  31. 31.
    Rybakov, M., Shkatov, D.: Complexity and expressivity of propositional dynamic logics with finitely many variables. Log. J. IGPL 26(5), 539–547 (2018). Scholar
  32. 32.
    Rybakov, M., Shkatov, D.: Complexity of finite-variable fragments of propositional modal logics of symmetric frames. Log. J. IGPL (to appear).
  33. 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).
  34. 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). Scholar
  35. 35.
    Shoham, Y., Leyton-Brown, K.: Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, Cambridge (2008). Scholar
  36. 36.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985). Scholar
  37. 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).
  38. 38.
    Švejdar, V.: The decision problem of provability logic with only one atom. Arch. Math. Log. 42(8), 763–768 (2003). Scholar
  39. 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. 40.
    Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: ATL satisfiability is indeed EXPTIME-complete. J. Log. Comput. 16(6), 765–787 (2006). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Tver State UniversityTverRussia
  2. 2.University of the WitwatersrandJohannesburgSouth Africa

Personalised recommendations