@INPROCEEDINGS{CEEMAS03,
AUTHOR = {Marco Alberti and Anna Ciampolini and
Marco Gavanelli and Evelina Lamma and Paola
Mello and Paolo Torroni},
TITLE = {A Social {ACL} Semantics by Deontic Constraints},
BOOKTITLE = {Multi-Agent Systems and Applications III. 3rd International Central and Eastern European Conference on Multi-Agent Systems
CEEMAS 2003},
YEAR = {2003},
EDITOR = {Vladimir Marik and J{\"o}rg M{\"u}ller and Michal Pechoucek},
VOLUME = {2691},
SERIES = {Lecture Notes in Artificial Intelligence},
PAGES = {204--213},
ADDRESS = {Prague, Czech Republic},
MONTH = JUN # { 16-–18},
PUBLISHER = {Springer Verlag},
ABSTRACT = {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.},
URL = {http://gerstner.felk.cvut.cz/ceemas2003/}
}
@INPROCEEDINGS{FAMAS03,
AUTHOR = {Marco Alberti and Anna Ciampolini and
Marco Gavanelli and Evelina Lamma and Paola
Mello and Paolo Torroni},
TITLE = {Logic Based Semantics for an Agent Communication Language},
BOOKTITLE = {FAMAS'03 - Formal Approaches to Multi-Agent Systems},
YEAR = {2003},
EDITOR = {Barbara Dunin-K\c{e}plicz and Rineke Verbrugge},
ADDRESS = {Warsaw, Poland},
MONTH = APR # { 5 -- 13},
PAGES = {21--36},
ABSTRACT = {Agent communication is one of the key issues in multi-agent systems.
Traditional interprocess communication formalisms are usually
considered insufficient for this purpose because of their lack of
expressiveness; thus, in most proposals for multi-agent
architectures, an Agent Communication Language (ACL) is designed to
provide for agent communication. However, a universally accepted
standard for ACLs is still missing. Agent communication in open
societies of heterogeneous agents poses requirements on ACLs
semantics (formal syntax and semantics, declarativeness,
verifiability, meaningfulness) which a social approach
seems to meet best.
In this paper we propose a logic-based social approach for ACL
semantics. We give a functional abstract model of societies and
agents. Then we propose a formalism (deontic constraints) to express
interaction protocols and give a social semantics to the behavior of
agents, focusing on communicative acts. Finally, we sketch a
prototypical implementation of deontic constraints exploiting the
Constraint Handling Rules language.},
URL = {http://www.ai.rug.nl/conf/famas/},
PS = {http://www.lia.deis.unibo.it/research/TechReport/lia03001.ps}
}
@ARTICLE{ENTCS-LCMAS,
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},
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}
}
@INPROCEEDINGS{DALT03,
AUTHOR = {Marco Alberti and Marco Gavanelli and
Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {Modeling interactions using social integrity constraints: a resource sharing case study},
BOOKTITLE = {Declarative Agent Languages and Technologies, First International
Workshop, DALT 2003, Melbourne, Australia, July 15, 2003, Revised
Selected and Invited Papers},
YEAR = {2004},
EDITOR = {Jo{\~a}o Alexandre Leite and Andrea Omicini and Leon Sterling and Paolo Torroni},
ADDRESS = {Melbourne, Australia},
PUBLISHER = {Springer Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2990},
ISBN = {3-540-22124-7},
PAGES = {243-262},
ABSTRACT = {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.},
URL = {http://www.springeronline.com/sgw/cda/frontpage/0,10735,5-0-22-31054059-0,00.html?referer=www.springer.de/cgi/svcat/search_book.pl?isbn=3-540-22124-7},
PDF = {http://centria.di.fct.unl.pt/~jleite/dalt03/papers/16.pdf}
}
@INPROCEEDINGS{AIIA03,
AUTHOR = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {An Abductive Interpretation for Open Societies},
BOOKTITLE = {AI*IA 2003: Advances in Artificial Intelligence},
YEAR = {2003},
VOLUME = {2829},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Pisa, Italy},
MONTH = SEP # { 23-26},
PUBLISHER = {Springer Verlag},
PAGES = {287-299},
URL = {http://www-aiia2003.di.unipi.it},
EDITOR = {A. Cappelli and F. Turini},
ABSTRACT = {The focus of this work is on the interactions among (possibly
heterogeneous) agents that form an open society, and on the
definition of a computational logic-based architecture for agent
interaction. We propose a model where the society defines the
allowed interaction protocols, which determine the ``socially''
allowed agent interaction patterns. The semantics of protocols can
be defined by means of social integrity constraints. The main
advantages of this approach are in the design of societies of
agents, and in the possibility to detect undesirable behavior. In
the paper, we present the model for societies ruled by protocols
expressed as integrity constraints, and its declarative semantics. A
sketch of the operational counterpart is also given.}
}
@INPROCEEDINGS{AT2AI-4,
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 Tool},
YEAR = 2004,
MONTH = APR # {~13-16},
BOOKTITLE = {Proceedings of the 17th European Meeting on Cybernetics and Systems Research, Vol. II, Symposium ``From Agent Theory to Agent Implementation'' (AT2AI-4)},
ADDRESS = {Vienna, Austria},
PAGES = {570--575},
PUBLISHER = {{A}ustrian {S}ociety for {C}ybernetic {S}tudies},
ISBN = {3 85206 169 5},
EDITOR = {Robert Trappl},
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 which can
be used to verify compliance of agent interaction to
protocols written in a logic-based formalism (Social
Integrity Constraints).},
URL = {http://www.ai.univie.ac.at/~paolo/conf/at2ai4/}
}
@INPROCEEDINGS{TAPOCS04,
AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni },
TITLE = {A logic based approach to interaction design in open multi-agent systems},
BOOKTITLE = {13th {IEEE} International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises ({WET ICE} 2004)},
YEAR = {2004},
EDITOR = {Martin Fredriksson and Rune Gustavsson and Alessandro Ricci and Andrea Omicini},
PUBLISHER = {IEEE Computer Society},
ADDRESS = {Washington, DC, USA},
ISBN = {0-7695-2183-5},
PAGES = {387-392},
DOI = {http://dx.doi.org/10.1109/ENABL.2004.3},
MONTH = SEP,
ABSTRACT = {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.},
URL = {http://www.computer.org/cspress/CATALOG/p2183.htm},
PDF = {http://www-lia.deis.unibo.it/~pt/Publications/tapocs04.pdf}
}
@INPROCEEDINGS{GC,
AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {The {SOCS} Computational Logic Approach to the Specification and Verification of Agent Societies},
BOOKTITLE = {Global Computing: {IST/FET} International Workshop, GC 2004 Rovereto, Italy, March 9-12, 2004 Revised Selected Papers},
YEAR = {2005},
ISBN = {3-540-24101-9},
ISSN = {0302-9743},
MONTH = FEB,
EDITOR = {Corrado Priami and Paola Quaglia},
SERIES = {Lecture Notes in Computer Science},
DOI = {10.1007/b103251},
PUBLISHER = {Springer Verlag},
ADDRESS = {Berlin, Germany},
ABSTRACT = {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.},
URL = {http://springerlink.metapress.com/link.asp?id=p56klftvjr9egx8p},
PAGES = {314 - 339},
VOLUME = 3267
}
@INPROCEEDINGS{NorMAS,
AUTHOR = {Marco Alberti and Evelina Lamma and Marco Gavanelli and Paola Mello and Giovanni Sartor and Paolo Torroni},
TITLE = {Mapping Deontic Operators to Abductive Expectations},
BOOKTITLE = {Proceedings of the Symposium on Normative Multi-Agent Systems},
YEAR = {2005},
MONTH = APR # { 12-15},
URL = {http://normas.di.unito.it/zope/aisb05/},
PDF = {http://normas.di.unito.it//zope/aisb05/papers/alberti},
ISBN = {1 902956 47 6},
PUBLISHER = {The Society for the study of Artificial Intelligence and the Simulation of Behaviour},
ADDRESS = {University of Hertfordshire, Hatfield, UK},
PAGES = {126--136},
ABSTRACT = {A number of approaches to agent society modeling can be found in the Multi-Agent Systems literature
which exploit (variants of) Deontic Logic. In this paper, after briefly mentioning related approaches,
we focus on the Computational Logic (CL) approach for society modeling developed within the UE
IST-2001-32530 Project (named SOCS), where obligations and prohibitions are mapped into abducible
predicates (respectively, positive and negative expectations), and norms ruling the behavior of members
are represented as abductive integrity constraints. We discuss how this abductive framework can deal
with Deontic Logic concepts, by introducing additional integrity constraints.}
}
@INPROCEEDINGS{IJCAI05-poster,
AUTHOR = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {Abduction with hypotheses confirmation},
BOOKTITLE = {IJCAI-05 Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence},
YEAR = {2005},
EDITOR = {Fausto Giunchiglia},
PAGES = {1545--1546},
PUBLISHER = {Professional Book Center},
ADDRESS = {USA},
ISBN = {0-938075-93-4},
URL = {http://www.ing.unife.it/docenti/MarcoGavanelli/publications/poster-ijcai05.ppt}
}
@INPROCEEDINGS{ESAW05,
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 ESAW'05},
YEAR = {2005},
EDITOR = {O\u{g}uz Dikenelli and Marie-Pierre Gleizes and Alessandro Ricci },
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Berlin, Germany},
ORGANIZATION = {Department of Computer Engineering Ege University},
PUBLISHER = {Springer Verlag},
NOTE = {to appear},
URL = {http://esaw05.ege.edu.tr/},
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.}
}
@INPROCEEDINGS{wlp05-auctions,
AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Alessio Guerri and Evelina Lamma and Michela Milano and Paolo Torroni},
TITLE = {Expressing Interaction in Combinatorial Auction through Social Integrity Constraints},
PAGES = {53--64},
ABSTRACT = {Combinatorial Auctions are an attractive application of
intelligent agents; their applications are countless and are shown
to provide good revenues. On the other hand, one of the issues
they raise is the computational complexity of the solving process
(the Winner Determination Problem, WDP), that delayed their
practical use. Recently, efficient solvers have been applied to
the WDP, so the framework starts to be viable.
A second issue, common to many agent systems, is trust: in
order for an agent system to be used, the users must trust
both their representative and the other agents inhabiting the
society. Malicious agents must be found, and their violations
discovered. The SOCS project addresses such issues, and provided a
language, the social integrity constraints, for defining the
allowed interaction moves, together with a proof-procedure able to
detect violations.
In this paper we show how to write a protocol for combinatorial
auctions by using social integrity constraints. In the devised
protocol, the auctioneer interacts with an external solver for the
winner determination problem. We also suggest some solutions for a
further, challenging issue: defining a protocol that contains the
concept of optimal allocation and checking efficiently that
the allocation proposed by the auctioneer is indeed optimal.},
BOOKTITLE = {19th Workshop on (Constraint) Logic Programming, Ulm, Germany, February 21-23, 2005},
YEAR = {2005},
EDITOR = {Armin Wolf and Thom Fr{\"u}hwirth and Marc Meister},
ADDRESS = {University of Ulm, Germany},
MONTH = FEB,
NUMBER = {2005-01},
SERIES = {Ulmer Informatik-Berichte},
ISSN = {0939-5091},
URL = {http://www.informatik.uni-ulm.de/epin/pw/11541},
PDF = {http://www.informatik.uni-ulm.de/epin-data/user/11541.218,UIB_2005-01.pdf}
}
@INPROCEEDINGS{wlp05-sciff,
AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma},
TITLE = {The {CHR}-based Implementation of a System for Generation and Confirmation of Hypotheses},
PAGES = {111-122},
BOOKTITLE = {19th Workshop on (Constraint) Logic Programming, Ulm, Germany, February 21-23, 2005},
YEAR = {2005},
EDITOR = {Armin Wolf and Thom Fr{\"u}hwirth and Marc Meister},
ADDRESS = {University of Ulm, Germany},
MONTH = FEB,
NUMBER = {2005-01},
SERIES = {Ulmer Informatik-Berichte},
ISSN = {0939-5091},
URL = {http://www.informatik.uni-ulm.de/epin/pw/11541},
PDF = {http://www.informatik.uni-ulm.de/epin-data/user/11541.218,UIB_2005-01.pdf}
}
@INPROCEEDINGS{CLIMA-VI-tutorial,
AUTHOR = {Federico Chesani and Marco Gavanelli},
TITLE = {Specification and Verification of Agent Interaction using {SOCS-SI}},
BOOKTITLE = {Pre-proceedings of the $6^{th}$ International workshop on Computational Logic in Multi-agent Systems. CLIMA-VI},
YEAR = {2005},
EDITOR = {Francesca Toni and Paolo Torroni},
PAGES = {6},
ADDRESS = {London, UK},
MONTH = {June},
ORGANIZATION = {City University},
ABSTRACT = {The definition of the agent interaction space is one of the key aspects of multi-agent systems design. Agent interaction specification has several facets: syntax, semantics, conformance verification and proof of properties. In open societies, heterogenous agents can participate without showing any credentials. Access to their internals or their knowledge bases is typically not permitted, which makes it impossible to know a-priori whether or not agents will behave according to the society interaction rules. On the other hand, when specifying such rules, it is important to know what properties hold in the society when all agents comply with them.
Social Integrity Constraints are the core element of a language proposed within the SOCS project as a means to define interactions in open societies. The proposed language and its abductive interpretation allows the designer to define open, extensible and not over-constrained protocols. Along with the definition language, the SCIFF proof-procedure and a software tool, named SOCS-SI, have been developed with the purposes of supporting execution-time verification of agent behaviour with respect to the defined protocols, and proof of protocol properties.
In this tutorial we introduce the theory and the tools (in particular SOCS-SI) that can be used to design, define and test interaction protocols in open agent societies. An introduction to SOCS-SI is included in the paper 'Compliance Verification of Agent Interaction: a Logic-Based Tool'.},
URL = {http://clima.deis.unibo.it/tutorials.html}
}
@INPROCEEDINGS{AIIA05,
AUTHOR = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {The \textit{S}{CIFF} abductive proof-procedure},
BOOKTITLE = {AI*IA 2005: Advances in Artificial Intelligence: 9th Congress of the Italian Association for Artificial Intelligence, Milan, Italy, September 21-32, 2005. Proceedings},
YEAR = {2005},
EDITOR = {Stefania Bandini and Sara Manzoni},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Berlin},
PUBLISHER = {Springer Verlag},
PAGES = {135-147},
VOLUME = {3673},
ISBN = {3-540-29041-9},
ISSN = {0302-9743},
ABSTRACT = {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.},
URL = {http://dx.doi.org/10.1007/11558590_14}
}
@ARTICLE{AEV04_auctions_riv,
AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Alessio Guerri and Evelina Lamma and Paola Mello and Paolo Torroni},
TITLE = {Expressing Interaction in Combinatorial Auction through Social Integrity Constraints},
JOURNAL = {Intelligenza Artificiale},
YEAR = {2005},
PAGES = {22--29},
VOLUME = {{II}},
NUMBER = {1},
ABSTRACT = {Combinatorial Auctions are an attractive
application of intelligent agents; their applications are
countless and are shown to provide good revenues. On the other
hand, one of the issues they raise is the computational complexity
of the solving process (the Winner Determination Problem, WDP),
that delayed their practical use. Recently, efficient solvers have
been applied to the WDP, so the framework starts to be viable.
%
A second issue, common to many other agent systems, is {\em
trust}: in order for an agent system to be used, the users must
{\em trust} both their representative and the other agents
inhabiting the society: malicious agents must be found, and their
violations discovered. The SOCS project addresses such issues, and
provided a language, the social integrity constraints, for
defining the allowed interaction moves, together with a proof
procedure able to detect violations.
%
In this paper we show how to write a protocol for the
combinatorial auctions by using social integrity constraints. In
the devised protocol, the auctioneer interacts with an external
solver for the winner determination problem.},
ISSN = {1724-8035},
URL = {http://ia.di.uniba.it/}
}
@INPROCEEDINGS{AlbertiChesani,
AUTHOR = {Marco Alberti and Federico Chesani},
TITLE = {The computational behaviour of the {SCIFF} abductive proof procedure and the {SOCS-SI} system},
PDF = {http://www.ing.unife.it/eventi/rcra05/articoli/AlbertiChesani.pdf},
PAGES = {77--84},
KEYWORDS = {Abduction, Proof Procedure, Experimentation, Agent Interaction Verification},
ABSTRACT = {The high computational cost of abduction has limited the application
of this powerful and expressive formalism to practical cases.
SCIFF is an abductive proof procedure used for verifying the
compliance of agent behaviour to interaction protocols in multi-agent
systems; SCIFF has been integrated in SOCS-SI, a system able to
observe the agent interaction, pass it to SCIFF for the reasoning
process and to display in a GUI the results of the SCIFF
computation.
In order to assess the applicability of SCIFF and SOCS-SI to
practical cases, we have evaluated qualitatively and experimentally
(not yet formally) their computational behaviour, as far as
limitations and scalability. In this paper we show the results of the
analysis.},
BOOKTITLE = {Atti della Giornata di Lavoro: Analisi sperimentale e benchmark di algoritmi per l'Intelligenza Artificiale},
YEAR = {2005},
EDITOR = {Marco Cadoli and Marco Gavanelli and Toni Mancini},
ADDRESS = {Dipartimento di Ingegneria, Universita` di Ferrara, Italy},
MONTH = JUN # { 10},
URL = {http://www.ing.unife.it/eventi/rcra05/},
NUMBER = {CS-2005-03},
SERIES = {Computer Science Group Technical Reports}
}
This file has been generated by bibtex2html 1.74