Specification and Verification of Agent Interaction Protocols in a Logic-based System

Abstract

A number of information systems can be described as a set of
interacting entities, which must follow interaction protocols. These
protocols determine the behaviour and the properties of the overall
system, hence it is of the uttermost importance that the entities
behave in a conformant manner.

A typical case is that of multi-agent systems, composed of a
plurality of agents without a centralized control. Compliance to
protocols can be hardwired in agent programs; however, this requires
that only certified agents interact. In open systems, composed
of autonomous and heterogeneous entities whose internal structure
is, in general, not accessible (open agent societies being, again, a
prominent example) interaction protocols should be specified in
terms of the observable behaviour, and compliance should be
verified by an external entity.

In this paper, we propose a Java-Prolog- system for
verification of compliance of computational entities to protocols
specified in a logic-based formalism (Social Integrity
Constraints). We also show the application of the formalism and the
system to the specification and verification of three different
scenarios: two specifications show the feasibility of our approach
in the context of Multi Agent Systems (FIPA Contract-Net Protocol
and Semi-Open societies), while a third specification applies to the
specification of a lower level protocol (Open-Connection phase of
the TCP protocol).