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

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

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.