Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
arXiv:1810.09142 · doi:10.1007/978-3-030-02508-3_21
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.
arXiv commentPrefinal version of the published paper
References in corpus (4)
- Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
- Complexity and expressivity of propositional dynamic logics with finitely many variables
- Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge
- Complexity of finite-variable fragments of propositional modal logics of symmetric frames