2006.bib

@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.