LCMAS 2004, the second international workshop on Logic and Communication in Multi-Agent Systems, was held in the second week of ESSLLI 2004, the 16th European Summerschool in Logic, Language and Information hosted by Université Henri Poincaré, Nancy, 9-20 August 2004. These proceedings contain an invited paper and four selected contributions, that were revised based on the feedback of a reviewing process and discussions during the workshop.

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 2004 consisted of Johan van Benthem (Amsterdam), Frank de Boer (CWI Amsterdam, Utrecht), Iliano Cervesato (ITT Industries), Marco Colombetti (Milan), Rogier van Eijk (University of Utrecht), Andrew Jones (King's College London), Yannis Labrou (Fujitsu Labs of America), Riccardo Pucella (Cornell University), Pierre-Yves Schobbens (University of Namur), Marek Sergot (Imperial College London) and Luca Viganò (ETH Zurich). Additional reviewing was carried out by the organisers.

The programme of the workshop consisted of two invited talks, one by Ahti-Veikko Pietarinen (University of Helsinki) entitled Epistemic Logics of Imperfect Information for Multi-Agent Communication, and one by Holger Schlingloff (Humboldt Universität and Frauenhofer Institut, Berlin) entitled Modelling and Model Checking Web Services, complemented by eight technical presentations.

Many thanks to Carlos Areces and Patrick Blackburn, local ESSLLI 2004 organisers, for their excellent logistic and organisational support, and to all who have contributed to and participated in LCMAS 2004 and helped making it a success.

November 2004,
Wiebe van der Hoek, Alessio Lomuscio, Erik de Vink and Mike Wooldridge
(workshop organizers)

Abstract
We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.

Abstract
We introduce an algebraic approach to Dynamic Epistemic Logic. This approach has the advantage that: (i) its semantics is a transparent algebraic object with a minimal set of primitives from which most ingredients of Dynamic Epistemic Logic arise, (ii) it goes with the introduction of non-determinism, (iii) it naturally extends beyond boolean sets of propositions, up to intuitionistic and non-distributive situations, hence allowing to accommodate constructive computational, information-theoretic as well as non-classical physical settings, and (iv) introduces a structure on the actions, which now constitute a quantale. We also introduce a corresponding sequent calculus (which extends Lambek calculus), in which propositions, actions as well as agents appear as resources in a resource-sensitive dynamic-epistemic logic.

Abstract
We present a model-theoretic approach for reasoning about security protocols, applying recent insights from dynamic epistemic logics. This enables us to describe exactly the subsequent epistemic states of the agents participating in the protocol, using Kripke models and transitions between them based on updates of the agents' beliefs associated with steps in the protocol. As a case study we will consider the SRA Three Pass protocol.

Abstract
ATEL is one of the most expressive logics for reasoning about knowledge, time and strategies. Several issues around the interpretation of this logic are still unresolved. This paper contributes to the ongoing discussion by showing that agents do not have to know a specific strategy for doing something in order to have a capability. Furthermore we claim that agents can possess so-called strategic knowledge that is derived from their knowledge of strategies being played. In order to prove these claims we present an alternative interpretation of ATEL over extensive game forms. For the definition of abilities we use strategy domination, and to deal with strategic knowledge we include strategy profiles in the model. We illustrate the interpretation issues mentioned using several small examples. Furthermore we show how perfect recall and perfect memory can be characterized.

Abstract
We propose a framework for the verification of multi-agent systems' specification by symbolic model checking. The language CTLDK (an extension of CTL) allows for the representation of the temporal evolution of epistemic states of the agents, as well as their correct and incorrect functioning behaviour. We ground our analysis on the semantics of deontic interpreted systems. The verification approach is based on an adaption of the technique of bounded model checking, a mainstream approach in verification of reactive systems. We test our results on a typical communication scenario: the bit transmission problem with faults.