A number of information systems can be described as a set of interacting entities, which must follow interaction protocols. 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 present the application of the formalism and the system to the specification and verification of the FIPA Contract-Net protocol, and to the open-connection phase of the TCP protocol.
Specification and verification of agent interaction protocols in a logic-based system
ALBERTI, Marco;GAVANELLI, Marco;LAMMA, Evelina;
2007
Abstract
A number of information systems can be described as a set of interacting entities, which must follow interaction protocols. 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 present the application of the formalism and the system to the specification and verification of the FIPA Contract-Net protocol, and to the open-connection phase of the TCP protocol.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
