文献类型：期刊文章

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

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

出　　处：《南京大学学报（自然科学版）》

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

年　　份：2008

卷　　号：44

期　　号：2

起止页码：171-178

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CAS、CSCD、CSCD2011_2012、MR、ZGKJHX、ZMATH、核心刊

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

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

分 类 号：TP18]