Three Valued Model Checking on Modal Transition Systems

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.