命题量化为什么使得树上的模态和时态逻辑变得强韧困难？
摘要：对于模态逻辑K、T或S4添加命题量化已知会导致不可判定性，但是基于树形语义的CTL命题量化（tQCTL）具有非元素级的Tower完备可满足性问题。我们研究了tQCTL的严格片段以及基于树形语义的模态逻辑K和命题量化的复杂性。具体来说，我们发现仅限于时态算子EX的tQCTL已经是Tower难解的，这是意料之外的，因为EX只能确保局部性质。当存在某个N >= 2时，我们证明了限制在N边界树上的tQCTL的可满足性问题是AExpPol完备的；通过从最近引入的平铺问题进行约简，我们建立了AExpPol困难性，该问题对于研究区间时态逻辑的模型检验问题非常重要。作为我们证明方法的结果，我们证明了tQCTL在EF或EXEF上受限的Tower难解性以及基于树类语义的K、KD、GL、K4和S4等著名模态逻辑的命题量化的Tower难解性。
作者：Bartosz Bednarczyk and St''ephane Demri
论文ID：2104.13122
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22