Chinese Journal of Computers   Full Text
Title	Symbolic Model Checking Knowledge and Time in Multi-Agent System Via Extended Mu-Calculus
Authors	WU Li-Jun1) SU Jin-Shu1) SU Kai-Le2)
Address	1)(School of Computer Science, National University of Defense Technology, Changsha 410073) 2)(Department of Computer Science and Technology, Sun Yat-Sen University, Guangzhou 510275)
Year	2008
Issue	No.2(245—252)
Abstract &   Background	Abstract Clarke and McMillan presented symbolic approaches to model check temporal logics via mu-calculus and OBDDs. These approaches are very efficient and can be applied to verify many practical systems with extremely large state spaces in excess of 1020 states. However, these approaches cannot model check knowledge logics. But temporal logics of knowledge can describe more accurately the desirable specification of systems and protocols in distributed systems. In this paper, the symbolic approaches for model checking the temporal logic of knowledge via extended mu-calculus and OBDDs are discussed mainly. First the Kripke structure and mu-calculus are extended. Then the symbolic approaches for model checking temporal logics of knowledge via extended mu-calculus and OBDDs are presented. keywords OBDDs; mu-calculus; temporal logics of knowledge; symbolic model checking; protocol verification background Model checking has been used mainly to check if a system satisfies the specifications expressed in temporal logic. People pay little attention to the problem of model checking logics of knowledge. However, in the distributed systems, the desirable specifications of systems and protocols have been expressed widely in the temporal logics of knowledge. Temporal logics of knowledge can express more accurately the security properties of systems and protocols. Therefore, model checking temporal logics of knowledge is a new important research domain. But at present, people have not solved the state-explosion problem in domain of model checking temporal logics of knowledge. The paper, by extending the mu-calculus of Kozen and OBDDs, presents a efficient algorithm of symbolic model checking temporal logics of knowledge in multi-agent systems. The approaches can handle security verification of systems with extremely large state spaces an so solves state-explosion problem. The research is supported by Supported by the National Natural Science Foundation of China under grant Nos.90604006, 60496327 and German Research Foundation under grant No.446 CHV113/240/0-1. The mission of these projects is to research the model checking of knowledge logics and its application in network security. The work of this paper is encouraged by the background and considered as a significant part of the mission. The research group has written a series of high-quality papers in the domain published by some good journals and internal conferences. The work of this paper is to solve security verification of systems with extremely large state spaces.