Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic

Model checking is one of the attracting methods in formal verification,but the main disadvantage of model checking is the state explosion that might occur if the system being verified becomes larger.This paper presents a method of abstracting a system and setting up an incomplete state model,Partial Kripke Structure,upon which proper- ties of the system is verified.Under such a structure,a 3-valued interpretation to CTL logic formulae is given,with a third truth value unknown(⊥),which means“true or false unknown”.A 3-valued CTL model checking algorithm based on partial Kripke structure is also provided.Compared with 2-valued model checking technique,the algorithm does not increase the time complexity.At last some applications of 3-valued logic model checking are addressed.