首页 | 本学科首页   官方微博 | 高级检索  
     

有界模型检测同步多智体系统的时态认知逻辑
引用本文:骆翔宇,苏开乐,杨晋吉.有界模型检测同步多智体系统的时态认知逻辑[J].软件学报,2006,17(12):2485-2498.
作者姓名:骆翔宇  苏开乐  杨晋吉
作者单位:1. 桂林电子科技大学计,算机系,广西,桂林,541004;中山大学,计算机科学系,广东,广州,510275
2. 中山大学,计算机科学系,广东,广州,510275;河南科技大学,电子信息工程学院,河南,洛阳,471003
3. 中山大学,计算机科学系,广东,广州,510275
基金项目:国家自然科学基金;国家重点基础研究发展计划(973计划);广东省自然科学基金
摘    要:提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKLn.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKLn的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.

关 键 词:模型检测  有界模型检测  多智体系统  同步时态认知模型  时态认知逻辑
收稿时间:2005-02-22
修稿时间:1/9/2006 12:00:00 AM

Bounded Model Checking for Temporal Epistemic Logic in Synchronous Multi-Agent Systems
LUO Xiang-Yu,SU Kai-Le and YANG Jin-Ji.Bounded Model Checking for Temporal Epistemic Logic in Synchronous Multi-Agent Systems[J].Journal of Software,2006,17(12):2485-2498.
Authors:LUO Xiang-Yu  SU Kai-Le and YANG Jin-Ji
Abstract:
Keywords:model checking  bounded model checking  multi-Agent system  synchronous temporal epistemic model  temporal epistemic logic
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号