交互时态信念逻辑及其模型检测  

Alternating-time temporal belief logic and its model checking

作　　者：宁正元[1] 胡山立[2] 赖贤伟[1] 

机构地区：[1]福建农林大学计算机科学与技术系,福州350002 [2]福州大学计算机科学与技术系

出　　处：《南京大学学报（自然科学版）》2008年第2期171-178,共8页Journal of Nanjing University（Natural Science）

基　　金：国家自然科学基金(60373079,60573076);中国科学院计算机科学重点实验室开放课题基金(SYSKF0505);福建省自然科学基金(2006J0299)

摘　　要：交互时态认知逻辑(ATEL)是对交互时态逻辑(ATL)的扩展,但是它只刻画了知识,没有探讨信念的刻画问题.给出广义并发博弈结构,以模态算子的形式在ATL的语法层面给出了三种信念算子,在广义并发博弈结构下给出其语义,建立了交互时态信念逻辑(ATBL).给出一个多项式时间模型检测算法,并证明了ATBL的模型检测复杂度为PTIME-complete;给出并证明了ATBL的若干良好性质,比较了相关工作.对Agent认知形式化作了进一步探索,为多Agent系统研究提供了一个较好的形式化工具.In recent years, great interest is shown in the developing of multi-agent cooperation logics for the representation, reasoning and verification of multi-agent systems. The two foundamental multi-agent cooperation logics are called ATL （Alternating-time Temporal Logic） and CL （coalition game logic）. Further work of muhb agent cooperation logics is done by investigating their complexity of satisfiability and model checking, as well as succinctness and expressivity. Furthermore, although much research work is left to be done, the combination of mult-agent cooperation logics with epistemic logic, BDI logic, normative systems and game theory turns out to be possible as a result. On extending ATL, ATEL （Alternating time Temporal Epistemic Logic） was developed. In ATEL, knowledge operators were added and its model checking complexity was investigated. However, belief operators were not taken into account. In this paper, first of all, the generalized concurrent game structures are introduced. Secondly, by introducing three kinds of belief operators into ATL and describing their semantics based on generalized concurrent game structures, a new logic which is called ATBL （Alternating-time Temporal Belief Logic） is developed. Last but not the least, a model checking algorithm whose time complexity is polynomial is developed, and it is proved that the model checking complexity of ATBL is PTIME complete. So that ATBL who is the counterpart of ATEL is developed for the research of multi agent systems, and the epistemic formalization of agents is further explored. Further work can be carried out on developing a sound and complete axiom system for ATBL, and the succinctness of this newly developed multi-agent cooperation logic can be investigated in depth and improved hopefully.

关 键 词：交互时态逻辑 并发博弈结构 模型检测 知识 信念 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]