Algorithm Research on “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 community and in the expression for the specifications of protocols. The model checking for temporal logics of knowledge becomes a new and important research domain. So approaches to the “on the fly” model checking the temporal logics of knowledge are discussed. Based on the “on the fly” model checking approaches for temporal logics, and according to automata theory and the semantics of knowledge, the “on the fly” model checking approaches to the temporal logics of knowledge are presented. These approaches, making the model checking for the specifications with knowledge operators, need only to construct a small portion of state space of system before a counterexample is found, and so avoid memory-shortage and state-explosion and realize “on the fly” model checking for the temporal logic of knowledge. And the time complexity of the algorithm is polynomial. Finally, the application to the verification of the TMN cryptographic protocol is illustrated to show the effectiveness of the approach.