Informatics Report Series
Report
 EDI-INF-RR-0367
 Related Pages Report (by Number) Index Report (by Date) Index Author Index Institute Index Home
Title:Verifiable Agent Dialogues
Authors: Christopher Walton
Date: 2005
Publication Title:Journal of Applied Logic, Special Issue on Logic-Based Agent Verification
Publisher:Elsevier
Publication Type:Journal Article Publication Status:Pre-print
ISBN/ISSN:15708683
Abstract:
In this paper, we introduce the Multi-Agent Protocol (MAP) language which expresses dialogues in Multi-Agent Systems. MAP defines precisely the pattern of message exchange that occurs between the agents, though it is independent of the actual rational processes and message-content. This approach makes MAP applicable to a wide range of different agent architectures, e.g.\ reactive, proactive, and deductive agent systems. In the first half of the paper we specify the syntax of MAP, together with an operational semantics that defines an abstract implementation of the language. Our specification is derived from process calculus and thus forms a sound basis for the verification of our protocols. We also sketch a connection between MAP and temporal logic. In the latter half of the paper we define a translation from MAP into PROMELA, which is the specification language of the SPIN model checker. This translation allows us to prove properties of our protocols, such as termination, liveness, and correctness. The verification process is defined by $P \models \varphi$, where P is our translated agent protocol, and $\varphi$ is a linear temporal logic formula. By performing model checking on our protocols we can obtain a high degree of confidence in the resulting agent dialogues.