Pubblicazioni

International conferences

Marco Alberti, Ana Sofia Gomes, Ricardo Gonçalves, Matthias Knorr, João Leite, and Martin Slota. What if we don't know who they are? In Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent Systems, 2012. To appear.

Marco Alberti, Ana Sofia Gomes, Ricardo Gonçalves, João Leite, and Martin Slota. Normative systems represented as hybrid knowledge bases. In João Leite, Paolo Torroni, Thomas Ågotnes, Guido Boella, and Leon van der Torre, editors, Computational Logic in Multi-Agent Systems - 12th International Workshop, CLIMA XII, Barcelona, Spain, July 17-18, 2011. Proceedings, volume 6814 of Lecture Notes in Artificial Intelligence, pages 330-346. Springer Verlag, July 2011.

Normative systems have been advocated as an effective tool to regulate interaction in multi-agent systems.

Logic programming rules intuitively correspond to conditional norms, and their semantics is based on the closed world assumption, which allows default negation, often used in norms. However, there are cases where the closed world assumption is clearly not adequate, and others that require reasoning about unknown individuals, which is not possible in logic programming.

On the other hand, description logics are based on the open world assumption and support reasoning about unknown individuals, but do not support default negation.

In this paper, we demonstrate the need for the aforementioned features (closed and open world assumptions, and reasoning about unknown individuals) in order to model human laws, with examples from the Portuguese Penal Code. We advocate the use of hybrid knowledge bases combining rules and ontologies, which provide the joint expressivity of logic programming and description logics.

We define a normative scenario as the pair of a set of facts and a set of norms, and give it a formal semantics by translation into an MKNF knowledge base.

We describe the implementation of the language, which computes the relevant consequences of given facts and norms, and use it to establish the resulting sentence in a penal scenario.

Marco Alberti, Marco Gavanelli, and Evelina Lamma. Runtime addition of integrity constraints in abductive logic programs. In Manuel Hermenegildo and Torsten Schaub, editors, Technical Communications of the 26th International Conference on Logic Programming, volume 7 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4-13, Dagstuhl, Germany, July 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

Marco Alberti, Pierangelo Dell'Acqua, and Luís Moniz Pereira. Observation strategies for event detection, with incidence on runtime verification. In Marco Gavanelli and Toni Mancini, editors, RCRA-2010: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, volume 616 of CEUR Workshop Proceedings, Bologna, Italy, June 2010.

Marco Alberti, Massimiliano Cattafi, Marco Gavanelli, Evelina Lamma, Federico Chesani, Marco Montali, Paola Mello, and Paolo Torroni. Integrating abductive logic programming and description logics in a dynamic contracting architecture. In Paul Hofmann, editor, ICWS 2009: 2009 IEEE International Conference on Web Services, pages 254-261. IEEE Computer Society, IEEE Computer Society Press, 2009.

In Semantic Web technologies, searching for a service means to identify components that can potentially satisfy the user needs in terms of outputs and effects (discovery), and that, when invoked by the customer, can fruitfully interact with her (contracting). In this paper, we present an application framework that encompasses both the discovery and the contracting steps, in a unified search process. In particular, we accommodate service discovery by ontology-based reasoning, and contracting by reasoning about policies published in a formal language. To this purpose, we consider a formal approach grounded on Computational Logic, and Abductive Logic Programming in particular. We propose a framework, called SCIFF Reasoning Engine, able to establish, by ontological and abductive reasoning, if a semantic web service and a requester can fruitfully inter-operate, taking as input the behavioural interfaces of both the participants, and producing as output a sort of a contract.

Marco Gavanelli, Marco Alberti, and Evelina Lamma. Integration of abductive reasoning and constraint optimization in SCIFF. In Patricia M. Hill and David S. Warren, editors, 25th International Conference on Logic Programming (ICLP 2009), volume 5649 of Lecture Notes in Computer Science, pages 387-401, Berlin Heidelberg, 2009. Springer-Verlag.

Abductive Logic Programming (ALP) and Constraint Logic Programming (CLP) share the feature to constrain the set of possible solutions to a program via integrity or CLP constraints. These two frameworks have been merged in works by various authors, which developed efficient abductive proof-procedures empowered with constraint satisfaction techniques. However, while almost all CLP languages provide algorithms for finding an optimal solution with respect to some objective function (and not just any solution), the issue has received little attention in ALP.

In this paper we show how optimisation meta-predicates can be included in abductive proof-procedures, achieving in this way a significant improvement to research and practical applications of abductive reasoning.

In the paper, we give the declarative and operational semantics of an abductive proof-procedure that encloses constraint optimization meta-predicates, and we prove soundness in the three-valued completion semantics. In the proof-procedure, the abductive logic program can invoke optimisation meta-predicates, which can invoke abductive predicates, in a recursive way.

Keywords: Abductive Logic Programming, Constraint Logic Programming, Constraint Optimization, Constraint Handling Rules

Marco Montali, Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Verification from declarative specifications using logic programming. In Maria Garcia de la Banda and Enrico Pontelli, editors, Logic Programming, 24th International Conference, ICLP 2008, volume 5366 of Lecture Notes in Computer Science, pages 440-454. Springer-Verlag, 2008.

