模型检测动态认知逻辑

Model checking has been applied into the areas of computer hardware, software and control systems, and made dramatic achievements. This project will investigate the model checking problem for multiagent systems by considering epistemic communication acts of agents. We will propose a framework of epistemic communication model for multiagent systems, and endows the new generation of dynamic epistemic logic a computationally grounded model. The corresponding axiomatic systems and model checking algorithms will be given and investigated. We will implement the model checking algorithms by using symbolic techniques like SAT and BDD, and carry out some case studies, including verification of informational security protocol and epistemic planning.

模型检测已经被用于计算机硬件、软件和控制系统等领域并取得了令人瞩目的成就.本项目从智能体之间的认知通信行为出发,研究多智能体系统的模型检测问题.本项目将提出多智能体系统的认知通信模型并给出新一代动态认知逻辑的给予计算的语义模型,进而给出相应的逻辑公理系统和模型检测算法.本项目将使用可满足性问题求解和二元决策图等符号化技术实现我们的模型检测算法,并给出信息安全协议验证和认知规划的应用案例.

模型检测已经被用于计算机硬件、软件和控制系统等领域并取得了令人瞩目的成就. 本项目从智能体之间的认知通信行为出发, 研究多智能体系统的模型检测问题. 主要内容包括：多智能体系统信息交互的模型研究; 基于多智能体系统信息交互模型的动态认知逻辑的研究； 模型检测多智能体系统的算法研究和模型检测多智能体系统的应用案例. 本项目已经提出了多智能体系统的认知通信模型并给出新一代动态认知逻辑的给予计算的语义模型, 而且给出相应的逻辑公理系统和模型检测算法. 并且使用可满足性问题求解(SAT)和二元决策图(BDD)等符号化技术实现我们的模型检测算法. 项目组在项目的支持下，已在多智能体逻辑建模, 动态认识逻辑(DEL)的符号化模型检测, 大规模软件系统的逻辑规范模型检测和逻辑优化计算方面取得一系列突出成果,项目组还超越了项目计划书的内容，探索逻辑推理技术与深度神经网络(Deep Neural Network)技术的结合，尝试把符号推理和机器学习融合起来解决人工智能的问题。本项目取得了较为突出的成果，在国际顶级会议和国际学报上已经发表论文22篇(SCI 7篇，EI 15篇)，其中包括CCF A类论文7篇 (AAAI 1篇 , IJCAI 3篇, ASE 1篇， Artificial Intelligence 1篇和IEEE Transactions on Software Engineering 1篇)，超额完成了研究任务。