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

TL;DR

This paper demonstrates that key branching- and alternating-time temporal logics maintain their full expressive power even with only one propositional variable, and it establishes the complexity of their satisfiability problems.

Contribution

It proves that these logics are as expressive with a single variable as with many, and determines the complexity of their satisfiability problems in this restricted setting.

Findings

CTL and CTL* satisfiability with one variable is EXPTIME-complete.

ATL and ATL* satisfiability with one variable is 2EXPTIME-complete.

Expressive power remains unchanged with a single propositional variable.

Abstract

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.