时序认知混合逻辑APTEL的模型检测方法研究

Model checking is an automatic technique used to verify the properties of software and hardware systems. In the verification process, the key problems are how to describe the properties of systems using logical formulas accurately and how to design an efficient verification algorithm. The existing model checking methods based on single logic can no longer meet the increasingly complex verification requirements of software and hardware systems in the current intelligent era. Therefore, it is urgent to carry out a research on the verification methods based on hybrid logics. Temporal logic is used for reasoning the correctness of systems and epistemic logic is used for reasoning the information of systems. In order to reason the correctness and information of systems simultaneously, alternating projection temporal epistemic logic (APTEL) is obtained by combing alternating projection temporal logic with epistemic logic and a symbolic model checking method based on APTEL is proposed in this project. This project conducts research mainly focus on the following three aspects: (1) Defining the syntax and semantics of APTEL，reasoning and proving its logic laws, defining the normal form of APTEL formulas and designing an algorithm for transforming APTEL formulas to normal forms; (2) Making study on the problem of decidability of APTEL; (3) Studying on the APTEL symbolic model checking method based on automata. The results of this project can provide sound theoretical foundations and automatic techniques for verifying the security and reliability of popular intelligent products in current.

模型检测是一种用于验证软硬件系统性能的自动化技术，其中如何基于逻辑准确描述系统的性质并设计出高效的检测算法是验证过程中的关键问题。现有基于单一逻辑的模型检测方法已不能满足智能时代软硬件系统日趋复杂的验证需求，因此迫切需要开展基于混合逻辑验证方法的研究。时序逻辑用于推理系统的正确性，认知逻辑用于推理系统的信息，为了同时推理系统的正确性和信息，本项目将交替投影时序逻辑与认知逻辑相融合得到交替投影时序认知逻辑（APTEL），并提出基于APTEL的符号模型检测方法。主要研究内容包括：（1）定义APTEL的语法和语义，推理逻辑规则并予以证明，定义APTEL公式的范式并设计转化范式的算法；（2）研究APTEL的判定问题；（3）研究基于自动机的APTEL符号模型检测方法。本项目的研究成果可为验证日趋普及的智能产品的安全性和可靠性提供坚实的理论依据和自动化技术。

模型检测是一种用于验证软硬件系统性能的形式化验证方法，如何基于逻辑准确描述系统的性质并设计出高效的检测算法是验证过程中的关键问题。多智能体系统是一种全新的分布式系统，是由在特定环境中交互的多个智能体组成的计算机系统。其广泛应用于智能机器人、交通控制、分布式预测、监控及诊断、分布式智能决策及虚拟现实等方面。验证多智能体系统的性质是人工智能研究中面临的棘手问题之一。现阶段多智能体系统的模型检测方法大多采用时序逻辑描述系统的性质，而时序逻辑不具备描述多智能体系统认知属性的能力。因此现有基于单一逻辑的模型检测方法已不满足多智能体系统验证的需求，迫切需要开展基于混合逻辑验证方法的研究。时序逻辑用于推理系统的正确性，认知逻辑用于推理系统的信息，本项目将交替投影时序逻辑APTL与认知逻辑相融合，得到交替投影时序认知逻辑APTEL，并且开展了相关研究工作。.本项目主要研究内容如下：.首先，进一步开展了时序逻辑APTL的相关研究，提出并实现了基于自动机的APTL统一模型检测方法。然后，提出了基于时序逻辑APTL的智能体的路径规划方法，并且开发了相应的工具。最后，本项目将时序逻辑APTL与认知逻辑相融合得到交替投影时序认知逻辑APTEL，并开展了相关的理论证明和研究。.本项目共发表或录用论文7篇，其中3篇期刊论文，4篇会议论文，培养硕士研究生1名。开展项目期间多次参加国际及国内会议，在国际会议上共做三次报告。