In most proposals for multi-agent systems, an Agent Communication Language (ACL) is the formalism designed to express knowledge exchange among agents. However, a universally accepted standard for ACLs is still missing. Among the different approaches to the definition of ACL semantics, the social approach seems the most appropriate to express semantics of communication in open societies of autonomous and heterogeneous agents.

In this paper we propose a formalism (deontic constraints) to express social ACL semantics, which can be grounded on a computational logic framework, thus allowing automatic verification of compliance by means of appropriate proof procedures. We also show how several common communication performatives can be defined by means of deontic constraints.

Agent communication is one of the key issues in multi-agent systems. Traditional interprocess communication formalisms are usually considered insufficient for this purpose because of their lack of expressiveness; thus, in most proposals for multi-agent architectures, an Agent Communication Language (ACL) is designed to provide for agent communication. However, a universally accepted standard for ACLs is still missing. Agent communication in open societies of heterogeneous agents poses requirements on ACLs semantics (formal syntax and semantics, declarativeness, verifiability, meaningfulness) which a social approach seems to meet best.

In this paper we propose a logic-based social approach for ACL semantics. We give a functional abstract model of societies and agents. Then we propose a formalism (deontic constraints) to express interaction protocols and give a social semantics to the behavior of agents, focusing on communicative acts. Finally, we sketch a prototypical implementation of deontic constraints exploiting the Constraint Handling Rules language.

In this paper we propose a logic-based social approach for specification and verification of agent interaction. We firstly introduce integrity constraints about social acts (called Social Integrity Constraints) as a formalism to express interaction protocols and give a social semantics to the behavior of agents, focusing on communicative acts. Then, we discuss several possible kinds of verification of agent interaction, and we show how social integrity constraints can be used to verify some properties in this respect. We focus our interest on static verification of the compliance of agent specifications to interaction protocols, and on run-time verification, based on agents' observable behavior. We adopt as a running example the NetBill security transaction protocol for the selling and delivery of information goods.

This work is about interactions among computees of a society, using a computational logic-based approach. Computees are abstractions of the entities that populate global and open computing environments. The society defines the allowed interaction protocols, which on their turn are defined by means of social integrity constraints. Using social integrity constraints, it is possible to give a formal definition of concepts such as violation, fulfillment, and social expectation. This allows for the automatic verification of the social behaviour of computees. In order to explain the ideas, we adopt as a running example a resource exchange scenario.

The focus of this work is on the interactions among (possibly heterogeneous) agents that form an open society, and on the definition of a computational logic-based architecture for agent interaction. We propose a model where the society defines the allowed interaction protocols, which determine the ``socially'' allowed agent interaction patterns. The semantics of protocols can be defined by means of social integrity constraints. The main advantages of this approach are in the design of societies of agents, and in the possibility to detect undesirable behavior. In the paper, we present the model for societies ruled by protocols expressed as integrity constraints, and its declarative semantics. A sketch of the operational counterpart is also given.

In open societies of agents, where agents are autonomous and heterogeneous, it is not realistic to assume that agents will always act so as to comply to interaction protocols. Thus, the need arises for a formalism to specify constraints on agent interaction, and for a tool able to observe and check for agent compliance to interaction protocols. In this paper we present a Java-Prolog software component which can be used to verify compliance of agent interaction to protocols written in a logic-based formalism (Social Integrity Constraints).

An important challenge posed by the design of open information systems concerns the choice of suitable methods to harness their complexity and to guarantee the correctness of their behaviour. In recent times, logic programming has been proposed as a powerful technology, formal and declarative, for the specification and verification of agent based and open systems. In this work, we focus on the interaction design. We base our approach on a logic-based formalism, which can be used to define the semantics of agent communication languages and interaction protocols. We advocate its use within a more general framework, drawing a design methodology which encompasses the specification of the interaction space and of its desired properties, and their verification.

This article summarises part of the work done during the first two years of the SOCS project, with respect to the task of modelling interaction amongst CL-based agents. It describes the SOCS social model: an agent interaction specification and verification framework equipped with a declarative and operational semantics, expressed in terms of abduction. The operational counterpart of the proposed framework has been implemented and integrated in SOCS-SI, a tool that can be used for on-the-fly verification of agent compliance with respect to specified protocols.

A number of approaches to agent society modeling can be found in the Multi-Agent Systems literature which exploit (variants of) Deontic Logic. In this paper, after briefly mentioning related approaches, we focus on the Computational Logic (CL) approach for society modeling developed within the UE IST-2001-32530 Project (named SOCS), where obligations and prohibitions are mapped into abducible predicates (respectively, positive and negative expectations), and norms ruling the behavior of members are represented as abductive integrity constraints. We discuss how this abductive framework can deal with Deontic Logic concepts, by introducing additional integrity constraints.

