• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

Complexity and expressivity of Branching- and Alternating-time temporal logics with finitely many variables

P. 396-414.
Rybakov M., Shkatov D.

We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and 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 CTL*, as well as for ATL*, 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.

In book

Edited by: B. Fisher, T. Uustalu. Vol. 11187. Springer, 2018.