Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Verifiable Agent Dialogues
Authors: Christopher Walton
Date: 2005
Publication Title:Journal of Applied Logic, Special Issue on Logic-Based Agent Verification
Publication Type:Journal Article Publication Status:Pre-print
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.
Links To Paper
No links available
Bibtex format
author = { Christopher Walton },
title = {Verifiable Agent Dialogues},
journal = {Journal of Applied Logic, Special Issue on Logic-Based Agent Verification},
publisher = {Elsevier},
year = 2005,

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh