Specification and Verification of Agent Interaction Using Abductive Reasoning (Tutorial Paper).

Amongst several fundamental aspects in multi-agent systems design, the definition of the agent interaction space is of the utmost importance. The specification of the agent interaction has several facets: syntax, semantics, and compliance verification. In an open society, heterogenous agents can participate without showing any credentials. Accessing their internals or their knowledge bases is typically impossible, thus it is impossible to prove a priori that agents will indeed behave according to the society rules. Within the SOCS (Societies Of ComputeeS) project, a language based on abductive semantics has been proposed as a mean to define interactions in open societies. The proposed language allows the designer to define open, extensible and not over-constrained protocols. Beside the definition language, a software tool has been developed with the purpose of verifying at execution time if the agents behave correctly with respect to the defined protocols. This paper provides a tutorial overview of the theory and of the tools the SOCS project provided to design, define and test agent interaction protocols. [ABSTRACT FROM AUTHOR]