一句话：证明仅含 EX 的树语义命题量化 CTL 已 Tower 难，并给出有界树上的 AExpPol 完全性及多类模态逻辑的 Tower 难下界。
本文研究命题量化如何影响树上模态与时序逻辑的可满足性复杂度。已知带命题量化的 K/T/S4 不可判定，而树语义下的 tQCTL 是 Tower 完全。作者分析 tQCTL 的严格片段及带命题量化的模态逻辑 K。关键结果显示，仅含 EX 的 tQCTL 片段已是 Tower 难，尽管 EX 只能表达局部性质；在 N≥2 的有界树上，该片段的可满足性为 AExpPol 完全，其难性由一种新 tiling 问题归约得到。由此进一步证明限制到 EF 或 EXEF 的 tQCTL，以及 K、KD、GL、K4、S4 等模态逻辑在树语义加命题量化下均为 Tower 难。
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.
@article{paperbot1682,
title = {Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?},
author = {Bartosz Bednarczyk and Stéphane Demri},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:5)2022}
}