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.