Model checking algorithm for temporal logics of knowledge in multi-agent systems

Model checking is used mainly to check if a system satisfies the specifications expressed in temporal logic and people pay little attention to the model checking problem for logics of knowledge. However, in the distributed systems community, the desirable specifications of systems and protocols are expressed widely in logics of knowledge. The model checking approaches for the temporal logic of knowledge are discussed. On the base of SMV (symbolic model verifier), according to the semantics of knowledge and set theory, several approaches for model checking of knowledge and common knowledge are presented. These approaches make SMV's functions extended from temporal logics to temporal logics of knowledge. They also correspond to other model checking approaches and tools where the output is the set of states.