Model Checking Multi-agent Systems

Abstract

In this paper, we consider a multi-agent system as a set of interacting objects. A model of object oriented automata, MOOA, is used to specify multi-agent systems. Under the framework of MOOA, each agent is modeled as an object oriented automaton. The formal syntax and semantics of MOOA are given in this paper. We first extend the PLTL logic so as to describe the dynamic properties of agents, then provide a model checking algorithm base on automata theory to verify the behaviors of MOOA model.