In recent years, the declarative programming philosophy has had a visible impact on new emerging disciplines, such as heterogeneous multi-agent systems and flexible business processes. We address the problem of formal verification for systems specified using declarative languages, focusing in particular on the Business Process Management field. We propose a verification method based on the g-SCIFF abductive logic programming proof procedure and evaluate our method empirically, by comparing its performance with that of other verification frameworks.

Keywords: Abductive Logic Programming, SCIFF, g-SCIFF, declarative specifications, formal verification, DecSerFlow, business process management

Marco Gavanelli, Marco Alberti, and Evelina Lamma. Integrating abduction and constraint optimization in constraint handling rules. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos Avouris, editors, ECAI 2008: 18th European Conference on Artificial Intelligence, pages 903-904. IOS press, July 2008.

Keywords: Abduction, Constraint Optimization, Logic and Constraint Programming, Logic Programming

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, Sergio Storari, and Paolo Torroni. A computational logic-based approach to verification of IT systems. In H.-G. Hegering, H. Reiser, M. Schiffers, and Th. Nebe, editors, Proceedings of the 14th Annual Workshop of HP Software University Association, Hosted by the Leibniz Computing Center and the Munich Network Management Team, July 8-11, 2007, pages 115-125, Stuttgart, Germany, July 2007. HP Software University Association, Infonomics-Consulting.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni. A rule-based approach for reasoning about collaboration between smart web services. In Massimo Marchiori, Jeff Z. Pan, and Christian de Sainte Marie, editors, Proceedings of the 1st International Conference on Web Reasoning and Rule Systems (RR), volume 4524 of Lecture Notes in Artificial Intelligence, pages 279-288, Innsbruck, June 2007. Springer-Verlag.

We present a vision of smart, goal-oriented web services that reason about other services’ policies and evaluate the possibility of future interactions. We assume web services whose behavioural interface is specified in terms of reactive rules. Such rules can be made public, in order for other web services to answer the following question: "is it possible to inter-operate with a given web service and achieve a given goal?". In this article we focus on the underlying reasoning process, and we propose a declarative and operational abductive logic programming based framework, called WAVe. We show how this framework can be used for a-priori verification of web services interaction.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni. Web service contracting: specification and reasoning with sciff. In Enrico Franconi, Michael Kifer, and Wolfgang May, editors, Proceedings of the 4th European Semantic Web Conference (ESWC), volume 4519 of Lecture Notes in Artificial Intelligence, pages 68-83, Innsbruck, June 2007. Springer-Verlag.

The semantic web vision will facilitate automation of many tasks, including the location and dynamic reconfiguration of web services. In this article, we are concerned with a specific stage of web service location, called, by some authors, contracting. We address contracting both at the operational level and at the semantic level. We present a framework encompassing communication and reasoning, in which web services exchange and evaluate goals and policies. Policies represent behavioural interfaces. The reasoning procedure at the core of the framework is based on the abductive logic programming SCIFF proof-procedure. We describe the framework, show by examples how to formalise policies in the declarative language of SCIFF, and give the framework a model-theoretic and a sound proof-theoretic semantics.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, Sergio Storari, and Paolo Torroni. Computational logic for run-time verification of web services choreographies: exploiting the SOCS-SI tool. In Mario Bravetti and Gianluigi Zavattaro, editors, Web Services and Formal Methods - Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006 Proceedings, volume 4184 of Lecture Notes in Computer Science, pages 58-72, Berlin/Heidelberg, 2006. Springer-Verlag.

In this work, we investigate the feasibility of using a framework based on computational logic, and mainly defined in the context of Multi-Agent Systems for Global Computing (SOCS UE Project), for modeling choreographies of Web Services with respect to the conversational aspect.

One of the fundamental motivations of using computational logic, beside its declarative and highly expressive nature, is given by its operational counterpart, that can provide a proof-theoretic framework able to verify the consistency of services designed in a cooperative ed incremental manner.

In particular, in this paper we show that suitable Social Integrity Constraints, introduced in the SOCS social model, can be used for specifying global protocols at the choreography level. In this way, we can use a suitable tool, derived from the proof-procedure defined in the context of the SOCS project, to check at run-time whether a set of existing services behave in a conformant manner w.r.t. the defined choreography.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, and Paola Mello. A verifiable logic-based agent architecture. In Floriana Esposito, Zbigniew W. Raś, Donato Malerba, and Giovanni Semeraro, editors, Foundations of Intelligent Systems - 16th International Symposium, ISMIS 2006 Bari, Italy, September 27-29, 2006 Proceedings, volume 4203 of Lecture Notes in Artificial Intelligence, pages 188-197, Berlin Heidelberg, 2006. Springer-Verlag.

In this paper, we present the SCIFF platform for multi-agent systems.

The platform is based on Abductive Logic Programming, with a uniform language for specifying agent policies and interaction protocols. A significant advantage of the computational logic foundation of the SCIFF framework is that the declarative specifications of agent policies and interaction protocols can be used directly, at runtime, as the programs for the agent instances and for the verification of compliance.

