Model Checking Temporal Logic Of Knowledge And Its Applications

In the area of artificial intelligence and theoretical computer science,researchers have paid incremental attentions to the knowledge reasoning ofmulti-agent systems during the near ten years. They intended to use logic ofknowledge to formalize the knowledge properties of agents, and then verifyknowledge specifications of multi-agent systems with formal methods. Modelchecking as a fully developed technology caught researchers'eye, due to itsexcellent performance of verifying large-scale systems. However, this tempo-ral logic based technology was not conveniently applied to the verification ofknowledge logic specification. Thus, some experts combined these two logicsinto the temporal logic of knowledge, and then developed various methodsand tools for model checking it.In this thesis, we've first introduced some conceptions of model checkingand knowledge reasoning. Then we've mainly introduced my tutor's methodof model checking temporal logic of knowledge. Lastly, we've applied thismethod to two specific areas with our tool MCTK: one problem is to verifythe winning strategies in the zero-sum games, which is to automatically findout whether there exists a way ensuring the necessarily win of players; theother problem is to verify the knowledge based security protocols, whosesecure properties rely on the knowledge reasoning of the anticipants in theprotocol.