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

项目名称： 基于Resolution算法的交互时态逻辑自动验证机

项目编号： No.61303018

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 章岚

作者单位： 首都经济贸易大学

项目金额： 22万元

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

中文关键词： 交互时态逻辑；自动定理证明；形式化验证；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 an

英文关键词： Alternating-Time Temporal Logic；Theorem Proving；Formal Verification；Resolution Calculus；