We also provide a definition of conformance of an agent policy to an interaction protocol (i.e., a property that guarantees that an agent will comply to a given protocol) and a operational procedure to test conformance.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni. Policy-based reasoning for smart web service interaction. In Proceedings of the 1st International Workshop on Applications of Logic Programming in the Semantic Web and Semantic Web Services (ALPSWS 2006), volume 196 of CEUR Workshop Proceedings, pages 87-102, Seattle, WA, USA, August 2006.

We present a vision of smart, goal-oriented web services that reason about other services' policies and evaluate the possibility of future interactions. To achieve our vision, we propose a proof theoretic approach. We assume web services whose interface behaviour is specified in terms of reactive rules. Such rules can be made public, in order for other web services to answer the following question: “is it possible to inter-operate with a given web service and achieve a given goal?” In this article we focus on the underlying reasoning process, and we propose a declarative and operational abductive logic programming-based framework, called WaVE.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Marco Montali. An abductive framework for a-priori verification of web services. In Michael Maher, editor, Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy, pages 39-50, New York, USA, July 2006. Association for Computing Machinery (ACM), Special Interest Group on Programming Languages (SIGPLAN), ACM Press.

Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user.

In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules; suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined.

Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies. We adapt the SCIFF framework for the new settings, and propose a heir of SCIFF, the framework AlLoWS (Abductive Logic Web-service Specification). AlLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, AlLoWS has a declarative and an operational semantics. We show examples of how AlLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, AlLoWS deals seamlessly with other cases involving constraints and deadlines.

Federico Chesani, Marco Gavanelli, Marco Alberti, Evelina Lamma, Paola Mello, and Paolo Torroni. Specification and verification of agent interaction using abductive reasoning. In Francesca Toni and Paolo Torroni, editors, CLIMA VI, volume 3900 of Lecture Notes on Artificial Intelligence, pages 243-264, Berlin Heidelberg, 2006. Springer-Verlag.

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.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Security protocols verification in abductive logic programming: a case study. In Oğuz Dikenelli, Marie-Pierre Gleizes, and Alessandro Ricci, editors, Proceedings of 6th International Workshop "Engineering Societies in the Agents' World" (ESAW'05), October 26-28, 2005, volume 3963 of Lecture Notes on Artificial Intelligence, pages 106-124, Berlin Heidelberg, 2006. Department of Computer Engineering Ege University, Springer-Verlag.

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.

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Abduction with hypotheses confirmation. In Fausto Giunchiglia, editor, IJCAI-05 Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pages 1545-1546, USA, 2005. Professional Book Center.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. A logic based approach to interaction design in open multi-agent systems. In Martin Fredriksson, Rune Gustavsson, Alessandro Ricci, and Andrea Omicini, editors, 13th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises (WET ICE 2004), pages 387-392, Washington, DC, USA, September 2004. IEEE Computer Society.

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.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Compliance verification of agent interaction: a logic-based tool. In Robert Trappl, editor, Proceedings of the 17th European Meeting on Cybernetics and Systems Research, Vol. II, Symposium “From Agent Theory to Agent Implementation” (AT2AI-4), pages 570-575, Vienna, Austria, April 13-16 2004. Austrian Society for Cybernetic Studies.

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

Marco Alberti, Davide Daolio, Paolo Torroni, Marco Gavanelli, Evelina Lamma, and Paola Mello. Specification and verification of agent interaction protocols in a logic-based system. In Hisham Haddad, Andrea Omicini, Roger L. Wainwright, and Lorie M. Liebrock, editors, Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14-17, 2004, pages 72-78, New York, NY, USA, 2004. ACM Press.

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.

Marco Alberti, Anna Ciampolini, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. A social ACL semantics by deontic constraints. In V.Marik, J.Muller, and M.Pechoucek, editors, Proceedings of the 3rd International/Central and Eastern European Conference on Multi-Agent Systems, number 2691 in Lecture Notes in Artificial Intelligence, pages 204-213, Prague, Czech Republic, June 2003.

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.

Marco Alberti and Evelina Lamma. Synthesis of object models from partial models: a CSP perspective. In Frank van Harmelen, editor, Proceedings of the Fifteenth European Conference on Artificial Intelligence (ECAI 2002), volume 77 of Frontiers in Artificial Intelligence and Applications, pages 116-120. IOS Press, July 2002.

In this work we present an approach for the synthesis of object models (expressed as Constraint Satisfaction Problems, CSPs) from views or partial models (expressed, in their turn, as CSPs as well).

The approach we propose is general enough to consider different types of features and relationships in the views. This is achieved by introducing the notion of model representation, where features, relationships and their domains are expressed. The (complete) model can be synthesized through a proper algorithm, which provides a albeling between the (complete) model and the partial models' components. The generated CSP representing the synthesized model must satisfy (or, better, entail) any constraint among features and any relationship occurring in each partial model.

The framework is applied for synthesizing object models (i.e., CSP descriptions). We provide two basic approaches for synthesizing a minimal or a correct model, and we experiment them by considering some case studies in artificial vision.