Published: 26th July 2013
DOI: 10.4204/EPTCS.120
ISSN: 2075-2180

EPTCS 120

Proceedings Combined 20th International Workshop on
Expressiveness in Concurrency
and 10th Workshop on
Structural Operational Semantics
Buenos Aires, Argentina, 26th August, 2013

Edited by: Johannes Borgström and Bas Luttik

Preface
A Timely Dataflow Model and the Naiad System
Martín Abadi
1
Towards Meta-Reasoning in the Concurrent Logical Framework CLF
Iliano Cervesato and Jorge Luis Sacchini
2
Adding Priority to Event Structures
Youssef Arbach, Kirstin Peters and Uwe Nestmann
17
Compositionality of Approximate Bisimulation for Probabilistic Systems
Daniel Gebler and Simone Tini
32
A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization
Shibashis Guha, Shankara Narayanan Krishna, Chinmay Narayan and S. Arun-Kumar
47
Algebraic Meta-Theory of Processes with Data
Daniel Gebler, Eugen-Ioan Goriac and Mohammad Reza Mousavi
63
The categorical limit of a sequence of dynamical systems
P.J.L. Cuijpers
78
Meta SOS - A Maude Based SOS Meta-Theory Framework
Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir
93

Preface

This volume contains the proceedings of the Combined 20th International Workshop on Expressiveness in Concurrency and the 10th Workshop on Structural Operational Semantics (EXPRESS/SOS 2013) which was held on 26th August, 2013 in Buenos Aires, Argentina, as an affiliated workshop of CONCUR 2013, the 24th International Conference on Concurrency Theory.

The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, and rewrite systems) on the basis of their relative expressive power. The EXPRESS workshop series has run successfully since 1994 and over the years this focus has become broadly construed.

The SOS workshops aim at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the SOS workshop series is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS. Reports on applications of SOS to other fields are also most welcome, including: modelling and analysis of biological systems, security of computer systems programming, modelling and analysis of embedded systems, specification of middle-ware and coordination languages, programming language semantics and implementation, static analysis software and hardware verification, and semantics for domain-specific languages and model-based engineering.

In 2012, the EXPRESS and SOS communities first organized a combined EXPRESS/SOS workshop on the expressiveness of mathematical models of computation and the formal semantics of systems and programming concepts; in 2013, it was decided to continue in this way.

We received nine submissions out of which the programme committee selected seven for presentation at the workshop. These proceedings contain these selected contributions. The workshop also had an invited presentation:

A Timely Dataflow Model and the Naiad System,
by Martín Abadi (Microsoft Research, USA).

We would like to thank the authors of the submitted papers, the invited speaker, the members of the programme committee, and their subreviewers for their contribution to both the meeting and this volume. We also thank the CONCUR 2013 organizing committee for hosting EXPRESS/SOS 2013. Finally, we would like to thank our EPTCS editor Rob van Glabbeek for publishing these proceedings and his help during the preparation.

Johannes Borgström and Bas Luttik,
August 2013.

Programme Committee

Luca Aceto (Reykjavík University, Iceland)
Filippo Bonchi (ENS de Lyon, France)
Johannes Borgström (Uppsala University, Sweden)
Ilaria Castellani (INRIA Sophia Antipolis, France)
Silvia Crafa (University of Padova, Italy)
Yuxi Fu (Shanghai Jiaotong University, China)
Thomas Hildebrandt (IT University of Copenhagen, Denmark)
Sławomir Lasota (Warsaw University, Poland)
Bas Luttik (Eindhoven University of Technology, The Netherlands)
Kirstin Peters (Technical University of Berlin, Germany)
Michel Reniers (Eindhoven University of Technology, The Netherlands)
Louis-Marie Traonouez (IRISA/INRIA Rennes, France)
Irek Ulidowski (University of Leister, United Kingdom)

Additional Reviewers

Benoit Boyer
Yuxin Deng
Mariangiola Dezani-Ciancaglini
Piotr Hofman
Furio Honsell
Bartek Klin
Iain Phillips


A Timely Dataflow Model and the Naiad System

Martín Abadi (Microsoft Research)

Many important data processing applications require high-throughput data ingestion, iterative computation, and low-latency responsiveness. Accordingly, a variety of recent systems aim to address these needs, relying on diverse models of computation.

Naiad is a distributed platform for the execution of data-parallel, cyclic dataflow programs. Naiad combines the high throughput of batch processors, the low latency of stream processors, and the ability to perform iterative and incremental computations. A new computational model, timely dataflow, underlies Naiad and captures opportunities for parallelism across a wide class of algorithms. It subsumes simpler models that support either batch processing or stream processing by enriching dataflow computation with pointstamps, which represent logical points in a computation and help track its progress.

This talk is an introduction to Naiad and to timely dataflow. It emphasizes basic concepts in the computational model and a key element in its realization, namely a distributed algorithm for tracking progress. It is a report on work in progress, joint with Derek Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, Paul Barham, and Tom Rodeheffer at Microsoft Research.