基于余归纳的最小Kripke结构的求解
文献类型：期刊论文
| 作者 | 高建华 ; 蒋颖 |
| 刊名 | 软件学报
 |
| 出版日期 | 2014 |
| 卷号 | 25期号:1页码:16-26 |
| 关键词 | 模型检测 互模拟 函子 终余代数 最小Kripke结构 |
| ISSN号 | 10009825 |
| 其他题名 | Coinduction-based solution for minimization of Kripke structure |
| 通讯作者 | Gao, J.-H.(gaojh@ios.ac.cn) |
| 中文摘要 | 状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：⑴对于任意给定的一类Kripke结构（记 为Kappa），在互模拟等价意义下Kappa中最小Kripke结构（记为Kappa_0）的存在唯一性。K0描述了Kappa中所有Kripke结构 的行为而且没有冗余的状态；(2)对于任意的MК（M可能包含无穷多个状态），在互模拟等价意义下的相对于（M且基于К_0）的最小Kripke结构（记 为КM）的存在唯一性.由此提出一种求解КM的算法，并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的КM代替M进行模型检测.该方法可 自然地推广到基于其他类型函子的余代数结构. |
| 英文摘要 | 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 K |
| 收录类别 | EI ; CSCD |
| 语种 | 中文 |
| CSCD记录号 | CSCD:5062354 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16766]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | 高建华,蒋颖. 基于余归纳的最小Kripke结构的求解[J]. 软件学报,2014,25(1):16-26. |
| APA | 高建华,&蒋颖.(2014).基于余归纳的最小Kripke结构的求解.软件学报,25(1),16-26. |
| MLA | 高建华,et al."基于余归纳的最小Kripke结构的求解".软件学报 25.1(2014):16-26. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。