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

Mikhail Rybakov, Dmitry Shkatov

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 pro…