%0 Journal Article
%T 有界模型检测同步多智体系统的时态认知逻辑
%A 骆翔宇？
%A 苏开乐？
%A 杨晋吉？
%J 软件学报
%P 2485-2498
%D 2006
%X 提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(boundedmodelchecking,简称bmc)算法.基于同步解释系统语义,在时态逻辑ctl*的语言中引入认知模态词,从而得到一个新的时态认知逻辑eckln.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.eckln的时态认知表达能力强于另一个逻辑ctlk.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.
%K 模型检测
%K 有界模型检测
%K 多智体系统
%K 同步时态认知模型
%K 时态认知逻辑
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20061208&flag=1