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

Three Valued Model Checking on Modal Transition Systems

分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题·提出了把模态转移系统转换成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.