文献类型：期刊文章

作　　者：骆翔宇[1,2] 苏开乐[3,4] 杨晋吉[3]

机构地区：[1]桂林电子科技大学计算机系 [2]中山大学计算机科学系,广东广州510275 [3]中山大学计算机科学系 [4]河南科技大学电子信息工程学院,河南洛阳471003

出　　处：《软件学报》

基　　金：国家自然科学基金Nos.60496327;10410638;60473004;国家重点基础研究发展规划(973)No.2005CB321900;广东省自然科学基金Nos.04205407;06023195~~

年　　份：2006

卷　　号：17

期　　号：12

起止页码：2485-2498

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20070310372713)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(boundedmodelchecking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKLn.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKLn的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.

关 键 词：模型检测  有界模型检测 多智体系统 同步时态认知模型  时态认知逻辑

分 类 号：TP301]