Specification and verification of agent interaction protocols in a logic-based system

Abstract

In multiagent systems, agent interaction is ruled by means of interaction protocols. Compliance to protocols can be hardwired in agent programs; however, this requires that only "certified" agents interact. In open societies, composed of autonomous and heterogeneous agents whose internal structure is, in general, not accessible, interaction protocols should be specified in terms of the agent observable behaviour, and compliance should be verified by an external entity.In this paper, we propose a Java-Prolog-CHR system for verification of compliance of agents' behaviour to protocols specified in a logic-based formalism (Social Integrity Constraints). We also present the application of the formalism and the system to the specification and verification of the FIPA Contract-Net protocol.