基于Resolution算法的交互时态逻辑自动验证机

Currently, the technologies of theorem proving in the formal verification field have been applied to verify the correctness of software or hardware design in many critical systems, for instance air traffic control systems and missile launching systems, by some international companies and organizations. Automated theorem provers for various logics have been developed and utilized as tools for verification by many universities and enterprises abroad. For example, NASA used theorem provers to verify the behavior of their Mars Roller; IBM and Intel established their own research labs to use theorem proving techniques to find the defects in their CPU design; the University of Manchester and the University of Liverpool developed efficient theorem provers for first-order logic and Computation Tree Logic, respectively. Alternating-Time Temporal Logic (ATL) is a logic which has a powerful expressiveness in the class of temporal logics and, therefore, plays a very important role in the formal verification field. However, at the present, the theorem proving techniques for such a well-known and useful logic, namely ATL, has not been thoroughly explored and, moreover, theorem provers for ATL do not exist so for as we know. The aim of this research project is to investigate further in the field of theorem proving for ATL and create the first prover of ATL for researchers in the universities or enterprises who have the need to use ATL to perform formal verification for their critical systems. The research of this application consists of the following two parts: a) establish a clausal resolution calculus for ATL, which must be sound and complete; b) develop an automated resolution theorem prover for ATL based on the aforementioned calculus.

目前在形式化验证领域中自动定理证明技术已在国外开始被一些超大型IT企业用来对关键系统的软硬件设计进行验证。各种逻辑的自动验证机相继的被国外的高校和企业开发并投入了使用。如美国宇航局应用自动验证机对其火星探测器的行为进行验证；IBM，Intel建立了自己的实验室并开发了相应自动验证机验证其CPU设计的正确性。英国的曼彻斯特大学和利物浦大学分别开发出了高效的一阶逻辑和树逻辑的自动验证机。交互时态逻辑（ATL）是一种表达能力强，又在形式化验证方面十分重要的时态逻辑。但目前国际和国内对ATL自动定理证明技术的研究尚浅，且尚无ATL的自动验证机问世。所以本项目的目标是深化ATL自动定理证明技术的研究，为发展我国关键系统设计的校验技术提供基础。本项目的工作可以分为两个阶段：a) 创立基于Resolution算法的ATL推理算法，并证明此算法具有可靠性和完备性。b) 开发出基于此算法的ATL自动验证机。

Resolution算法自从60年代被提出后，就一直被认为是自动定理证明领域中最重要的基础理论之一。由于该算法很容易被计算机所实现，所以它被称之为“面向机器的算法”。因此，它一直是计算机逻辑领域内的学者所关注的焦点之一。.时序逻辑是人工智能和计算机科学领域中的一个重要的建立模型和验证模型的工具。计算树逻辑(CTL)是离散分支时序逻辑中最重要的一种。它所提供的路径量词 A 和E，使我们对未来分支的描述和约束成为可能。而交互时态逻辑（ATL）是在CTL逻辑的基础上引入了参与者的概念而形成的一种全新的逻辑。ATL逻辑表达式可以处理更多CTL逻辑无法描述的复杂问题。本项目的主要研究内容为利用Resolution算法设计出具有可靠性和完备性的交互时态逻辑ATL推理演算法。.项目组主要做了以下重点工作；（1）对最新的关于Resolution算法的文献进行广泛的收集和整理，形成了一个比较完整的综述。（2）由于计算树逻辑和交互时态逻辑有很大程度的相似性，项目组将计算树逻辑Resolution算法作为项目基础，对其进行了完整的系统化的综合和改进，并且对一些缺乏严谨数学证明的定理和推理进行了补全。最后，我们形成了一篇完整的计算树逻辑Resolution算法的高水平论文（全文共50页,文章发表时,该期刊在 SCI的Logic 类下的所有期刊里排名第4）。该文章对我们的后续工作产生了重要的贡献。（3）我们将Resolution算法扩展到Next-Fragment交互时态逻辑(XATL)中，并且成功的发表了一篇SCI论文。（4）我们将前面介绍的XATL逻辑的Resolution算法用计算机完整地实现并进行了优化。主要是通过给推理规则加入了顺序的约束，从而大大减少应用推理规则的次数，提升证明器的计算效率。自动定理证明器的研究结果发表在了本领域中重要的国际会议上。（5）最后，我们结合CTL逻辑的Resolution算法和XATL逻辑的Resolution算法得到了交互时态逻辑ATL的Resolution算法。 (6)另外，在我们对CTL逻辑、XATL逻辑和ATL逻辑研究的同时，我们受到了很多的启发，其中一项帮助我们找到了一种新的扩展方法。该方法可以将CTL逻辑的Resolution算法加入不多的新推理规则来处理另一种非常实用的刻画逻辑，即扩展计算树逻辑。这部分贡献属于本项目额外的收获。