[Home Page of ENTCS] [Volume/Issue List of ENTCS] [Author Index of ENTCS]
Table of Contents of Volume 85, Issue 2
Preface Volume 85, Issue 2
Wiebe van der Hoek, Alessio Lomuscio, Erik de Vink & Mike Wooldrige
[Preface]
Alternating-time logic with imperfect recall
Pierre-Yves Schobbens
[Abstract]
[Full text]
(PDF 164.0 Kb)
Specification and Verification of Agent Interaction using
Social Integrity Constraints
Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello & Paolo Torroni
[Abstract]
[Full text]
(PDF 261.1 Kb)
A Logic of Ignorance
Wiebe van der Hoek & Alessio Lomuscio
[Abstract]
[Full text]
(PDF 215.8 Kb)
Dialogue Games for Inconsistent and Biased Information
Henk-Jan Lebbink, Cilia Witteman & John-Jules Ch. Meyer
[Abstract]
[Full text]
(PDF 280.7 Kb)
Knowledge as Strategic Ability
Sieuwert van Otterloo, Wiebe van der Hoek & Michael Wooldridge
[Abstract]
[Full text]
(PDF 250.6 Kb)
A Tool for Specification and Verification of Epistemic Properties
Franco Raimondi & Alessio Lomuscio
[Abstract]
[Full text]
(PDF 205.3 Kb)
A Logical Model for Agent Communication Languages
Mario Verdicchio & Marco Colombetti
[Abstract]
[Full text]
(PDF 182.2 Kb)
Preface Volume 85, Issue 2
Wiebe van der Hoek, Alessio Lomuscio, Erik de Vink and Mike Wooldridge
LCMAS 2003, the first international workshop on Logic and Communication in Multi-Agent Systems, was held on June 29th, 2003 in Eindhoven, the Netherlands as a pre-conference satelite of the thirtieth International Colloquium on Automata, Languages and Programming ICALP 2003. These proceedings contain invited and contributed papers that were revised based on the feedback of a reviewing process and discussions during the workshop and have been collected in this volume.
The LCMAS workshop series aims at bringing together researchers interested in topics related to the development and use of formal tools when applied to modelling, specifying, verifying, and reasoning about multi-agent systems in which communication and updating play a crucial role. Therefore, the workshop wants to provide a forum for discussing technical issues that arise in formalisms (epistemic, temporal, dynamic and authentication logics and tools) inspired by the needs of modelling information exchanges in multi-agent systems. The papers contained in this volume illustrate various approaches of dealing with interpretation and profilation of information in multi-agent systems.
The program commitee for LCMAS 2003 consisted of David Basin (Zurich), Johan van Benthem (Amsterdam), Frank de Boer (CWI Amsterdam, Utrecht), Marco Colombetti (Milan), Tim Finin (Baltimore), Yannis Labrou (Fujitsu Labs of America), Marek Sergot (Imperial College London) and Paul Syverson (Naval Research Lab). Additional reviewing was carried out by the organisers. At the workshop two invited talks were welcomed: one by Pierre-Yves Schobbens (Namur) entitled Alternating-time logic with imperfect recall, and one by Alexandru Baltag (Oxford) entitled Epistemic Program Constructs: learning, updating, responding, intercepting. Many thanks to all who have contributed to and participated in LCMAS 2003. The financial support of the ICALP 2003 organisation and of Technische Universiteit Eindhoven is gratefully acknowledged.
December 2003, Wiebe van der Hoek, Alessio Lomuscio, Erik de Vink and Mike Wooldridge (workshop organizers)
Abstract
We study here a variant of the alternating-time temporal logic (ATL) where each
agent has a given memory. We show that it is an interesting compromise, rather
realistic but with a reasonable complexity. In contrast, most models with
perfect recall and imperfect information have an undecidable model-checking
Specification and Verification of Agent Interaction using
Social Integrity Constraints
Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello & Paolo Torroni
Abstract
In this paper we propose a logic-based social approach to the 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 to 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 attention on static verification of 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.
A Logic of Ignorance
Wiebe van der Hoek & Alessio Lomuscio
Abstract
We introduce and motivate a non-standard multi-modal logic to
represent and reason about ignorance in Multi-Agent Systems. We argue
that in Multi-agent systems being able to reason about what agents
ignore is just as important as being able to reason about what
agents know. We show a sound and complete axiomatisation for the
logic. We investigate its applicability by restating the feasibility
condition for the FIPA communication primitive of inform.
Dialogue Games for Inconsistent and Biased Information
Henk-Jan Lebbink, Cilia Witteman & John-Jules Ch. Meyer
Abstract
A dialogue game is presented that describes coherent conversational sequences
with inconsistent and biased information between agents at the speech act
level. These types of information are represented with the use of a
multi-valued logic based on a bilattice structure. This approach makes it
possible to devise a dialogue game in which agents can deliberate their
cognitive states with inconsistent and biased information.
Knowledge as Strategic Ability
Sieuwert van Otterloo, Wiebe van der Hoek & Michael Wooldridge
Abstract
The ultimate goal of our research is to develop techniques for model
checking knowledge properties of multi-agent systems. ATEL, an
extension of the Alternating-time Temporal Logic of Alur et al, is a
logic for specifying epistemic and strategic properties of such
systems. We present a technique for reducing the ATEL model checking
problem to one of model checking in ATL, whereby epistemic relations
are explicitly encoded in ATL models as as dynamic transitions. The
techniques is illustrated by means of a knowledge game, which is used
as a running example throughout the paper.
A Tool for Specification and Verification of Epistemic Properties
Franco Raimondi & Alessio Lomuscio
Abstract
We present a compiler that translates a multi-agent systems specification
given in the formalism of Interpreted Systems into an SMV program. We show
how an SMV model checker can be coupled with a Kripke model editor (Akka) to
allow for the mechanical verification of epistemic properties of multi-agent
systems.
A Logical Model for Agent Communication Languages
Mario Verdicchio & Marco Colombetti
Abstract
The current ACL proposals show some shortcomings with respect to
the definition of their semantics. Our paper aims at tackling
those issues by defining an ACL semantics as a specification of
the analytical effects of agent communicative acts. We analyze
agent communication in terms of concepts taken from Speech Act
Theory, as several researchers have already done, but move away
from the mainstream view of artificial agent research, as we
define communicative acts in terms of changes at the level of
social relationship between agents. We take commitment to be a
primitive concept underlying the social dimension of multiagent
systems, and define a basic artificial institution whose aim is to
provide agents with the means to affect the commitment network
that binds them to each other.
© Copyright 2004, Elsevier Science, All rights reserved.