@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c 'keywords : "agents"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@inproceedings{AnconaEtAl16,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Comparing Trace Expressions and Linear Temporal Logic for Runtime
Verification},
booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank
de Boer on the Occasion of His 60th Birthday},
pages = {47--64},
year = {2016},
abstract = {{Trace expressions are a compact and expressive formalism, initially devised
for runtime verification of agent interactions in multiagent systems, which has been
successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms,
and generalized to support runtime verification of different kinds of properties and systems.
In this paper we formally compare the expressive power of trace expressions with
the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification.
We show that any LTL formula can be translated into a trace expression
which is equivalent from the point of view of runtime verification.
Since trace expressions are able to express and verify sets of traces that
are not context-free, we can derive that in the context of runtime verification
trace expressions are more expressive than LTL.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaEtAlFdB16.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaBFMT14,
author = {Ancona, Davide and
Briola, Daniela and
El Fallah{-}Seghrouchni, Amal and
Mascardi, Viviana and
Taillibert, Patrick},
title = {Exploiting Prolog for Projecting Agent Interaction Protocols},
booktitle = {Proceedings of the 29th Italian Conference on Computational Logic,
Torino, Italy, June 16-18, 2014.},
pages = {30--45},
year = {2014},
abstract = {{Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we demonstrated that they can be used to represent complex protocols in a very compact way, and we exploited them to dynamically verify correct implementation of a protocol in a real MAS framework, Jason.
The main drawback of our previous approach is the full centralization of the monitoring activity which is delegated to a unique monitor agent.
This approach works well for MASs with few agents, but could become unsuitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored.
In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags,
by restricting it to the interactions involving agents in Ags, so that the outcome of the algorithm is
another constrained global type that can be safely used for verifying the compliance of the sub-system Ags to the protocol specified by the original constrained global type.
The projection mechanism is implemented in SWI Prolog and is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning the agents of the MAS into small sets
of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type.
We leave for further investigation the problem of finding suitable partitions of agents in a MAS, to guarantee that
verification through projected types and distributed agents is equivalent to verification
performed by a single centralized monitor with a unique global type.}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaBFMT14.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@article{MascardiEtAl14,
keywords = {{agents}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/MABBR@WIAS14.pdf},
author = {Mascardi, V. and Ancona, D. and Barbieri, M. and Bordini, R. H. and Ricci, A.},
title = {{CooL-AgentSpeak: Endowing AgentSpeak-DL agents with plan exchange and ontology services}},
journal = {{Web Intelligence and Agent Systems}},
volume = {12},
number = {1},
pages = {83-107},
year = {2014},
abstract = { In this paper we present CooL-AgentSpeak, an extension of
AgentSpeak-DL with plan exchange and ontology services. In
CooL-AgentSpeak, the search for an ontologically relevant plan is no
longer limited to the agent's local plan library but is carried out
in the other agents' libraries too, according to a cooperation
strategy, and it is not based solely on unification and on the
subsumption relation between concepts, but also on ontology
matching. Belief querying and updating also take advantage of
ontological reasoning and matching.}
}
@inproceedings{AnconaEtAl13a,
booktitle = {{ACM Symposium on Applied Computing (SAC 2013)}},
keywords = {{agents, behavioral-types,runtime-verification}},
note = {{Poster paper}},
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {{Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems}},
pages = {1-3},
year = {2013},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-SAC13.pdf},
abstract = {Global types are behavioral types for specifying and verifying multiparty
interactions between distributed components, inspired by the process algebra approach.
In this paper we extend the formalism of global types in multi-agent systems resulted from our previous work with a mechanism for easily expressing constrained shuffle of message sequences; accordingly, we extend the semantics to include the newly introduced feature, and show the expressive power of these ``constrained global types''.
}
}
@inproceedings{AMP-SAC12,
author = {Ancona, D. and Mascardi, V. and Pavarino, O.},
title = {Ontology-based documentation extraction for
semi-automatic migration of {J}ava code},
booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
2012)},
editor = {Ossowski, S. and Lecca, P.},
pages = {1137--1143},
publisher = {ACM},
abstract = {Migrating libraries is not a trivial task, even under
the simplest assumption of a downward compatible
upgrade. We propose a novel approach to partially
relieve programmers from this task, based on the simple
observation that class, method and field names and
comments contained in a Java library should be a good
approximation of its semantics, and that code migration
requires knowing the semantic similarities between the
two libraries. Following this assumption, we borrow the
main concepts and notions from the Semantic Web, and
show how (1) an ontology can be automatically generated
from the relevant information extracted from the code
of the library; (2) semantic similarities between two
different libraries can be found by running a
particular ontology matching (a.k.a. ontology
alignment) algorithm on the two ontologies extracted
from the libraries. The main advantages of the approach
are that ontology extraction can be fully automated,
without adding ad-hoc code annotations, and that
results and tools produced by the Semantic Web research
community can be directly re-used for our purposes.
Experiments carried out even with simple and efficient
freely available matchers show that our approach is
promising, even though it would benefit from the use of
more advanced ontology matchers possibly integrated
with a component for checking type compatibility of the
computed alignments. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AMP-SAC12.pdf},
keywords = {agents, ontologies, refactoring},
year = 2012
}
@inproceedings{ABM-ICTCS12,
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {Global {T}ypes for {D}ynamic {C}hecking of {P}rotocol
{C}onformance of {M}ulti-{A}gent {S}ystems ({E}xtended
{A}bstract)},
booktitle = {13th {I}talian {C}onference on {T}heoretical
{C}omputer {S}cience ({ICTCS} 2012)},
editor = {Massazza, P.},
pages = {39--43},
abstract = {In this paper we investigate the theoretical
foundations of global types for dynamic checking of
protocol compliance in multi-agents systems and we
extend the formalism by introducing a concatenation
operator that allows a significant enhancement of the
expressive power of global types. As examples, we show
how two non trivial protocols can be compactly
represented in the formalism: a ping-pong protocol, and
an alternating bit protocol, in the version proposed by
Deni\backslash{}'elou and Yoshida. Both protocols
cannot be specified easily (if at all) by other global
type frameworks, while in our approach they can be
expressed by two deterministic types (in a sense made
precise in the sequel) that can be effectively employed
for dynamic checking of the conformance to the
protocol.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-ICTCS12.pdf},
keywords = {agents, behavioral-types,runtime-verification},
year = 2012
}
@inproceedings{ADM-DALT12,
author = {Ancona, D. and Drossopoulou, S. and Mascardi, V.},
title = {{Automatic Generation of Self-Monitoring MASs from
Multiparty Global Session Types in Jason}},
booktitle = {Declarative agent languages and technologies (DALT
2012).},
pages = {1--20},
publisher = {Springer},
abstract = {Global session types are behavioral types designed for
specifying in a compact way multiparty interactions
between distributed components, and verifying their
correctness. We take advantage of the fact that global
session types can be naturally represented as cyclic
Prolog terms - which are directly supported by the
Jason implementation of AgentSpeak - to allow simple
automatic generation of self-monitoring MASs: given a
global session type specifying an interaction protocol,
and the implementation of a MAS where agents are
expected to be compliant with it, we define a procedure
for automatically deriving a self-monitoring MAS. Such
a generated MAS ensures that agents conform to the
protocol at run-time, by adding a monitor agent that
checks that the ongoing conversation is correct w.r.t.
the global session type. The feasibility of the
approach has been experimented in Jason for a
non-trivial example involving recursive global session
types with alternative choice and fork type
constructors. Although the main aim of this work is the
development of a unit testing framework for MASs, the
proposed approach can be also extended to implement a
framework supporting self-recovering MASs.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ADM-DALT12.pdf},
keywords = {agents, behavioral-types, runtime-verification},
year = 2012
}
@inproceedings{MA-DALT11,
author = {Mascardi, V. and Ancona, D},
title = {1000 Years of Coo-{BDI}},
booktitle = {{D}eclarative {A}gent {L}anguages and {T}echnologies
{IX} - 9th {I}nternational {W}orkshop, {DALT} 2011,
Revised Selected and Invited Papers},
pages = {95-101},
abstract = {The idea of extending the BDI architecture with
cooperativity started shaping in 2003 when two
independent proposals to support cooperation in a BDI
setting were presented at DALT. One proposal, Coo-BDI,
extended the BDI architecture by allowing agents to
cooperate by exchanging and sharing plans in a quite
flexible way; the other extended the BDI operational
semantics for introducing speech-act based
communication, including primitives for plan exchange.
Besides allowing a natural and seamless integration
with speech-act based communication for BDI languages,
the intuitions behind Coo-BDI have proved to be
promising and attractive enough to give rise to new
investigations. In this retrospective review we discuss
papers that were influenced by Coo-BDI and we outline
other potential developments for future research.},
keywords = {agents, behavioral-types},
ftp = {http://www.disi.unige.it/person/MascardiV/Download/1000YearsCooBDI.pdf},
year = 2011
}
@inproceedings{MABR-IAT11,
author = {Mascardi, V. and Ancona, D. and Bordini, R. H. and
Ricci, A.},
title = {CooL-{A}gent{S}peak: {E}nhancing {A}gent{S}peak-{DL}
{A}gents with {P}lan {E}xchange and {O}ntology
{S}ervices},
booktitle = {Proceedings of the 2011 {IEEE}/{WIC}/{ACM}
{I}nternational {C}onference on {I}ntelligent {A}gent
{T}echnology, {IAT} 2011},
pages = {109-116},
abstract = {In this paper we present CooL-AgentSpeak, an extension
of AgentSpeak-DL with plan exchange and ontology
services. In CooL-AgentSpeak, the search for a plan is
no longer limited to the agent's local plan library but
is carried out in the other agents' libraries too,
according to a cooperation strategy, and it is not
based solely on unification and on the subsumption
relation between concepts, but also on ontology
matching. Belief querying and updating take advantage
of ontological reasoning and matching as well.},
keywords = {agents, behavioral-types},
ftp = {http://www.disi.unige.it/person/MascardiV/Download/IAT2011.pdf},
year = 2011
}
@inproceedings{AnconaMascardi-MALLOW-AWESOME09,
author = {Ancona, D. and Mascardi, V.},
title = {Exploiting {A}gents and {O}ntologies for {T}ype- and
{M}eaning-{S}afe {A}daptation of {J}ava {P}rograms},
booktitle = {Proceedings of the {MALLOW}-{AWESOME} 2009 workshop},
volume = {494},
publisher = {CEUR Workshop Proceedings},
abstract = {This paper discusses an application of intelligent
software agents and ontologies to solve the problem of
semi-automatic porting of Java programs. We have
designed a system for aiding users to adapt Java code
in a type- and meaning-safe way, when an application
has to migrate to new libraries which are not fully
compatible with the legacy ones. To achieve this, we
propose an approach based on an integration of the two
type-theoretic notions of subtyping and type
isomorphism with ontology matching. While the former
notions are needed to ensure flexible adaptation in the
presence of type-safety, the latter supports the user
to preserve the meaning of names that appear in the
program to be adapted. Intelligent agents control the
different components of the system and interact with
other agents in order to provide the final user with
the semi-automatic porting service he/she required.},
ftp = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-494/mallowawesomepaper6.pdf},
keywords = {agents,refactoring},
year = 2009
}
@inproceedings{MDA-WOA05,
author = {Mascardi, V. and Demergasso, D. and Ancona, D.},
title = {Languages for {P}rogramming {BDI}-style {A}gents: an
{O}verview},
booktitle = {W{OA} 2005 - {W}orkshop {F}rom {O}bjects to {A}gents},
editor = {Corradini, F. and De Paoli, F. and Merelli, E. and
Omicini, A.},
pages = {9--15},
abstract = {The notion of an intelligent agent as an entity which
appears to be the subject of mental attitudes like
beliefs, desires and intentions (hence, the BDI
acronym) is well known and accepted by many
researchers. Besides the definition of various BDI
logics, many languages and integrated environments for
programming BDI-style agents have been proposed since
the early nineties. In this reasoned bibliography, nine
languages and implemented systems, namely PRS, dMARS,
JACK, JAM, Jadex, AgentSpeak(L), 3APL, Dribble, and
Coo-BDI, are discussed and compared. References to
other systems and languages based on the BDI model are
also provided, as well as pointers to surveys dealing
with related topics. },
ftp = {http://www.disi.unige.it/person/MascardiV/Download/ancona-demergasso-mascardi-WOA05-final.pdf},
keywords = {agents},
year = 2005
}
@inproceedings{BMAB-EUMAS05,
author = {Bozzo, L. and Mascardi, V. and Ancona, D. and Busetta,
P.},
title = {C{OOWS}: {A}daptive {BDI} {A}gents meet
{S}ervice-{O}riented {C}omputing},
booktitle = {E{UMAS} 2005 - {P}roceedings of the {T}hird {E}uropean
{W}orkshop on {M}ulti-{A}gent {S}ystems, {B}russels,
{B}elgium, {D}ecember 7-8, 2005},
editor = {Gleizes, M. P. and Kaminka, G. A. and Now\'e, A. and
Ossowski, S. and Tuyls, K. and Verbeeck, K.},
pages = {473},
abstract = {Mainstream research in Web Services is currently
looking at two main aspects, namely formally describing
interactions among services, and finding and combining
services. Much work made in the intelligent agents area
is being applied to these issues. In this paper, we
investigate the application of agent research to Web
Services from a different perspective, that is,
procedural learning. The final objective is to enable
an adaptive system (an agent in our terminology) to
discover or being fed with knowledge concerning how to
solve a specific set of problems in a specific software
or physical environment. Our work is a very preliminary
step into the issue, with the main objective of
assessing how current Web Services technology can
support a component, described in terms of beliefs,
desires and intentions, dynamically adapting its
behaviour to new environments. },
ftp = {http://www.disi.unige.it/person/MascardiV/Download/coows4eumas.zip},
keywords = {agents},
year = 2005
}
@inproceedings{AMHB-AAMAS04,
author = {Ancona, D. and Mascardi, V. and H\"ubner, J.F. and
Bordini, R. H.},
title = {Coo-{A}gent{S}peak: {C}ooperation in {A}gent{S}peak
through {P}lan {E}xchange},
booktitle = {A{AMAS} 2004 ({I}nt. {C}onf. on {A}utonomous {A}gents
and {M}ultiagent {S}ystems)},
editor = {Jennings, N. R. and Sierra, C. and Sonenberg, L. and
Tambe, M.},
pages = {698--705},
publisher = {ACM press},
abstract = { This paper brings together two recent contributions
to the area of declarative agent-oriented programming,
made feasible in practice by the recent introduction of
an interpreter for a BDI programming language. The work
on CooBDI has proposed an approach to plan exchange
which applies to BDI agents in general. The other
contribution is the introduction of special
illocutionary forces for plan exchange between
AgentSpeak agents. This has been implemented in Jason,
an interpreter for an extended version of
AgentSpeak(L). Jason also provides mechanisms that
allow the specification of plan permissions, which are
important in the cooperation context. This paper shows
how elaborate plan exchange can take place between
AgentSpeak agents implemented with Jason. It also
discusses an application in which plan sharing is
essential.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/AAMAS04.pdf},
keywords = {agents},
year = 2004
}
@inproceedings{AM-DALT04,
author = {Ancona, D. and Mascardi, V.},
title = {Coo-{BDI}: {E}xtending the {BDI} {M}odel with
{C}ooperativity},
booktitle = {Declarative {A}gent {L}anguages and {T}echniques,
{F}irst {I}nternational {W}orkshop, {DALT} 2003,
{R}evised {S}elected and {I}nvited {P}apers},
editor = {Leite, J. and Omicini, A. and Sterling, L. and
Torroni, P.},
volume = {2990},
series = {Lecture Notes in Computer Science},
pages = {109--134},
publisher = {Springer Verlag},
abstract = {We define Coo-BDI, an extension of the BDI
architecture with the notion of cooperativity. Agents
can cooperate by exchanging and sharing plans in a
quite flexible way. As a main result Coo-BDI promotes
adaptivity and sharing of resources; as a by-product,
it provides a better support for dealing with agents
which do not possess their own procedural knowledge for
processing a given event. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DALT03.ps.gz},
keywords = {agents},
year = 2004
}
@inproceedings{BriolaMascardiAnconaIDC14,
author = {Briola, D. and
Mascardi, V. and
Ancona, D.},
title = {Distributed Runtime Verification of {JADE} Multiagent Systems},
booktitle = {Intelligent Distributed Computing {VIII} - Proceedings of the 8th
International Symposium on Intelligent Distributed Computing, {IDC}
2014, Madrid, Spain, September 3-5, 2014},
pages = {81--91},
year = {2014},
abstract = {{Verifying that agent interactions in a multiagent system (MAS) are compliant to a given global protocol is of paramount importance for most systems, and is mandatory for safety-critical applications. Runtime verification requires a proper formalism to express such a protocol, a possibly non intrusive mechanism for capturing agent interactions, and a method for verifying that captured interactions are compliant to the global protocol. Projecting the global protocol onto agents' subsets can improve efficiency and fault tolerance by allowing the distribution of the verification mechanism. Since many real MASs are based on JADE, a well known open source platform for MAS development, we implemented a monitor agent that achieves all the goals above using the "Attribute Global Types" (AGT) formalism for representing protocols. Using our JADE monitor we were able to verify FYPA, an extremely complex industrial MAS currently used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations, besides the Alternating Bit and the Iterated Contract Net protocols which are well known in the distributed systems and MAS communities. Depending on the monitored MAS, the performances of our monitor are either comparable or slightly worse than those of the JADE Sniffer because of the logging of the verification activities. Reducing the log files dimension, re-implementing the monitor in a way independent from the JADE Sniffer, and heavily exploiting projections are the three directions we are pursuing for improving the monitor's performances, still keeping all its features. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/IDC2014.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@inproceedings{MascardiBriolaAnconaAIIA13,
author = {Mascardi, V. and
Briola, D. and
Ancona, D.},
title = {On the Expressiveness of Attribute Global Types: The Formalization
of a Real Multiagent System Protocol},
booktitle = {AI*IA 2013: Advances in Artificial Intelligence - XIIIth International
Conference of the Italian Association for Artificial Intelligence,
Turin, Italy, December 4-6, 2013. Proceedings},
pages = {300--311},
year = {2013},
abstract = {{Attribute global types are a formalism for specifying and dynamically verifying multi-party agents interaction protocols. They allow the multiagent system designer to easily express synchronization constraints among protocol branches and global constraints on sub-sequences of the allowed protocol traces. FYPA (Find Your Path, Agent!) is a multiagent system implemented in Jade currently being used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations. Since information on the station topology and on the current resource allocation is fully distributed, FYPA involves complex negotiation among agents to find a solution in quasi-real time. In this paper we describe the FYPA protocol using both AUML and attribute global types, showing that the second formalism is more concise than the first, besides being unambiguous and amenable for formal reasoning. Thanks to the Prolog implementation of the transition function defining the attribute global type semantic, we are able to generate a large number of protocol traces, and to manually inspect a subset of them to empirically validate that the protocol's formalization is correct. The integration of the Prolog verification mechanism into a Jade monitoring agent extending the Sniffer Agent is under way and will be used to verify the compliance of the actual conversation with the protocol. Keywords: multiagent systems, attribute global types, negotiation, dynamic verification of protocol compliance. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AIIA2013.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@article{Betty16,
author = {Ancona, D. and
Bono, V. and
Bravetti, M. and
Campos, J. and
Castagna, G. and
Deni{\'{e}}lou, P.~M. and
Gay, S.~J. and
Gesbert, N. and
Giachino, E. and
Hu, R. and
Johnsen, E.~B. and
Martins, F. and
Mascardi, V. and
Montesi, F. and
Neykova, R. and
Ng, N. and
Padovani, L. and
Vasconcelos, V.T. and
Yoshida, N.},
title = {Behavioral Types in Programming Languages},
journal = {Foundations and Trends in Programming Languages},
volume = {3},
number = {2-3},
pages = {95--230},
year = {2016},
url = {http://dx.doi.org/10.1561/2500000031},
doi = {10.1561/2500000031},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/behavioralTypes.pdf}
}
@inproceedings{AnconaFerrandoMascardi17,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Parametric Runtime Verification of Multiagent Systems},
booktitle = {Proceedings of the 16th Conference on Autonomous Agents and MultiAgent
Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},
pages = {1457--1459},
year = {2017},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
Parametricity is an important feature of a monitoring
system for making runtime verification (RV) more effective,
since, typically, correctness of traces depends on the specific
data values that are carried by the monitored events of the
trace, and that, in general, cannot be predicted statically.
Typically, the correctness of an interaction protocol may
depend on the values exchanged by agents; protocols may
also be parametric in the involved agents, and resources, and
this parametricity is naturally reflected on the data carried
by values.
In this work we propose parametric trace expressions, an
extension to trace expressions, expressly designed for
parametric RV of multiagent systems. Such an extension is
achieved by introducing variables in trace expressions that
are substituted with data values at runtime, when events are
matched during monitoring.
}},
http = {http://www.disi.unige.it/person/AnconaD/papers/AnconaFerrandoMascardiAAMAS17Parametric.pdf}
}
This file was generated by bibtex2html 1.98.