模态转移系统的三值逻辑模型检验  

Three Valued Model Checking on Modal Transition Systems

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

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

出　　处：《计算机辅助设计与图形学学报》2006年第6期881-884,共4页Journal of Computer-Aided Design & Computer Graphics

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

摘　　要：分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题·提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验·用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度·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.

关 键 词：三值逻辑 模型检验 模态转移系统 不完全Kripke结构 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]