| 基于余归纳的最小Kripke结构的求解 |
| |
| 引用本文： | 高建华,蒋颖.基于余归纳的最小Kripke结构的求解[J].软件学报,2014,25(1):16-26. |
| |
| 作者姓名： | 高建华 蒋颖 |
| |
| 作者单位： | 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190 |
| |
| 基金项目： | 国家自然科学基金（60833001）；中法NSFC-ANR共同资助合作研究项目（61161130530） |
| |
| 摘 要： | 状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K），在互模拟等价意义下K中最小Kripke结构（记为K0）的存在唯一性.K0描述了K中所有Kripke结构的行为而且没有冗余的状态；（2） 对于任意的M∈K（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于K0）的最小Kripke结构（记为KM）的存在唯一性.由此提出一种求解KM的算法，并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的KM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.
|
| 关 键 词： | 模型检测 互模拟 函子 终余代数 最小Kripke结构 |
| 收稿时间： | 2012/11/6 0:00:00 |
| 修稿时间： | 2013/1/25 0:00:00 |
Coinduction-Based Solution for Minimization of Kripke Structures |
| |
| GAO Jian-Hua and JIANG Ying.Coinduction-Based Solution for Minimization of Kripke Structures[J].Journal of Software,2014,25(1):16-26. |
| |
| Authors: | GAO Jian-Hua and JIANG Ying |
| |
| Affiliation: | State Key Laboratory of Computer Science (Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China |
| |
| Abstract: | |
| |
| Keywords: | model checking bisimulation functor final coalgebra minimal Kripke structure |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
