【摘要】 状态空间爆炸问题是模型检测的最大障碍.从余归纳(特别是余代数)的角度研究了这个问题.用余归纳的方法证明:(1)对于任意给定的一类Kripke结构(记为K),在互模拟等价意义下K中最小Kripke结构(记为K0)的存在唯一性.K0描述了K中所有Kripke结构的行为而且没有冗余的状态;(2)对于任意的M∈K(M可能包含无穷多个状态),在互模拟等价意义下的相对于(M且基于K0)的最小Kripke结构(记为KM)的存在唯一性.由此提出一种求解KM的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的KM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.更多还原

【Abstract】 State explosion problem is the main obstacle of model checking. This problem is addressed in the paper from a coalgebraic point of view. By coninduction principle, the paper proves that:(1) Given any class of Kripke Structures(denoted by K), there exists a unique smallest Kripke structure(denoted by K0) with respect to bisimilarity which describes all behaviors of the Kripke structures with no redundancy.(2) For any Kripke Structure M∈K(the state space of M may be infinite), there exists a unique concrete smallest Kripke structure KM. Base on this idea, an algorithm is established for minimization of Kripke Structures. A naive implementation of this algorithm is developed in Ocaml. One of its applications is that instead of M, KM can be used with a smaller state space to verify properties for M in the process of Model Checking.更多还原