EPTCS 59
Proceedings Fourth
Interaction and Concurrency Experience
Reykjavik, Iceland, 9th June 2011
Edited by: Alexandra Silva, Simon Bliudze, Roberto Bruni and Marco Carbone
This volume contains the pre-proceedings of ICE'11, the 4th Interaction and Concurrency Experience workshop, which was held in Reykjavik, Iceland on the 9th of June
2011 as a satellite event of DisCoTec'11.
The ICE workshop series has two distinguishing aspects: firstly,
each year, the workshop focuses on a specific topic and, secondly, it features a novel review
and selection procedure.
The previous editions of ICE were affiliated to ICALP'08 (Reykjavik, Iceland),
CONCUR'09 (Bologna, Italy) and DisCoTec'10 (Amsterdam, The Netherlands) with focus on Synchronous and Asynchronous Interactions, on Structured Interactions, and on Guaranteed Interactions, respectively. The topic of ICE'11 was Reliable and Contract-based Interaction. Reliable interactions are, e.g., those enjoying suitable logical, behavioural, or security properties, or adhering to certain QoS standards. Contract-based interactions are, e.g., those where the interacting entities are committed to give certain guarantees whenever certain assumptions are met by their operating environment.
The ICE procedure for paper selection allows for PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published
on a Wiki and associated with a discussion forum whose access is restricted to the authors
and to all the PC members not declaring a conflict of interests. The PC members post
comments and questions that the authors reply to. As at the past three editions, the forum
discussion during the review and selection phase of ICE'11 has considerably improved
the accuracy of the feedback from the reviewers and the quality of accepted papers, and
offered the basis for a lively discussion during the workshop.
The interactive selection procedure implies additional effort for both authors and PC
members. The effort and time spent in the forum interaction is rewarding for both
authors -- when updating their papers -- and reviewers -- when writing their reviews: the
forum discussion helps to discover and correct typos in key definitions and mispelled
statements, to improve examples and presentation of critical cases, and solve any misunderstanding at the very early stage of the review
process.
Each paper was reviewed by four PC members, and altogether 8 papers (out of
12) were accepted for publication. We were proud to host three invited talks by Rocco De Nicola (joint with PACO), Simon Gay and Prakash Panangaden, whose abstracts are included
in this volume together with the regular
papers. The contributions
are included in the same order as they were presented at the workshop. Final versions,
taking into account the discussion at the workshop, will appear in the final proceedings
to be published by the Electronic Proceedings in Theoretical Computer Science.
We would like to thank the authors of all the submitted papers for their interest in
the workshop and the PC members for their efforts, which provided for the success of the
ICE workshop. We thank Rocco de Nicola, Simon Gay and Prakash Panangaden for accepting
our invitations to present their recent work, and the DisCoTec'11 organisers, in particular the general and workshop chairs, for providing
an excellent environment for the preparation and staging of the event. Moreover, we thank the organizers of the workshop PACO for having accepted sharing Rocco De Nicola as an invited speaker. Finally, we thank
EPTCS editors for the publication of post-proceedings and the sponsors of the event,
namely CEA LIST, Centrum Wiskunde & Informatica and the University of Pisa that made it possible to offer travel grants to students.
Simon Bliudze - CEA LIST (France)
Roberto Bruni - University of Pisa (Italy)
Marco Carbone - ITU (Denmark)
Alexandra Silva - CWI (The Netherlands)
Prakash Panangaden
We develop a game semantics for process algebra with two interacting agents. The purpose of our
semantics is to make manifest the role of knowledge and information flow in the interactions between
agents and to control the information available to interacting agents. We define games and strategies on
process algebras, so that two agents interacting according to their strategies determine the execution of
the process, replacing the traditional scheduler. We show that different restrictions on strategies repre-
sent different amounts of information being available to a scheduler. We also show that a certain class
of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were
developed to overcome problems with traditional schedulers modelling interaction. The restrictions on
these strategies have an explicit epistemic flavour. This is joint work with Konstantinos Chatzikokolakis
and Sophia Knight, both at INRIA Saclay
Rocco De Nicola (IMT - Institute for Advanced Studies Lucca and University of Florence, Italy)
Labeled transition systems (LTS) are typically used as behavioral models of nondeterministic processes, with labeled transitions defining a one-step state-to-state reachability relation. This model is made more general by modifying the transition relation in such a way that it associates with any source state and transition label a reachability distribution, i.e., a function mapping each possible target state to a value of some domain that expresses the degree of one-step reachability of that target state from the source one. The resulting model, called ULTraS from Uniform Labeled Transition System, can then be specialized, by selecting suitable domains, to a number of widely used behavioral models representing fully nondeterministic, fully probabilistic and fully stochastic processes, but also processes combining nondeterminism and probability or nondeterminism and stochasticity.
We will show how ULTraS can be used to model stochastic process calculi when the reachability distribution does represent the rate of the exponential distribution characterizing the execution time of the performed action. By defining appropriate operators on reachability distributions, we will provide compositional operational semantics of representative fragments of the major stochastic calculi and shed light on their differences and similarities.
The uniform treatment of different operational models can be extended uniformly to model classical behavioral equivalences like bisimulation, trace, and testing. These equivalences will be defined over ULTraS parametrically with respect to some measure function that expresses the degree of multi-step reachability of a set of states. It will be then shown that the specializations of bisimulation, trace, and testing equivalences over ULTraS, obtained for the various types of process by selecting suitable measure functions, coincide with some of the well known behavioral equivalences defined in the literature, thus emphasizing the adequacy of ULTraS as a unifying behavioral model.
This is the outcome of joint work with M. Bernardo, D. Latella, M. Loreti, M. Massink.