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

Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic

作　　者：郭建[1] 韩俊刚[2] 

机构地区：[1]西安电子科技大学,西安710071 [2]西安邮电学院,西安710061

出　　处：《计算机科学》2006年第3期263-266,278,共5页Computer Science

基　　金：国家自然科学基金(90207015)

摘　　要：模型检验技术是形式化验证中比较成熟的技术,但随着设计系统规模的增加,状态爆炸已成为其发展的一个主要问题。为解决此问题,本文提出对系统进行抽象,建立不完全的状态模型,在此状态模型上来验证表示其属性的逻辑公式。这样一个逻辑公式的真值除了真、假外,还出现了第三种情况:未知,即在这个状态模型下无法确定其真值,需要更多的状态信息才能确定。本文还讨论了二值逻辑的模型检验技术,在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法,此算法与二值逻辑模型检验算法相比,没有带来时间复杂度的增加,最后给出了三值逻辑模型检验算法的应用。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 and setting up an incomplete state model, Partial Kripke Structure, upon which properties of the system is verified. Under such a structure, a 3-valued interpretation to CTL logic formulae is given, with a third truth value unknown（⊥）, which means ＂ true or false unknown＂. A 3-valued CTL model checking algorithm based on partial Kripke structure is also provided. Compared with 2-valued model checking technique, the algorithm does not increase the time complexity. At last some applications of 3-valued logic model checking are addressed.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论] TP311[自动化与计算机技术—计算机科学与技术]