一句话：证明树上命题量化模态逻辑的 EX 片段已 Tower-hard，并给出有界树上的 AExppol-完全性。
在模态逻辑 K、T、S4 中加入命题量化会导致不可判定，而树语义下含命题量化的 CTL（QCTLt）的可满足性是非初等 Tower-完全。本文研究 QCTLt 的严格片段以及树语义下带命题量化的模态逻辑 K 的复杂度。作者证明，QCTLt 仅保留时态算子 EX 时已是 Tower-hard，这出乎意料，因为 EX 通常只能表达局部性质。对于 N≥2 的 N-有界树，EX 片段的复杂度精确为 AExppol-完全；AExppol-hardness 通过从新近用于区间时态逻辑模型检测的铺砖问题归约得到。作为证明方法的推论，还得到 QCTLt 限制到 EF 或 EXEF、以及 K、KD、GL、S4、K4、D4 等模态逻辑在基于树类语义下带命题量化的 Tower-hardness。
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 (QCTLt) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTLtas well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTLtrestricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When QCTLtrestricted 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 QCTLtrestricted 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.
DOI 原文 ·
@inproceedings{paperbot4971,
title = {Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?},
author = {Bartosz Bednarczyk and Stephane Demri},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785656}
}