Why is Modal Logic So Robustly Decidable?
Why is Modal Logic So Robustly Decidable?
复制标题
为什么模态逻辑如此稳健可判定？
DOI：
10.1090/dimacs/031/05
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
Moshe Y. Vardi
在过去的20年中，模态逻辑已经被应用于计算机科学的许多领域，包括人工智能，程序验证，硬件验证，数据库理论和分布式计算。模态逻辑有两个主要的计算问题。第一个问题是检查给定公式在给定结构的给定状态下是否为真。这个问题被称为模型检查问题。第二个问题是检查给定的公式是否在所有结构的所有状态下都为真。这个问题被称为有效性问题。这两个问题都是可以解决的。模型检验问题可以在线性时间内解决，而有效性问题是PSPACE完全的。这是相当令人惊讶的，当一个人考虑到模态逻辑，尽管其明显的命题语法，本质上是一个一阶逻辑，因为必要性和可能性模态量化的一组可能的世界，模型检查和有效性的一阶逻辑是计算困难的问题。那么，为什么模态逻辑如此鲁棒可判定？为了回答这个问题，我们必须仔细研究模态逻辑作为一阶逻辑的一部分。仔细的研究表明，命题模态逻辑实际上可以被看作是2-变量一阶逻辑的一个片段。事实证明，这个片段在计算上比完整的一阶逻辑更易处理，这为模态逻辑的易处理性提供了一些解释。然而，经过更深入的研究，我们发现这种解释并不令人满意。模态逻辑的易处理性是相当的，不能用与二变量一阶逻辑的关系来解释。我们认为，模态逻辑的强大的可判定性可以解释所谓的树模型属性，我们展示了树模型属性如何导致基于自动机的决策过程。这里报告的研究是在作者访问DIMACS和贝尔实验室时进行的，这是DIMACS逻辑和算法特别年的一部分。
In the last 20 years modal logic has been applied to numerous areas of computer science, including artificial intelligence, program verification, hardware verification, database theory, and distributed computing. There are twomain computational problems associated with modal logic. The first problem is checking if a given formula is true in a given state of a given structure. This problem is known as the model-checking problem. The second problem is checking if a given formula is true in all states of all structures. This problem is known as the validity problem. Both problems are decidable. The modelchecking problem can be solved in linear time, while the validity problem is PSPACE-complete. This is rather surprising when one considers the fact that modal logic, in spite of its apparent propositional syntax, is essentially a first-order logic, since the necessity and possibility modalities quantify over the set of possible worlds, and model checking and validity for first-order logic are computationally hard problems. Why, then, is modal logic so robustly decidable? To answer this question, we have to take a close look at modal logic as a fragment of first-order logic. A careful examination reveals that propositional modal logic can in fact be viewed as a fragment of 2-variable first-order logic. It turns out that this fragment is computationally much more tractable than full first-order logic, which provides some explanation for the tractability of modal logic. Upon a deeper examination, however, we discover that this explanation is not too satisfactory. The tractability of modal logic is quite and cannot be explained by the relationship to two-variable first-order logic. We argue that the robust decidability of modal logic can be explained by the so-called tree-model property, and we show how the tree-model property leads to automata-based decision procedures. The research reported here was conducted while the author was visiting DIMACS and Bell Laboratories as part of the DIMACS Special Year on Logic and Algorithm.