Pubblicazioni

Non-ISI journals

Marco Alberti, Marco Gavanelli, Evelina Lamma, Fabrizio Riguzzi, and Sergio Storari. Learning specifications of interaction protocols and business processes and proving their properties. Intelligenza artificiale, 5(1):71-75, February 2011.

In this paper we overview our recent research activity concerning the induction of Logic Programming specifications, and the proof of their properties via Abductive Logic Programming. Both the inductive and abductive tools here briefly described have been applied to respectively learn and verify (properties of) interaction protocols in multi-agent systems, Web service choreographies, careflows and business processes.

Marco Alberti, Federico Chesani, Davide Daolio, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Specification and verification of agent interaction protocols in a logic-based system. Scalable Computing: Practice and Experience, 8(1):1-13, March 2007.

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-CHR 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).

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, Giovanni Sartor, and Paolo Torroni. Mapping deontic operators to abductive expectations. Computational and Mathematical Organization Theory, 12(2-3):205 - 225, October 2006.

Deontic concepts and operators have been widely used in several fields where representation of norms is needed, including legal reasoning and normative multi-agent systems.

The EU-funded SOCS project has provided a language to specify the agent interaction in open multi-agent systems. The language is equipped with a declarative semantics based on abductive logic programming, and an operational semantics consisting of a (sound and complete) abductive proof procedure. In the SOCS framework, the specification is used directly as a program for the verification procedure.

In this paper, we propose a mapping of the usual deontic operators (obligations, prohibition, permission) to language entities, called expectations, available in the SOCS social framework. Although expectations and deontic operators can be quite different from a philosophical viewpoint, we support our mapping by showing a similarity between the abductive semantics for expectations and the Kripke semantics that can be given to deontic operators.

The main purpose of this work is to make the computational machinery from the SOCS social framework available for the specification and verification of systems by means of deontic operators.

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Specification and verification of agent interactions using social integrity constraints. Electronic Notes in Theoretical Computer Science, 85(2):94-116, April 2004.

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.