基于不完全Kripke结构三值逻辑的模型检验

郭建; 韩俊刚

首页> 中文期刊> 《计算机科学》 >基于不完全Kripke结构三值逻辑的模型检验

基于不完全Kripke结构三值逻辑的模型检验

开具论文收录证明 >>

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

文献代查 >>

页面导航

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

摘要

模型检验技术是形式化验证中比较成熟的技术,但随着设计系统规模的增加,状态爆炸已成为其发展的一个主要问题.为解决此问题,本文提出对系统进行抽象,建立不完全的状态模型,在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外,还出现了第三种情况:未知,即在这个状态模型下无法确定其真值,需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术,在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法,此算法与二值逻辑模型检验算法相比,没有带来时间复杂度的增加,最后给出了三值逻辑模型检验算法的应用.

著录项

来源
《计算机科学》 |2006年第3期|263-266278|共5页
作者
郭建; 韩俊刚;
展开▼
作者单位

西安电子科技大学;

西安;

710071;

西安邮电学院;

西安;

710061;

展开▼
原文格式 PDF
正文语种 chi
中图分类计算技术、计算机技术;
关键词
三值逻辑; 模型检验; 不完全Kripke结构;

相似文献

中文文献
外文文献
专利

1. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法 [J] . 刘姣 ,雷丽晖 . 计算机工程与科学 . 2015,第010期
2. 不确定型模糊Kripke结构的计算树逻辑模型检测 [J] . 范艳焕 ,李永明 ,潘海玉 . 电子学报 . 2018,第001期
3. 模态转移系统的三值逻辑模型检验 [J] . 郭建 ,韩俊刚 . 计算机辅助设计与图形学学报 . 2006,第006期
4. 基于余归纳的最小Kripke结构的求解 [J] . 高建华 ,蒋颖 . 软件学报 . 2014,第001期
5. 基于模糊逻辑的几类Kripke结构之间的关系 [J] . 潘海玉 ,张敏 ,陈仪香 . 计算机科学 . 2013,第005期
6. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法 [C] . LIU Jiao ,刘姣 ,LEI Li-hui . 2015全国理论计算机科学学术年会 . 2015
7. 带时间算子的Kripke模型 [A] . 郭良明 . 2009

基于不完全Kripke结构三值逻辑的模型检验

摘要

著录项

相似文献

相关主题

期刊订阅