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

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