Abstract:

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.

Key words: three-valued logic;model checking;extensional partial Kripke structure