有界模型检测同步多智体系统的时态认知逻辑

• 作者: 杨晋吉 苏开乐 骆翔宇
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 有界模型检测 多智体系统 同步时态认知模型 时态认知逻辑
• 年，卷（期）: 2006,（12）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 2485-2498
• 页数: 14页
• 分类号: TP301
• 字数: 17806字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	中山大学计算机科学系	22	309	11.0	17.0
3	杨晋吉	中山大学计算机科学系	10	111	6.0	10.0