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

ISCAS OpenIR

	基于余归纳的最小Kripke结构的求解
Alternative Title	Coinduction-based solution for minimization of Kripke structure
	高建华; 蒋颖; Gao, J.-H.(gaojh@ios.ac.cn)
	2014
Source	软件学报
ISSN	10009825
Volume	25 Issue:1 Pages:16-26
English Abstract	状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：⑴对于任意给定的一类Kripke结构（记为Kappa），在互模拟等价意义下Kappa中最小Kripke结构（记为Kappa_0）的存在唯一性。K0描述了Kappa中所有Kripke结构的行为而且没有冗余的状态；(2)对于任意的MК（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于К_0）的最小Kripke结构（记为КM）的存在唯一性.由此提出一种求解КM的算法，并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的КM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.
Indexed Type	EI ; CSCD
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 Κ), 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.
Keyword	模型检测互模拟函子终余代数最小kripke结构
Department	高建华, 中国科学院软件研究所, 计算机科学国家重点实验室, 北京 100190, 中国. 蒋颖, 中国科学院软件研究所, 计算机科学国家重点实验室, 北京 100190, 中国.
Language	中文
CSCD ID	CSCD:5062354
Content Type	期刊论文
URI	http://ir.iscas.ac.cn/handle/311060/16766
Collection	中国科学院软件研究所
Corresponding Author	Gao, J.-H.(gaojh@ios.ac.cn)
Recommended Citation 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.

Files in This Item:
There are no files associated with this item.

If you have any objections to this item, please fill out the form below and the administrator will contact you as soon as possible.
Content:
Email：	*
Institution:
Verification Code:	Refresh

Any comments and suggestions are welcomed.
Title:	*
Content:
Email：	*
Verification Code:	Refresh

中国科学院软件研究所机构知识库