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}
  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://doi.ieeecomputersociety.org/10.1109/ENABL.2004.3},
  pdf = {http://www-lia.deis.unibo.it/~pt/Publications/tapocs04.pdf}
  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/}
  title = {Specification and verification of agent interaction protocols in a logic-based system},
  author = {Marco Alberti and Davide Daolio and Paolo Torroni and Marco Gavanelli and Evelina Lamma and Paola Mello},
  editor = {Hisham Haddad and
               Andrea Omicini and
               Roger L. Wainwright and
               Lorie M. Liebrock},
  booktitle = {Proceedings of the 2004 ACM Symposium on Applied Computing (SAC),
               Nicosia, Cyprus, March 14-17, 2004},
  publisher = {ACM Press},
  address = { New York, NY, USA},
  pages = {72--78},
  year = 2004,
  location = {Nicosia, Cyprus},
  acceptrate = {29\%},
  url = {http://doi.acm.org/10.1145/967900.967918},
  abstract = {
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.},
  isbn = {1-58113-812-1}
  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},
  journal = {Lecture Notes in Artificial Intelligence},
  volume = {2990},
  issn = {0302-9743},
  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.},
  pdf = {http://centria.di.fct.unl.pt/~jleite/dalt03/papers/16.pdf},
  note = {IF: 0.251}
  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.}
  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},
  booktitle = {Conferenza Italiana sui Sistemi Intelligenti},
  editor = {Alfredo Milani},
  publisher = {Morlacchi Editore},
  year = {2004},
  address = {Perugia (Italy)},
  month = {sep},
  isbn = {88-89422-09-2},
  organization = {AI*IA, SIREN, GIPR},
  url = {http://www.dipmat.unipg.it/si04/},
  pages = {80},
  pdf = {http://www.ing.unife.it/docenti/MarcoGavanelli/papers/aev.pdf},
  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
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 the
combinatorial auctions by using social integrity constraints. In
the devised protocol, the auctioneer interacts with an external
solver for the winner determination problem.

This file was generated by bibtex2html 1.98.