| 模态转移系统的三值逻辑模型检验 |
| |
| 引用本文： | 郭建,韩俊刚.模态转移系统的三值逻辑模型检验[J].计算机辅助设计与图形学学报,2006,18(6):881-884. |
| |
| 作者姓名： | 郭建 韩俊刚 |
| |
| 作者单位： | 1. 西安电子科技大学微电子学院,西安,710071;西安邮电学院计算机科学系,西安,710061
2. 西安邮电学院计算机科学系,西安,710061 |
| |
| 摘 要： | 分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题.提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验.用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度.
|
| 关 键 词： | 三值逻辑 模型检验 模态转移系统 不完全Kripke结构 |
| 收稿时间： | 2005-03-03 |
| 修稿时间： | 2006-02-17 |
Three Valued Model Checking on Modal Transition Systems |
| |
| Guo Jian,Han Jungang.Three Valued Model Checking on Modal Transition Systems[J].Journal of Computer-Aided Design & Computer Graphics,2006,18(6):881-884. |
| |
| Authors: | Guo Jian Han Jungang |
| |
| Abstract: | Analysis is conducted on model checking for three valued logic formulae of modal transition system using existing model checking techniques. We reduce the three valued logic model checking problem for modal transition system to the two valued model checking problem under Kripke structure. This reduction is linear in the number of states, size of transition relations, and number of atomic propositional formulae in the new formed model compared with those in the original model. It does not increase the complexity of model checking under the Kripke structures. |
| |
| Keywords: | three valued logic model checking modal transition system partial Kripke structure |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
