The Algorithm Research for "On the fly" Model Checking Temporal Logics of Knowledge in Multi-Agent Systems

Temporal logics of knowledge have been widely used in the distributed systems and expression for the specifications of protocols. The model checking for temporal logics of knowledge becomes a new and important research domain. In this paper, approaches for "on the fly " model checking the temporal logics of knowledge are discussed mainly. Based on the "on the fly" model checking approaches for temporal logics, according to automaton theory and the semantics of knowledge, "on the fly " model checking approaches for the temporal logics of knowledge are presented. These approaches make the model checking for the specifications with knowledge operators only need to construct a small portion of state space of the system before a counterexample is found, and so can avoid memory-shortage and state-explosion and realize "on the fly" model checking for the temporal logic of knowledge