| 摘要: |
| 状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K），在互模拟等价意义下K中最小Kripke结构（记为K0）的存在唯一性.K0描述了K中所有Kripke结构的行为而且没有冗余的状态；（2） 对于任意的M∈K（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于K0）的最小Kripke结构（记为KM）的存在唯一性.由此提出一种求解KM的算法，并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的KM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构. |
| 关键词: 模型检测 互模拟 函子 终余代数 最小Kripke结构 |
| DOI：10.13328/j.cnki.jos.004408 |
| 分类号: |
| 基金项目:国家自然科学基金（60833001）；中法NSFC-ANR共同资助合作研究项目（61161130530） |
|
| Coinduction-Based Solution for Minimization of Kripke Structures |
|
GAO Jian-Hua1,2, JIANG Ying1
|
|
1.State Key Laboratory of Computer Science (Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China;2.University of Chinese Academy of Sciences, Beijing 100190, China
|
| Abstract: |
| State explosion problem is the main obstacle of model checking. This problem is addressed in the paper from a coalgebraic point of view. By coninduction principle, the paper proves that: (1) Given any class of Kripke Structures (denoted by K), there exists a unique smallest Kripke structure (denoted by K0) with respect to bisimilarity which describes all behaviors of the Kripke structures with no redundancy. (2) For any Kripke Structure M∈K (the state space of M may be infinite), there exists a unique concrete smallest Kripke structure KM. Base on this idea, an algorithm is established for minimization of Kripke Structures. A naive implementation of this algorithm is developed in Ocaml. One of its applications is that instead of M, KM can be used with a smaller state space to verify properties for M in the process of Model Checking. |
| Key words: model checking bisimulation functor final coalgebra minimal Kripke structure |
