Verifying the contract net protocol: a case study in interaction protocol and agent communication semantics
OA Location
Author(s)
Paurobally, S
Cunningham, J
Jennings, NR
Type
Conference Paper
Abstract
Multi-agent conversations are built upon two components: agent communication languages (ACLs) that specify the individual messages that can be exchanged and interaction protocols (IPs) that specify the sequences in which these message can be arranged. Although informative, the semantic definition proposed for the most standard ACL (FIPA 1997) is complicated and contentious, while published IPs tend to be ambiguous, incomplete, and unverified with respect to message semantics. As a case study to clarify and help rectify these problems, we have investigated verification of the contract net protocol when its messages are presumed to be expressed in FIPA ACL. In order to help both informal comprehension and formal verification we separate several concerns. We suggest a revised and simpler core semantics for many of the FIPA ACL speech acts, using the same belief-intention style of logic, although the underlying ideas are not dependent on this detail. An extended form of propositional dynamic logic and statecharts is used to express IPs. States are interpreted using mutual beliefs and intention, and properties such as termination and consistency of joint beliefs are shown.
Date Issued
2004
Citation
2004, pp.98-117
Start Page
98
End Page
117
Identifier
http://eprints.soton.ac.uk/259563/
Source
2nd International Workshop on Logic and Communication in Multi-Agent Systems
Notes
Event Dates: 2004
Publication Status
Unpublished