Model Checking Multi-Agent Systems

Multi-agent systems are increasingly complex, and the problem of their verification and validation is ac-quiring increasing importance. In this paper we show how a well known and effective verification technique,model checking, can be generalized to deal with multi-agent systems. This paper explores a particular type of multi-agent system, in which each agent is viewed as having the three mental attitudes of belief (B), desire (D), and intention (I). We present a new approach to the verification of multi-agent systems, based on the use of possible-worlds framework to describe the system, a multi-modal branching-time logic BDICTL, with a semantics that is grounded in traditional decision theory, to specify the properties, and a decision procedure based on model checking technique. An imperative multi-agent programming language and a formal semantics for this language in terms of the BDICTL logic are used to specify multi-agent systems. The multi-agent program is used to systemically construct the agents state spaces. Then an automatic synthesis of these state spaces using the agents mental attitudes will generate the possible worlds structures. These possible worlds will be used by the adopted decision procedure to solve the problems of verification. A preliminary implementation of the approach shows promising results.