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

ISCAS OpenIR

	基于余归纳的最小Kripke结构的求解
其他题名	Coinduction-based solution for minimization of Kripke structure
	高建华; 蒋颖; Gao, J.-H.(gaojh@ios.ac.cn)
	2014
发表期刊	软件学报
ISSN	10009825
卷号	25 期号:1 页码:16-26
摘要	状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：⑴对于任意给定的一类Kripke结构（记为Kappa），在互模拟等价意义下Kappa中最小Kripke结构（记为Kappa_0）的存在唯一性。K0描述了Kappa中所有Kripke结构的行为而且没有冗余的状态；(2)对于任意的MК（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于К_0）的最小Kripke结构（记为КM）的存在唯一性.由此提出一种求解КM的算法，并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的КM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.
收录类别	EI ; CSCD
其他摘要	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 Κ), 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∈Κ (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. © Copyright 2014, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
关键词	模型检测互模拟函子终余代数最小kripke结构
部门归属	高建华, 中国科学院软件研究所, 计算机科学国家重点实验室, 北京 100190, 中国. 蒋颖, 中国科学院软件研究所, 计算机科学国家重点实验室, 北京 100190, 中国.
语种	中文
CSCD记录号	CSCD:5062354
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16766
专题	中国科学院软件研究所
通讯作者	Gao, J.-H.(gaojh@ios.ac.cn)
推荐引用方式 GB/T 7714	高建华,蒋颖,Gao, J.-H.(gaojh@ios.ac.cn). 基于余归纳的最小Kripke结构的求解[J]. 软件学报,2014,25(1):16-26.
APA	高建华,蒋颖,&Gao, J.-H..(2014).基于余归纳的最小Kripke结构的求解.软件学报,25(1),16-26.
MLA	高建华,et al."基于余归纳的最小Kripke结构的求解".软件学报 25.1(2014):16-26.