In order to overcome the state explosion problem in model checking the probabilistic temporal logic of knowledge

a three-valued abstraction is proposed.Our work includes three parts:first the three-value semantics of the probabilistic temporal logic of knowledge is defined on the abstract model

and the initial abstract model is build according to the equivalence partition of state space

and the preservation of satisfaction under the abstraction is proved;second the model checking algorithm of the probabilistic temporal logic of knowledge is proposed;third how to refine the abstraction by the minimal witnesses and counterexamples generated in model checking is shown.Finally

the abstraction is applied in model checking the Dining Cryptographer protocols.