In this paper we present by a case study an approach to the verification of security protocols based on Abductive Logic Programming. We start from the perspective of open multi-agent systems, where the internal architecture of the individual system's components may not be completely specified, but it is important to infer and prove properties about the overall system behaviour. We take a formal approach based on Computational Logic, to address verification at two orthogonal levels: `static' verification of protocol properties (which can guarantee, at design time, that some properties are a logical consequence of the protocol), and `dynamic' verification of compliance of agent communication (which checks, at runtime, that the agents do actually follow the protocol). We adopt as a running example the well-known Needham-Schroeder protocol. We first show how the protocol can be specified in our previously developed SOCS-SI framework, and then demonstrate the two types of verification.

Combinatorial Auctions are an attractive application of intelligent agents; their applications are countless and are shown to provide good revenues. On the other hand, one of the issues they raise is the computational complexity of the solving process (the Winner Determination Problem, WDP), that delayed their practical use. Recently, efficient solvers have been applied to the WDP, so the framework starts to be viable.

A second issue, common to many agent systems, is trust: in order for an agent system to be used, the users must trust both their representative and the other agents inhabiting the society. Malicious agents must be found, and their violations discovered. The SOCS project addresses such issues, and provided a language, the social integrity constraints, for defining the allowed interaction moves, together with a proof-procedure able to detect violations.

In this paper we show how to write a protocol for combinatorial auctions by using social integrity constraints. In the devised protocol, the auctioneer interacts with an external solver for the winner determination problem. We also suggest some solutions for a further, challenging issue: defining a protocol that contains the concept of optimal allocation and checking efficiently that the allocation proposed by the auctioneer is indeed optimal.

The definition of the agent interaction space is one of the key aspects of multi-agent systems design. Agent interaction specification has several facets: syntax, semantics, conformance verification and proof of properties. In open societies, heterogenous agents can participate without showing any credentials. Access to their internals or their knowledge bases is typically not permitted, which makes it impossible to know a-priori whether or not agents will behave according to the society interaction rules. On the other hand, when specifying such rules, it is important to know what properties hold in the society when all agents comply with them. Social Integrity Constraints are the core element of a language proposed within the SOCS project as a means to define interactions in open societies. The proposed language and its abductive interpretation allows the designer to define open, extensible and not over-constrained protocols. Along with the definition language, the SCIFF proof-procedure and a software tool, named SOCS-SI, have been developed with the purposes of supporting execution-time verification of agent behaviour with respect to the defined protocols, and proof of protocol properties. In this tutorial we introduce the theory and the tools (in particular SOCS-SI) that can be used to design, define and test interaction protocols in open agent societies. An introduction to SOCS-SI is included in the paper 'Compliance Verification of Agent Interaction: a Logic-Based Tool'.

We propose an operational framework which builds on the classical understanding of abductive reasoning in logic programming, and extends it in several directions. The new features include the ability to reason with a dynamic knowledge base, where new facts can be added anytime, the ability to generate expectations about such new facts occurring in the future (forecasting), and the process of confirmation/disconfirmation of such expectations.

Combinatorial Auctions are an attractive application of intelligent agents; their applications are countless and are shown to provide good revenues. On the other hand, one of the issues they raise is the computational complexity of the solving process (the Winner Determination Problem, WDP), that delayed their practical use. Recently, efficient solvers have been applied to the WDP, so the framework starts to be viable. A second issue, common to many other agent systems, is trust: in order for an agent system to be used, the users must trust both their representative and the other agents inhabiting the society: malicious agents must be found, and their violations discovered. The SOCS project addresses such issues, and provided a language, the social integrity constraints, for defining the allowed interaction moves, together with a proof procedure able to detect violations. In this paper we show how to write a protocol for the combinatorial auctions by using social integrity constraints. In the devised protocol, the auctioneer interacts with an external solver for the winner determination problem.

The high computational cost of abduction has limited the application of this powerful and expressive formalism to practical cases. SCIFF is an abductive proof procedure used for verifying the compliance of agent behaviour to interaction protocols in multi-agent systems; SCIFF has been integrated in SOCS-SI, a system able to observe the agent interaction, pass it to SCIFF for the reasoning process and to display in a GUI the results of the SCIFF computation. In order to assess the applicability of SCIFF and SOCS-SI to practical cases, we have evaluated qualitatively and experimentally (not yet formally) their computational behaviour, as far as limitations and scalability. In this paper we show the results of the analysis.

Keywords: Abduction, Proof Procedure, Experimentation, Agent Interaction Verification