时态认知逻辑CTL*K的符号化模型检查算法

摘要：

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.

关键词：符号模型检测、多主体系统、时态认知逻辑

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

资助基金：863高技术计划基金项目2007AA01Z126;国防预研基金项目9140A06020206JB8101

在线出版日期：2009-06-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：214-219