Model Checking Agent Dialogues

In this paper we address the challenges associated with the verification of correctness of communication between agents in MultiAgent Systems. Our approach applies 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 express a wide range of dialogue types, and we use the SPIN model checker to verify properties of this language. Our early results show this approach has a high success rate in the detection of failures in agent dialogues.

• Type: Conference
• Year: 2004
• Where: DALT
• Authors: Christopher D. Walton
• Keywords: DALT 2004, Lightweight Protocol Language, Multiagent Systems, SPIN Model Checker