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

Files in This Item:

There are no files associated with this item.


Recommended Citation:
高建华,蒋颖. 基于余归纳的最小Kripke结构的求解[J]. 软件学报,2014-01-01,25(1):16-26.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[高建华]'s Articles
[蒋颖]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[高建华]‘s Articles
[蒋颖]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace