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