@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.}
}
@incollection{AlbGavLam06-IUS-BC,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Giovanni Sartor and Paolo Torroni},
title = {Un Sistema Basato su Logica Computazionale per il Trattamento degli Operatori Deontici},
booktitle = {La Gestione e la Negoziazione Automatica dei Diritti sulle Opere dell'Ingegno Digitali: Aspetti Giuridici e Informatici},
pages = {1--33},
publisher = {Gedit},
year = 2006,
editor = {Silvia Bisi and Claudio di Cocco},
chapter = 1,
address = {Bologna},
month = {October},
isbn = { 978-88-6027-015-3}
}
@inproceedings{AlbCheGav06-WSFM-IC,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and
Paola Mello and Marco Montali and Sergio Storari and Paolo Torroni},
title = {Computational Logic for Run-Time Verification of
Web Services Choreographies: exploiting the {SOCS-SI} tool},
booktitle = {Web Services and Formal Methods -
Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006 Proceedings},
year = {2006},
editor = {Mario Bravetti and Gianluigi Zavattaro},
publisher = {Springer-Verlag},
address = {Berlin/Heidelberg},
series = {Lecture Notes in Computer Science},
pages = {58-72},
issn = {0302-9743},
isbn = {3-540-38862-1},
volume = {4184},
doi = {10.1007/11841197_4},
url = {http://dx.doi.org/10.1007/11841197_4},
abstract = {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.}
}
@inproceedings{AlbCheGav06-ISMIS-IC,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello},
title = {A verifiable logic-based agent architecture},
booktitle = {Foundations of Intelligent Systems - 16th International
Symposium, ISMIS 2006 Bari, Italy, September 27-29,
2006 Proceedings},
year = {2006},
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
address = {Berlin Heidelberg},
issn = {0302-9743},
isbn = {3-540-45764-X},
volume = {4203},
pages = {188--197},
doi = {10.1007/11875604},
editor = {
Floriana Esposito and Zbigniew W. Ra\'{s} and Donato Malerba and Giovanni Semeraro},
url = {http://www.di.uniba.it/~ismis2006/},
abstract = {
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.}
}
@inproceedings{AlbCheGav06-ALPSWS-IW,
address = {Seattle, WA, USA},
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali and Paolo Torroni},
booktitle = {Proceedings of the 1st International Workshop on Applications of Logic Programming in the Semantic Web and Semantic Web Services (ALPSWS 2006)},
month = {August},
pages = {87--102},
series = {CEUR Workshop Proceedings},
title = {Policy-based reasoning for smart web service interaction},
volume = 196,
year = 2006,
issn = {1613-0073},
abstract = { 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.}
}
@inproceedings{AlbCheGav06-PPDP-IC,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali},
title = {An Abductive Framework for A-Priori Verification of Web Services},
booktitle = {Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy},
year = 2006,
editor = {Michael Maher},
publisher = {ACM Press},
month = jul,
url = {http://doi.acm.org/10.1145/1140335.1140342},
pages = {39--50},
isbn = {1-59593-388-3},
address = {New York, USA},
doi = {10.1.1.182.5574},
organization = {Association for Computing Machinery (ACM), Special Interest Group on
Programming Languages (SIGPLAN)},
abstract = {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 A$^l$LoWS (Abductive Logic
Web-service Specification). A$^l$LoWS comes with a language for
defining formally a choreography and a web service specification. As
its ancestor, A$^l$LoWS has a declarative and an operational
semantics. We show examples of how A$^l$LoWS deals correctly with
interaction patterns previously identified. Moreover, thanks to its
constraint-based semantics, A$^l$LoWS deals seamlessly with other
cases involving constraints and deadlines.}
}
@inproceedings{CheGavAlb06-CLIMA-IC,
author = {Federico Chesani and Marco Gavanelli and Marco Alberti and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Specification and Verification of Agent Interaction Using Abductive Reasoning},
booktitle = {CLIMA VI},
year = {2006},
editor = {Francesca Toni and Paolo Torroni},
series = {Lecture Notes on Artificial Intelligence},
publisher = {Springer-Verlag},
volume = {3900},
address = {Berlin Heidelberg},
pages = {243--264},
issn = {0302-9743},
isbn = {3-540-33996-5},
url = {http://dx.doi.org/10.1007/11750734_14},
abstract = {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.}
}
@inproceedings{AlbCheGav05-ESAW-IW,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Security protocols verification in Abductive Logic Programming: a case study},
booktitle = {Proceedings of 6th International Workshop "Engineering Societies in the Agents' World" (ESAW'05), October 26-28, 2005},
year = {2006},
series = {Lecture Notes on Artificial Intelligence},
publisher = {Springer-Verlag},
volume = {3963},
address = {Berlin Heidelberg},
editor = {O\u{g}uz Dikenelli and Marie-Pierre Gleizes and Alessandro Ricci },
organization = {Department of Computer Engineering Ege University},
url = {http://esaw05.ege.edu.tr/},
pages = {106-124},
abstract = {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.},
isbn = {3-540-34451-9},
issn = {0302-9743}
}
@inproceedings{AlbCheGav06-SWAP-IW,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali and Paolo Torroni},
title = {Policy-based Reasoning for Smart Web Service Interaction},
booktitle = {Proceedings of SWAP 2006, the 3rd Italian Semantic Web Workshop},
year = 2006,
editor = {Giovanni Tummarello and Paolo Bouquet and Oreste Signore},
address = {Pisa, Italy},
month = {December},
publisher = {CEUR Workshop Proceedings},
issn = {ISSN 1613-0073},
note = {available electronically at \url{http://ceur-ws.org/Vol-201}},
abstract = { 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 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.}
}
This file was generated by bibtex2html 1.98.