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

Symbolic Model Checking Algorithm for Temporal Epistemic Logic CTL*K

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

Temporal epistemic logics have been gradually used in specification of multiple agents system, which are composed by temporal logics and epistemic logics. Most of temporal epistemic logics are based on CTL, which have a limited expressivity. And some model checking techniques existing for them have problems such as memory-shortage and state explosion. A temporal epistemic logic CTL ＊ K based on CTL ＊ was proposed. Through the definition of syntax and se mantics,CTL ＊ K had a strong expressivity and could describe agents＇ epistemic properties such as belief and goal. To check CTL ＊ K, a symbolic model checking algorithm for CTL ＊ K was offered, which translated a CTL ＊ K formula into a common CTL ＊ formula and could be easily encoded into NuSMV model checker. The experiment showed that the algorithm could obviously enlarge the size of system to be checked.