%0 Journal Article
%T 基于余归纳的最小kripke结构的求解
%A 高建华？
%A 蒋颖？
%J 软件学报
%P 16-26
%D 2014
%R 10.13328/j.cnki.jos.004408
%X 状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1）对于任意给定的一类kripke结构（记为k），在互模拟等价意义下k中最小kripke结构（记为k0）的存在唯一性.k0描述了k中所有kripke结构的行为而且没有冗余的状态；（2）对于任意的m∈k（m可能包含无穷多个状态），在互模拟等价意义下的相对于（m且基于k0）的最小kripke结构（记为km）的存在唯一性.由此提出一种求解km的算法，并用ocaml予以简单实现.其应用之一在于可以用状态空间更小的km代替m进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.
%K 模型检测
%K 互模拟
%K 函子
%K 终余代数
%K 最小kripke结构
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4408&flag=1