Published: 31st July 2011
DOI: 10.4204/EPTCS.59
ISSN: 2075-2180


Proceedings Fourth
Interaction and Concurrency Experience
Reykjavik, Iceland, 9th June 2011

Edited by: Alexandra Silva, Simon Bliudze, Roberto Bruni and Marco Carbone

Simon Bliudze, Roberto Bruni, Marco Carbone and Alexandra Silva
Invited Presentation: Epistemic Strategies and Games on Concurrent Processes
Prakash Panangaden
Innocent strategies as presheaves and interactive equivalences for CCS
Tom Hirschowitz and Damien Pous
Interaction and observation, categorically
Vincenzo Ciancia
Structured Operational Semantics for Graph Rewriting
Andrei Dorman and Tobias Heindel
Polymorphic Endpoint Types for Copyless Message Passing
Viviana Bono and Luca Padovani
Invited Presentation (joint with PACO): A Uniform Framework for Modeling Processes Behaviors and their Performances
Rocco De Nicola
On the reaction time of some synchronous systems
Ilias Garnier, Christophe Aussaguès, Vincent David and Guy Vidal-Naquet
Correlating Formal Semantic Models of Reo Connectors: Connector Coloring and Constraint Automata
Sung-Shik T.Q. Jongmans and Farhad Arbab
Invited Presentation: Formal Analysis of Quantum Systems using Process Calculus
Timothy A.S. Davidson, Simon J. Gay and Rajagopal Nagarajan
Amending Contracts for Choreographies
Laura Bocchi, Julien Lange and Emilio Tuosto
Contracts in distributed systems
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino


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)

Epistemic Strategies and Games on Concurrent Processes

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

A Uniform Framework for Modeling Processes Behaviors and their Performances

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.