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

摘要：

交互时态认知逻辑(ATEL)是对交互时态逻辑(ATL)的扩展,但是它只刻画了知识,没有探讨信念的刻画问题.给出广义并发博弈结构,以模态算子的形式在ATL的语法层面给出了三种信念算子,在广义并发博弈结构下给出其语义,建立了交互时态信念逻辑(ATBL).给出一个多项式时间模型检测算法,并证明了ATBL的模型检测复杂度为PTIME-complete;给出并证明了ATBL的若干良好性质,比较了相关工作.对Agent认知形式化作了进一步探索,为多Agent系统研究提供了一个较好的形式化工具.

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

所属期刊栏目：44

分类号：TP18(自动化基础理论)

资助基金：国家自然科学基金60373079;60573076;中国科学院重点实验室基金SYSKF0505;福建省自然科学基金2006J0299

在线出版日期：2008-06-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：171-178