Model Checking Agent Dialogues in SPIN
Christopher Walton · 2004
The theory of Multi-Agent Systems (MAS) is typically concerned with a definition of the rational processes within the agents, or the communicative processes between agents. In this paper we are primarily interested in the latter, and in particular the problem of ensuring the correctness of communication. We address the problem by applying model checking techniques to protocols which express interactions between a group of agents in the form of a dialogue. We define a lightweight protocol language which can cleanly express a wide range of dialogues types, and we use the SPIN model checker to check the properties of this language.