| 基于不完全Kripke结构三值逻辑的模型检验 |
| |
| 引用本文： | 郭建,韩俊刚.基于不完全Kripke结构三值逻辑的模型检验[J].计算机科学,2006,33(3):263-266. |
| |
| 作者姓名： | 郭建 韩俊刚 |
| |
| 作者单位： | 1. 西安电子科技大学,西安,710071
2. 西安邮电学院,西安,710061 |
| |
| 摘 要： | 模型检验技术是形式化验证中比较成熟的技术，但随着设计系统规模的增加，状态爆炸已成为其发展的一个主要问题.为解决此问题，本文提出对系统进行抽象，建立不完全的状态模型，在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外，还出现了第三种情况：未知，即在这个状态模型下无法确定其真值，需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术，在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法，此算法与二值逻辑模型检验算法相比，没有带来时间复杂度的增加，最后给出了三值逻辑模型检验算法的应用.
|
| 关 键 词： | 三值逻辑 模型检验 不完全Kripke结构 |
Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic |
| |
| GUO Jian,HAN Jun-Gang.Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic[J].Computer Science,2006,33(3):263-266. |
| |
| Authors: | GUO Jian HAN Jun-Gang |
| |
| 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 |
| |
| Keywords: | 3-valued loglc Model checking Partial kripke structure |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
