规范模型与模态团队逻辑的复杂性
摘要：在这项研究中，我们研究了模态团队逻辑MTL，这是模态逻辑ML的团队语义扩展，同时也可以由布尔否定闭合。它的片段，如模态依赖、独立性和包含性逻辑已经被很好地理解。然而，由于无限制的布尔否定，完整的MTL的可满足性问题一直以来都难以进行复杂性理论分类。 在我们的方法中，我们将规范模型的概念引入到团队语义设置中。通过构造这样一个模型，我们将MTL的可满足性问题约简为简单的模型检查问题。之后，我们证明了这种方法是最优的，因为MTL公式可以高效地强制具有规范性。 此外，为了将这些结果用复杂性术语进行捕捉，我们引入了一个非元素复杂性类TOWER(poly)，并证明它包含MTL的可满足性和有效性作为完全问题。我们还证明，具有有界模态深度的MTL片段是等级层次（多项式次数的交替）的完全问题。相应的困难结果适用于模态操作符和分裂析取的严格或松散语义，以及自反性和传递性框架类。
作者：Martin L"uck
论文ID：1709.05253
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22