基于余归纳的最小kripke结构的求解

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