Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
Logic in Computer Science
2019-01-23 v2
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.
Cite
@article{arxiv.1810.09142,
title = {Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables},
author = {Mikhail Rybakov and Dmitry Shkatov},
journal= {arXiv preprint arXiv:1810.09142},
year = {2019}
}
Comments
Prefinal version of the published paper