论文部分内容阅读
状态空间爆炸问题是模型检测的最大障碍．从余归纳（特别是余代数）的角度研究了这个问题．用余归纳的方法证明：（1）对于任意给定的一类Kripke结构（记为K），在互模拟等价意义下庀中最小Kripke结构（it为‰）的存在唯一性．硒描述了足中所有Kripke结构的行为而且没有冗余的状态；（2）对于任意的MEK（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于Ko）的最小Kripke结构（记为KM）的存在唯一性．由此提出一种求解KM的算法，并用Ocaml予以简单实现．其应用之一在于可以用状态空间更小