Why propositional quantification makes modal logics on trees robustly hard?

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Why propositional quantification makes modal logics on trees robustly hard?

Vortrag von Bartosz Bednarczyk
Bartosz Bednarczyk and Stephane Demri. Why propositional quantification makes modal logics on trees robustly hard? In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'19), Vancouver, Canada, June 2019. IEEE Press. To appear.


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 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 QCTL^t restricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.