Pubblicazioni

ISI journals

Gregory Wheeler and Marco Alberti. No revision and no contraction. Minds and Machines, 21:411-430, 2011. 10.1007/s11023-011-9243-1.

One goal of normative multi-agent system theory is to formulate principles for normative system change that maintain the rule-like structure of norms and preserve links between norms and individual agent obligations. A central question raised by this problem is whether there is a framework for norm change that is at once specific enough to capture this rule-like behavior of norms, yet general enough to support a full battery of norm and obligation change operators. In this paper we propose an answer to this question by developing a bimodal logic for norms and obligations called NO . A key to our approach is that norms are treated as propositional formulas, and we provide some independent reasons for adopting this stance. Then we define norm change operations for a wide class of modal systems, including the class of NO systems, by constructing a class of modal revision operators that satisfy all the AGM postulates for revision, and constructing a class of modal contraction operators that satisfy all the AGM postulates for contraction. More generally, our approach yields an easily extendable framework within which to work out principles for a theory of normative system change.

Marco Alberti, Massimiliano Cattafi, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni. A computational logic application framework for service discovery and contracting. International Journal of Web Services Research, 8(3):1-25, 2011.

In Semantic Web technologies, searching for a service means identifying components that can potentially satisfy user needs in terms of inputs and outputs (discovery) and devise a fruitful interaction with the customer (contracting). In this paper, the authors present an application framework that encompasses both the discovery and the contracting steps in a unified search process. In particular, the authors accommodate service discovery by ontology-based reasoning and contracting by reasoning about behavioural interfaces, published in a formal language. To this purpose, the authors consider a formal approach grounded on Computational Logic. They define, illustrate, and evaluate a framework, called SCIFF Reasoning Engine (SRE), which can establish if a Semantic Web Service and a requester can fruitfully inter-operate, by computing a possible interaction plan based on the behavioural interfaces of both. The same operational machinery used for contracting can be used for runtime verification.

Marco Alberti, Pierangelo Dell'Acqua, and Luís Moniz Pereira. Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation. Annals of Mathematics and Artificial Intelligence, 62:161-186, 2011. 10.1007/s10472-011-9259-5.

Many applications (such as system and user monitoring, runtime verification, diagnosis, observation-based decision making, intention recognition) all require to detect the occurrence of an event in a system, which entails the ability to observe the system. Observation can be costly, so it makes sense to try and reduce the number of observations, without losing full certainty about the event's actual occurrence. In this paper, we propose a formalization of this problem. We formally show that, whenever the event to be detected follows a discrete spatial or temporal pattern, then it is possible to reduce the number of observations. We discuss exact and approximate algorithms to solve the problem, and provide an experimental evaluation of them. We apply the resulting algorithms to verification of linear temporal logics formulæ. Finally, we discuss possible generalizations and extensions, and, in particular, how event detection can benefit from logic programming techniques.

Marco Montali, Paolo Torroni, Marco Alberti, Federico Chesani, Evelina Lamma, and Paola Mello. Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business Processes. Fundamenta Informaticae, 102(3-4):325-361, 2010. IF: 0.693.

We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework's theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and it is guaranteed to terminate when applied to models that contain loops.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Verifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logic (TOCL), 9(4), 2008. IF: 2.766.

SCIFF is a framework thought to specify and verify interaction in open agent societies. The SCIFF language is equipped with a semantics based on abductive logic programming; SCIFF's operational component is a new abductive logic programming proof-procedure, also named SCIFF, for reasoning with expectations in dynamic environments. In this paper we present the declarative and operational semantics of the SCIFF language, the termination, soundness and completeness results of the SCIFF proof procedure, and we demonstrate SCIFF's possible application in the multi-agent domain.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni. Expressing and verifying business contracts with abductive logic programming. International Journal of Electronic Commerce, 12(4):9-38, Summer 2008. IF: 1.366.

In this article, we propose to adopt the SCIFF abductive logic language to specify business contracts, and show how its proof procedures are useful to verify contract execution and fulfilment. SCIFF is a declarative language based on abductive logic programming, which accommodates forward rules, predicate definitions, and constraints over finite domain variables. Its declarative semantics is abductive, and can be related to that of deontic operators; its operational specification is the sound and complete SCIFF proof procedure, defined as a set of transition rules, which has been implemented and integrated into a reasoning and verification tool. A variation of the SCIFF proof-procedure (g-SCIFF) can be used for static verification of contract properties. We demonstrate the use of the SCIFF language for business contract specification and verification, in a concrete scenario. In order to accommodate integration of SCIFF with architectures for business contract, we also propose an encoding of SCIFF contract rules in RuleML.

Keywords: Abductive logic programming, business contracts, declarative specifications, g-SCIFF, SCIFF, runtime verification, static verification.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Compliance verification of agent interaction: a logic-based software tool. Applied Artificial Intelligence, 20(2-4):133-157, February-April 2006. IF: 0.576.

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 built on logic programming technology, which can be used to verify compliance of agent interaction to protocols, and that has been integrated with the PROSOCS platform.

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. The SCIFF abductive proof-procedure. Lecture Notes in Artificial Intelligence, 3673:135-147, 2005. IF: 0.302.

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.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. The SOCS computational logic approach to the specification and verification of agent societies. Lecture Notes in Computer Science, 3267:314 - 339, February 2005. IF: 0.402.

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.

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Michela Milano. A CHR-based implementation of known arc-consistency. Theory and Practice of Logic Programming, 5(4/5):419-440, July 2005. IF: 1.372.

In classical CLP(FD) systems, domains of variables are completely known at the beginning of the constraint propagation process. However, in systems interacting with an external environment, this assumption may lead to waste of computation time, or even to obsolescence of the acquired data at the time of use.

For such cases, the Interactive Constraint Satisfaction Problem (ICSP) model has been proposed as an extension of the CSP model, to make it possible to start constraint propagation even when domains are not fully known, performing acquisition of domain elements only when necessary and without the need to restart propagation after every acquisition.

In this paper, we present a two sorted CLP language to express and solve ICSPs, and its implementation in the Constraint Handling Rules (CHR) language, a declarative language particularly suitable for high level implementation of constraint solvers.

Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Modeling interactions using social integrity constraints: a resource sharing case study. Lecture Notes in Artificial Intelligence, 2990:243-262, 2004. IF: 0.251.

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.