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

• 作者: 蒋颖 高建华
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 互模拟 函子 终余代数 最小Kripke结构
• 年，卷（期）: 2014,（1）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 16-26
• 页数: 11页
• 分类号: TP301
• 字数: 9871字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004408

摘要

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