Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
Publikation: Beitrag in Fachzeitschrift › Forschungsartikel › Beigetragen › Begutachtung
Beitragende
Abstract
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 (QCTL t) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTL t as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTL t restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When QCTL t restricted to EX is interpreted on N-bounded trees for some N ≥ 2, we prove that the satisfiability problem is AExp pol-complete; AExp polhardness 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 QCTL t 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.
Details
Originalsprache | Englisch |
---|---|
Seiten (von - bis) | 5:1–5:46 |
Fachzeitschrift | Logical methods in computer science |
Jahrgang | 18 |
Ausgabenummer | 3 |
Publikationsstatus | Veröffentlicht - 1 Juli 2022 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85135163248 |
---|