1. Why Propositional Quantification Makes Modal and Temporal Logics on Trees Robustly Hard?
- Author
-
Bartosz Bednarczyk, Stéphane Demri, Uniwersytet Wroclawski, Technische Universität Dresden = Dresden University of Technology (TU Dresden), Centre National de la Recherche Scientifique (CNRS), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Faculty of Computer Science [TU Dresden]
- Subjects
FOS: Computer and information sciences ,[INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC] ,Computer Science - Logic in Computer Science ,General Computer Science ,modal logic K ,Theoretical Computer Science ,[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] ,expressive power ,tower-hardness ,propositional quantification ,branching-time temporal logic CTL ,modal logic K4 ,[INFO]Computer Science [cs] ,modal logic ,tiling problem ,nonelementarity ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,nominal ,Logic in Computer Science (cs.LO) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,modal logic GL ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,undecidability ,tree unfolding ,tree semantics ,complexity - Abstract
Submitted to LMCS. Full version of our LICS 2019 paper; Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.
- Published
- 2021
- Full Text
- View/download PDF