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

作者：高建华; 蒋颖

来源：软件学报, 2014, 25(01): 16-26.

DOI：10.13328/j.cnki.jos.004408

• 模型检测
• 互模拟
• 函子
• 终余代数
• 最小Kripke结构

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

• 单位
  中国科学院大学; 计算机科学国家重点实验室; 中国科学院软件研究所