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

计算机科学 ›› 2006, Vol. 33 ›› Issue (3): 263-266.

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

郭建韩俊刚

西安电子科技大学,西安710071 西安邮电学院,西安710061

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
国家自然科学基金（90207015）.

GUO Jian　, HAN Jun-Gang　（1. Xidian University,Xi＇an 710071;2. Xi＇an Institute of Post and Telecommunications,Xi＇an 710071）

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

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

关键词: 三值逻辑模型检验不完全Kripke结构

Abstract: Model checking is one of the attracting methods in formal verification, but the main disadvantage of model checking is the state explosion that might occur if the system being verified becomes larger. This paper presents a method of abstracting a system a

Key words: 3-valued loglc,Model checking,Partial kripke structure

郭建韩俊刚. 基于不完全Kripke结构三值逻辑的模型检验[J]. 计算机科学, 2006, 33(3): 263-266. https://doi.org/

GUO Jian　, HAN Jun-Gang　（1. Xidian University,Xi＇an 710071;2. Xi＇an Institute of Post and Telecommunications,Xi＇an 710071）. [J]. Computer Science, 2006, 33(3): 263-266. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed