@article{AlbGavLam04-ENTCS-IJ,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Specification and Verification of Agent Interactions using Social Integrity Constraints},
journal = {Electronic Notes in Theoretical Computer Science},
year = 2004,
volume = 85,
number = 2,
month = {April},
publisher = {Elsevier},
pages = {94--116},
editor = {Wiebe van der Hoek and Alessio Lomuscio and Erik de Vink and Mike Wooldrige},
abstract = {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.},
url = {http://www1.elsevier.com/gej-ng/31/29/23/138/49/show/Products/notes/index.htt#003},
pdf = {http://www1.elsevier.com/gej-ng/31/29/23/138/49/25/85.2.003.pdf},
issn = {1571-0661}
}
@article{AlbGavLam05-TPLP-IJ,
key = 001,
author = {Marco Alberti And Marco Gavanelli And Evelina Lamma And Paola Mello And Michela Milano},
title = {A {CHR}-based implementation of known arc-consistency},
journal = {Theory and Practice of Logic Programming},
year = 2005,
volume = 5,
number = {4/5},
pages = {419-440},
month = jul,
http = {http://journals.cambridge.org/action/displayIssue?jid=TLP&volumeId=5&issueId=4-5},
doi = {http://dx.doi.org/10.1017/S147106840500236X},
abstract = { 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.},
issn = {1471-0684},
note = {IF: 1.372}
}
@article{AlbCheGav06-AAI-IJ,
key = 003,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Compliance Verification of Agent Interaction: a Logic-based Software Tool},
journal = {Applied Artificial Intelligence},
year = {2006},
volume = {20},
number = {2-4},
month = {February-April},
pages = {133--157},
doi = {10.1080/08839510500479546},
editor = {P. Petta and J.P. M{\"u}ller},
publisher = {Taylor & Francis},
abstract = {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.},
issn = {0883-9514},
note = {IF: 0.576}
}
@article{AlbGavLam06-CMOT-IJ,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Giovanni Sartor and Paolo Torroni},
title = {Mapping Deontic Operators to Abductive Expectations},
journal = {Computational and Mathematical Organization Theory},
year = {2006},
volume = {12},
number = {2--3},
month = oct,
pages = {205 - 225},
doi = {10.1007/s10588-006-9544-8},
url = {http://dx.doi.org/10.1007/s10588-006-9544-8},
issn = {1381-298X},
abstract = {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.}
}
@article{AlbCheDao07-SCPE-IJ,
author = {Marco Alberti and Federico Chesani and Davide Daolio and
Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo
Torroni},
title = {Specification and Verification of Agent Interaction Protocols
in a Logic-based System},
journal = {Scalable Computing: Practice and Experience},
year = 2007,
volume = 8,
number = 1,
pages = {1-13},
month = {March},
abstract = {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 \textit{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 (\textit{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).},
issn = {1895-1767}
}
@article{AlbCheGav08-TOCL-IJ,
key = 005,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Verifiable Agent Interaction in Abductive Logic Programming: the \emph{S}{CIFF} Framework},
journal = {ACM Transactions on Computational Logic (TOCL)},
year = 2008,
volume = 9,
number = 4,
issn = { 1529-3785},
abstract = {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.},
note = {IF: 2.766}
}
@article{AlbCheGav08-IJEC-IJ,
key = 004,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali and Paolo Torroni},
title = {Expressing and Verifying Business Contracts with Abductive Logic Programming},
journal = {International Journal of Electronic Commerce},
abstract = {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.
},
issn = {1086-4415},
doi = {10.2753/JEC1086-4415120401},
volume = 12,
number = 4,
pages = {9--38},
year = 2008,
month = {Summer},
keywords = {Abductive logic programming, business contracts, declarative specifications, g-SCIFF, SCIFF, runtime verification, static verification},
note = {IF: 1.366}
}
@article{AlbDalPer10-AMAI-IJ,
abstract = {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{\ae}. Finally, we discuss possible generalizations and extensions, and, in particular, how event detection can benefit from logic programming techniques.},
affiliation = {Centro de Intelig{\^e}ncia Artificial (CENTRIA), Departamento de Inform{\'a}tica, Faculdade de Ci{\^e}ncias e Tecnologia, Universidade Nova de Lisboa, Caparica, Portugal},
author = {Alberti, Marco and Dell'Acqua, Pierangelo and Pereira, Lu{\'\i}s Moniz},
issn = {1012-2443},
issue = {3},
journal = {Annals of Mathematics and Artificial Intelligence},
keyword = {Computer Science},
note = {10.1007/s10472-011-9259-5},
pages = {161-186},
publisher = {Springer Netherlands},
title = {Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation},
url = {http://dx.doi.org/10.1007/s10472-011-9259-5},
volume = {62},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.1007/s10472-011-9259-5}
}
@article{MonTorAlb10-FI-IJ,
title = {{Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business Processes}},
journal = {Fundamenta Informaticae},
year = {2010},
author = {Marco Montali and Paolo Torroni and Marco Alberti and Federico Chesani and Evelina Lamma and Paola Mello},
volume = {102},
number = {3-4},
pages = {325--361},
issn = {0169-2968},
note = {IF: 0.693},
doi = {10.3233/FI-2010-310},
abstract = {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.}
}
@article{AlbGavLam11-IA-IJ,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Fabrizio Riguzzi and Sergio Storari},
title = {Learning specifications of interaction protocols and business processes and proving their properties},
journal = {Intelligenza artificiale},
year = 2011,
volume = 5,
number = 1,
pages = {71--75},
month = feb,
doi = {10.3233/IA-2011-0006},
issn = {1724-8035},
abstract = {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.},
pdf = {http://ml.unife.it/wp-content/uploads/Papers/AlbGavLam-IA08.pdf}
}
@article{WheAlb11-MM-IJ,
abstract = {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.},
affiliation = {CENTRIA---Artificial Intelligence Center, Department of Computer Science, Universidade Nova de Lisboa, FCT/UNL, 2829-516 Caparica, Portugal},
author = {Wheeler, Gregory and Alberti, Marco},
issn = {0924-6495},
issue = {3},
journal = {Minds and Machines},
keyword = {Computer Science},
note = {10.1007/s11023-011-9243-1},
pages = {411-430},
publisher = {Springer Netherlands},
title = {NO Revision and NO Contraction},
url = {http://dx.doi.org/10.1007/s11023-011-9243-1},
volume = {21},
year = {2011},
bdsk-url-1 = {http://dx.doi.org/10.1007/s11023-011-9243-1}
}
@article{AlbCatChe11-IJWSR-IJ,
author = {Marco Alberti and Massimiliano Cattafi and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali and Paolo Torroni},
title = {A Computational Logic Application Framework for Service Discovery and Contracting},
journal = {International Journal of Web Services Research},
year = 2011,
volume = 8,
number = 3,
pages = {1--25},
abstract = {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.}
}
@article{BalGiu13-EMS-IJ,
author = {Stefano Balbi and
Carlo Giupponi and
Pascal Perez and
Marco Alberti},
title = {A spatial agent-based model for assessing strategies of adaptation
to climate and tourism demand changes in an alpine tourism destination},
journal = {Environmental Modelling and Software},
volume = {45},
pages = {29--51},
year = {2013},
url = {http://dx.doi.org/10.1016/j.envsoft.2012.10.004},
doi = {10.1016/j.envsoft.2012.10.004},
timestamp = {Mon, 24 Jun 2013 11:11:32 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/envsoft/BalbiGPA13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{AlbGavLam13-FI-IJ,
author = {Marco Alberti and
Marco Gavanelli and
Evelina Lamma},
title = {The CHR-based Implementation of the {SCIFF} Abductive System},
journal = {Fundam. Inform.},
volume = {124},
number = {4},
pages = {365--381},
year = {2013},
url = {http://dx.doi.org/10.3233/FI-2013-839},
doi = {10.3233/FI-2013-839},
timestamp = {Tue, 18 Jun 2013 15:03:39 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/fuin/AlbertiGL13},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{AlbBelCot17-IA-IJ,
author = {Marco Alberti and Elena Bellodi and Giuseppe Cota and
Fabrizio Riguzzi and Riccardo Zese},
title = {\texttt{cplint} on {SWISH}: Probabilistic Logical Inference with a Web Browser},
journal = {Intelligenza Artificiale},
publisher = {IOS Press},
copyright = {IOS Press},
year = {2017},
issn-print = {1724-8035},
issn-online = {2211-0097},
url = {http://ml.unife.it/wp-content/uploads/Papers/AlbBelCot-IA17.pdf},
abstract = {
\texttt{cplint} on SWISH is a web application that allows users to
perform reasoning tasks on probabilistic logic programs.
Both inference and learning systems can be performed: conditional probabilities with exact,
rejection sampling and Metropolis-Hasting methods. Moreover, the system now allows hybrid programs,
i.e., programs where some of the random variables are continuous. To perform inference on such programs likelihood weighting and particle filtering are used.
\texttt{cplint} on SWISH is also able to sample goals' arguments and
to graph the results. This paper reports on advances and new features
of \texttt{cplint} on SWISH, including the capability of drawing the
binary decision diagrams created during the inference processes.
},
keywords = { Logic Programming, Probabilistic Logic Programming,
Distribution Semantics, Logic Programs with Annotated Disjunctions, Web
Applications
},
volume = {11},
number = {1},
doi = {10.3233/IA-170106},
pages = {47--64},
wos = {WOS:000399736500004}
}
@article{GavAlbLam18-TOIT-IJ,
author = {Gavanelli, Marco and Alberti, Marco and Lamma, Evelina},
title = {Accountable Protocols in Abductive Logic Programming},
journal = {ACM Trans. Internet Technol.},
issue_date = {September 2018},
volume = {18},
number = {4},
month = apr,
year = {2018},
issn = {1533-5399},
pages = {46:1--46:20},
articleno = {46},
numpages = {20},
url = {http://doi.acm.org/10.1145/3107936},
doi = {10.1145/3107936},
acmid = {3107936},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {SCIFF, abductive logic programming, accountability}
}
@article{AlbGavLam20-FI-IJ,
author = {Marco Alberti and
Marco Gavanelli and
Evelina Lamma and
Fabrizio Riguzzi and
Ken Satoh and
Riccardo Zese},
title = {Dischargeable Obligations in the {SCIFF} Framework},
journal = {Fundamenta Informaticae},
volume = {176},
number = {3-4},
pages = {321--348},
year = {2020},
doi = {10.3233/FI-2020-1976},
publisher = {IOS Press}
}
@article{BelAlbRig20-TPLP-IJ,
author = {Elena Bellodi and Marco Alberti and Fabrizio Riguzzi and Riccardo Zese},
title = {{MAP} Inference for Probabilistic Logic Programming},
journal = {Theory and Practice of Logic Programming},
publisher = {Cambridge University Press},
copyright = {Cambridge University Press},
year = {2020},
url = {https://arxiv.org/abs/2008.01394},
volume = {20},
doi = {10.1017/S1471068420000174},
pdf = {https://arxiv.org/pdf/2008.01394.pdf},
number = {5},
pages = {641--655}
}
@article{RigBelZesAlbLam21-ML-IJ,
author = {Riguzzi, Fabrizio and Bellodi, Elena and Zese, Riccardo and Alberti, Marco and Lamma, Evelina},
title = {Probabilistic inductive constraint logic},
journal = {Machine Learning},
year = {2021},
volume = {110},
issue = {4},
pages = {723-754},
doi = {10.1007/s10994-020-05911-6},
pdf = {https://link.springer.com/content/pdf/10.1007/s10994-020-05911-6.pdf},
publisher = {Springer},
issn = {08856125},
abstract = {Probabilistic logical models deal effectively with uncertain relations and entities typical of many real world domains. In the field of probabilistic logic programming usually the aim is to learn these kinds of models to predict specific atoms or predicates of the domain, called target atoms/predicates. However, it might also be useful to learn classifiers for interpretations as a whole: to this end, we consider the models produced by the inductive constraint logic system, represented by sets of integrity constraints, and we propose a probabilistic version of them. Each integrity constraint is annotated with a probability, and the resulting probabilistic logical constraint model assigns a probability of being positive to interpretations. To learn both the structure and the parameters of such probabilistic models we propose the system PASCAL for “probabilistic inductive constraint logic”. Parameter learning can be performed using gradient descent or L-BFGS. PASCAL has been tested on 11 datasets and compared with a few statistical relational systems and a system that builds relational decision trees (TILDE): we demonstrate that this system achieves better or comparable results in terms of area under the precision–recall and receiver operating characteristic curves, in a comparable execution time.}
}
@article{FerGent2023-AWHM-IJ,
title = {Sex differences in schizophrenia-spectrum diagnoses: results from a 30-year health record registry},
author = {Ferrara, Maria and Curtarello, Eleonora Maria Alfonsina and Gentili, Elisabetta and Domenicano, Ilaria and Vecchioni, Ludovica and Zese, Riccardo and Alberti, Marco and Franchini, Giorgia and Sorio, Cristina and Benini, Lorenzo and others},
journal = {Archives of Women's Mental Health},
pages = {1--10},
year = {2023},
publisher = {Springer}
}
This file was generated by bibtex2html 1.98.