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

高建华; 蒋颖

首页> 中文期刊> 《软件学报》 >基于余归纳的最小Kripke结构的求解

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

状态空间爆炸问题是模型检测的最大障碍.从余归纳(特别是余代数)的角度研究了这个问题.用余归纳的方法证明:(1)对于任意给定的一类Kripke结构(记为K),在互模拟等价意义下K中最小Kripke结构(记为Ko)的存在唯一性.Ko描述了K中所有Kripke结构的行为而且没有冗余的状态;(2)对于任意的M∈ K(M可能包含无穷多个状态),在互模拟等价意义下的相对于(M且基于K0)的最小Kripke结构(记为KM)的存在唯一性.由此提出一种求解KM的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的KM代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.

著录项

来源
《软件学报》 |2014年第1期|16-26|共11页
作者
高建华; 蒋颖;
展开▼
作者单位

计算机科学国家重点实验室(中国科学院软件研究所);

北京100190;

中国科学院大学;

北京 100190;

计算机科学国家重点实验室(中国科学院软件研究所);

北京100190;

展开▼
原文格式 PDF
正文语种 chi
中图分类理论、方法;
关键词
模型检测; 互模拟; 函子; 终余代数; 最小Kripke结构;

相似文献

中文文献
外文文献
专利

1. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法 [J] . 刘姣 ,雷丽晖 . 计算机工程与科学 . 2015,第010期
2. 基于模糊逻辑的几类Kripke结构之间的关系 [J] . 潘海玉 ,张敏 ,陈仪香 . 计算机科学 . 2013,第005期
3. 基于Kripke结构的程序正确性证明 [J] . 林杰 ,余建坤 . 计算机应用 . 2011,第005期
4. 基于不完全Kripke结构三值逻辑的模型检验 [J] . 郭建 ,韩俊刚 . 计算机科学 . 2006,第003期
5. 基于最大最小蚁群算法求解最小点覆盖问题 [J] . 吴佩雯 ,陈京荣 ,姬璐烨 . 兰州交通大学学报 . 2020,第002期
6. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法 [C] . LIU Jiao ,刘姣 ,LEI Li-hui . 2015全国理论计算机科学学术年会 . 2015
7. 基于能量损失率最小原理求解稳定渗流场渗流参数 [A] . 赵磊 . 2021

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

摘要

著录项

相似文献

相关主题

期刊订阅