主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
高建华,蒋颖.基于余归纳的最小Kripke结构的求解.软件学报,2014,25(1):16-26
基于余归纳的最小Kripke结构的求解
Coinduction-Based Solution for Minimization of Kripke Structures
投稿时间:2012-11-06  修订日期:2013-01-25
DOI:10.13328/j.cnki.jos.004408
中文关键词:  模型检测  互模拟  函子  终余代数  最小Kripke结构
英文关键词:model checking  bisimulation  functor  final coalgebra  minimal Kripke structure
基金项目:国家自然科学基金(60833001);中法NSFC-ANR共同资助合作研究项目(61161130530)
作者单位E-mail
高建华 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190
中国科学院大学, 北京 100190 
gaojh@ios.ac.cn 
蒋颖 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190  
摘要点击次数: 2548
全文下载次数: 2736
中文摘要:
      状态空间爆炸问题是模型检测的最大障碍.从余归纳(特别是余代数)的角度研究了这个问题.用余归纳的方法证明:(1) 对于任意给定的一类Kripke结构(记为K),在互模拟等价意义下K中最小Kripke结构(记为K0)的存在唯一性.K0描述了K中所有Kripke结构的行为而且没有冗余的状态;(2) 对于任意的MKM可能包含无穷多个状态),在互模拟等价意义下的相对于(M且基于K0)的最小Kripke结构(记为KM)的存在唯一性.由此提出一种求解KM的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的KM代替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 K), 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 MK (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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利