一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。

A three-valued logic model checking approach based on extensional partial Kripke structure

Multi valued model checking is an important method to solve the state explosion problem in formal verification, and its basis is the three valued logic model checking. The challenge is how to obtain the value of uncertain states. We first propose a method to extend the partial Kripke structure (PKS), then present an approach for for obtaining the values of uncertain states based on the extended PKS, and finally design a three valued logic model checking algorithm. Compared with the existing three valued model checking algorithms, our algorithm reduces the complexity. Moreover, the proposed algorithm can improve the processing of uncertain or inconsistent information, and enhance the practicality of the three-valued logic model checking.