模型检测动态认知逻辑

项目名称： 模型检测动态认知逻辑

项目编号： No.61472369

项目类型： 面上项目

立项/批准年度： 2015

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

项目作者： 苏开乐

作者单位： 暨南大学

项目金额： 86万元

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

中文关键词： 知识表示与推理；自动推理

英文摘要： 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.

英文关键词： knowledge representation and reasoning;automatic reasoning