Verification that agent communication protocols have desirable properties or do not have undesirable properties is an important issue in agent systems where agents intend to communicate using such protocols. In this paper we explore the use of model checkers to verify properties of agent communication protocols, with these properties expressed as formulae in temporal logic. We illustrate our approach using a recentlyproposed protocol for agent dialogues over commands, a protocol that permits the agents to present questions, challenges and arguments for or against compliance with a command.
Katie Atkinson, Roderic A. Girle, Peter McBurney,