EXPRESS/SOS 2013Combined 20th International Workshop on
Expressiveness in Concurrencyand 10th Workshop on
Structural Operational Semantics
Buenos Aires, Argentina
Affiliated with CONCUR 2013
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, semantics for domain-specific languages and model-based engineering.
In 2012, the EXPRESS and SOS communities decided to join forces and organise a combined EXPRESS/SOS workshop. The combined workshop was a success, so this year there will again be a combined workshop on the semantics of systems and programming concepts, and on the expressiveness of mathematical models of computation.
|Martín Abadi (Microsoft Research)|
|9.00-10.00:||Martín Abadi (invited presentation)|
|A Timely Dataflow Model and the Naiad System|
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.
|10:30-11:00||Iliano Cervesato and Jorge Luis Sacchini|
|Towards Meta-Reasoning in the Concurrent Logical Framework CLF|
|The Concurrent Logical Framework (CLF) is an extension of the logical framework LF designed to specify concurrent and distributed languages. While it can be used to define a variety of formalisms, reasoning about such languages within CLF has proved elusive. In this paper, we propose an extension of LF that allows us to express properties of CLF specifications. We illustrate the approach with a proof of safety for a small language with a parallel semantics.|
|11.00-11.30:||Youssef Arbach, Kirstin Peters and Uwe Nestmann|
|Adding Priority to Event Structures|
Event structures (ESs) are mainly concerned with the representation of causal relationships between events, usually accompanied by other event relations capturing conflicts and disabling. By now, the most prominent variants of ESs are Prime ES, Extended Bundle ES and Dual ES, which differ in their causality models and event relations. Yet, some application domains require further kinds of relations between events. Here, we add the possibility to express priority relationships among events.
Technically, we enhance the three mentioned variants in the same way. For each variant, we then study the interference between priority and the other event relations. From this, we extract equivalence rules-notably differing for the types of ESs-that are valuable for modelling and enable us to provide a comparison between the extensions. We also exhibit that priority complicates the definition of partial orders in ESs.
|11.30-12.00:||Daniel Gebler and Simone Tini|
|Compositionality of Approximate Bisimulation for Probabilistic Systems|
|Probabilistic transition system specifications using the rule format \ntmufxt\ provide structural operational semantics for Segala-type systems and guarantee that probabilistic bisimilarity is a congruence. Probabilistic bisimilarity is for many applications too sensitive to the exact probabilities of transitions. Approximate bisimulation provides a robust semantics that is stable for bounded implementation and measurement errors of probabilistic behavior. We provide a general method to quantify how much a process combinator expands the approximate bisimulation distance. As a direct application we derive an appropriate rule format that guarantees compositionality with respect to approximate bisimilarity. Moreover, we describe how specification formats for non-standard compositionality requirements may be derived.|
|12.00-12.30:||Shibashis Guha, Shankara Narayanan Krishna, Chinmay Narayan and S. Arun-Kumar|
|A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization|
|In this paper we present a unifying approach for deciding various bisimulations, simulation equivalences and preorders between two timed automata states. We propose a zone based method for deciding these relations in which we eliminate an explicit product construction of the region graphs or the zone graphs as in the classical methods. Our method is also generic and can be used to decide several timed relations. We also present a game characterization for these timed relations and show that the game hierarchy reflects the hierarchy of the timed relations. One can obtain an infinite game hierarchy and thus the game characterization further indicates the possibility of defining new timed relations which have not been studied yet. The game characterization also helps us to come up with a formula which encodes the separation between two states that are not timed bisimilar. Such formulae can also be generated for many relations other than timed bisimulation.|
|14:00-14.30||Daniel Gebler, Eugen-Ioan Goriac and Mohammadreza Mousavi|
|Algebraic Meta-Theory of Processes with Data|
|There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics (SOS). Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (memory, or store), which has numerous practical applications. We show how the rule formats for algebraic properties can be exploited in a generic manner in the setting with the data. Moreover, we introduce a new approach of deriving sound and ground-complete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on using intuitive operations for handling the store component.|
|The categorical limit of a sequence of dynamical systems|
|Modeling a sequence of design steps, or a sequence of parameter settings, yields a sequence of dynamical systems. In many cases, such a sequence is intended to approximate a certain limit case. However, formally defining that limit turns out to be subject to ambiguity. Depending on the interpretation of the sequence, i.e. depending on how the behaviors of the systems in the sequence are related, it may vary what the limit should be. Topologies, and in particular metrics, define limits uniquely, if they exist. Thus they select one interpretation implicitly and leave no room for other interpretations. In this paper, we define limits using category theory, and use the mentioned relations between system behaviors explicitly. This resolves the problem of ambiguity in a more controlled way. We introduce a category of prefix orders on executions and partial history preserving maps between them to describe both discrete and continuous branching time dynamics. We prove that in this category all projective limits exist, and illustrate how ambiguity in the definition of limits is resolved using an example. Moreover, we show how various other problems with known topological approaches to taking limits are now resolved, and how the construction of projective limits enables us to approximate continuous time dynamics as a sequence of discrete time systems.|
|15:00-15:30||Luca Aceto, Eugen-Ioan Goriac and Anna Ingolfsdottir|
|Meta SOS - A Maude Based SOS Meta-Theory Framework|
|Meta SOS is a software framework designed to integrate the results from the meta-theory of structural operational semantics (SOS). These results include deriving semantic properties of language constructs just by syntactically analyzing their rule-based definition, as well as automatically deriving sound and ground-complete axiomatizations for languages modulo a notion of behavioural equivalence. This paper describes the Meta SOS framework by blending aspects from the meta-theory of SOS, details of their implementation in Maude, and running examples.|
The workshop proceedings are available as EPTCS 120.
|Notification of acceptance:||July 8, 2013|
|Final version due:||July 21, 2013|
|Johannes Borgström (Uppsala University, SE)|
|Bas Luttik (Eindhoven University of Technology, NL)|
|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)|
The EXPRESS workshops were originally held as meetings of the HCM project EXPRESS, which was active with the same focus from January 1994 till December 1997. The first three workshops were held respectively in Amsterdam (1994, chaired by Frits Vaandrager), Tarquinia (1995, chaired by Rocco De Nicola), and Dagstuhl (1996, co-chaired by Ursula Goltz and Rocco De Nicola). EXPRESS'97, which took place in Santa Margherita Ligure and was co-chaired by Catuscia Palamidessi and Joachim Parrow, was organized as a conference with a call for papers and a significant attendance from outside the project. EXPRESS'98 was held as a satellite workshop of the CONCUR'98 conference in Nice, co-chaired by Ilaria Castellani and Catuscia Palamidessi, and like on that occasion EXPRESS'99 was hosted by the CONCUR'99 conference in Eindhoven, co-chaired by Ilaria Castellani and Björn Victor. The EXPRESS'00 workshop was held as a satellite workshop of CONCUR 2000, Pennsylvania State University, co-chaired by Luca Aceto and Björn Victor. The EXPRESS'01 workshop was held at Aalborg University as a satellite of CONCUR'01 and was co-chaired by Luca Aceto and Prakash Panangaden. The EXPRESS'02 workshop was held at Brno University as a satellite of CONCUR'02 and was co-chaired by Uwe Nestmann and Prakash Panangaden. The EXPRESS'03 workshop was co-located with CONCUR 2003 in Marseille and was co-chaired by Flavio Corradini and Uwe Nestmann. The EXPRESS'04 workshop was co-located with CONCUR 2004 in London and was co-chaired by Jos Baeten and Flavio Corradini. The EXPRESS'05 workshop was co-located with CONCUR 2005 in San Francisco and was co-chaired by Jos Baeten and Iain Phillips. The EXPRESS'06 workshop was co-located with CONCUR 2006 in Bonn and was co-chaired by Roberto Amadio and Iain Phillips. The EXPRESS'07 workshop was co-located with CONCUR 2007 in Lisbon and was co-chaired by Roberto Amadio and Thomas Hildebrandt. The EXPRESS'08 workshop was co-located with CONCUR 2008 in Toronto and was co-chaired by Daniele Gorla and Thomas Hildebrandt. The EXPRESS'09 workshop was co-located with CONCUR 2009 in Bologna and was co-chaired by Sibylle Fröschle and Daniele Gorla. The EXPRESS'10 workshop was co-located with CONCUR 2010 in Paris and was co-chaired by Sibylle Fröschle and Frank Valencia. The EXPRESS'11 workshop was co-located with CONCUR 2011 in Aachen and was co-chaired by Bas Luttik and Frank Valencia.
The first SOS Workshop took place in London as one of the satellite workshops of CONCUR 2004. Subsequently, SOS 2005 occurred in Lisbon as a satellite workshop of ICALP 2005, SOS 2006 in Bonn as a satellite workshop of CONCUR 2006, SOS 2007 in Wroclaw as a satellite workshop of LICS and ICALP 2007, and SOS 2008 in Reykjavik as a satellite workshop of ICALP 2008. SOS 2009 was held as a satellite workshop of CONCUR 2009 in Bologna. SOS 2010 was held as a satellite workshop of CONCUR 2010 in Paris. Finally, SOS 2011 was held as a satellite workshop of CONCUR 2011 in Aachen. A special issue of the Journal of Logic and Algebraic Programming on Structural Operational Semantics appeared in 2004; a special issue of Theoretical Computer Science dedicated to SOS 2005 appeared in 2007, and a special issue of Information & Computation on Structural Operational Semantics inspired by SOS 2006-2007 appeared in 2009.
The first combined EXPRESS/SOS workshop (EXPRESS/SOS 2012) was co-located with CONCUR 2012 in Newcastle upon Tyne, UK and was co-chaired by Bas Luttik and Michel Reniers
|Page maintained by Bas Luttik||Last modified: Thu Aug 15 23:44:11 CEST 2013|