EXPRESS logo EXPRESS/SOS 2015 EXPRESS logo

Combined 22th International Workshop on

Expressiveness in Concurrency

and 12th Workshop on

Structural Operational Semantics

Monday, August 31, 2015
Madrid, Spain
Affiliated with CONCUR 2015

Scope and Topics

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.

Since 2012, the EXPRESS and SOS communities have joined forces and organised a combined EXPRESS/SOS workshop. The past combined workshops were 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.

Topics of interest for this combined workshop include (but are not limited to):

Invited Speaker

Davide Sangiorgi (University of Bologna, Italy)

Programme

9.30-10.30: Davide Sangiorgi (invited presentation)
Bisimulation techniques in probabilistic higher-order languages

TBA

10:30-11:00 Coffee Break
11:00-11:30 Ornela Dardha and Jorge A. Perez
Comparing Deadlock-Free Session Typed Processes

Besides respecting prescribed protocols, communication-centric systems should never 'get stuck'. This important requirement has been expressed by liveness properties such as progress or (dead)lock- freedom. Several typing disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines---and the classes of typed processes they induce.

In this paper, we compare L and K, two classes of deadlock-free, session typed concurrent processes. The class L stands out for its canonicity: it results naturally from interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's usage types, includes processes not typable in other typing systems.

We show that L is strictly included in K. We also identify the precise condition under which L and K coincide. One key observation is that the degree of sharing between parallel processes determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving rewriting procedure of processes in K into processes in L. This procedure suggests that, while effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes.

11.30-12.00: Jovana Dedeic, Jovanka Pantovic and Jorge A. Perez
On Compensation Primitives as Adaptable Processes

We compare mechanisms for compensation handling and dynamic update in calculi for concurrency. These mechanisms are increasingly relevant in the formal specification of dependable communicating systems. Compensations and updates are intuitively similar: both specify how the behavior of a concurrent system changes at runtime in response to an exceptional event. However, calculi with compensations and updates are technically quite different.

In this paper, we investigate the relative expressiveness of these calculi: we develop encodings of core process languages with compensations into a calculus of adaptable processes developed in prior work. The encodings shed light on the (intricate) semantics of compensation handling and its key constructs: compensation scopes, protected blocks, forms of dynamic recovery. Our encodings enable the transference of existing verification and reasoning techniques for adaptable processes to core languages with compensation handling.

12.00-12.30: Pedro R. D'Argenio, Matias D. Lee and Daniel Gebler
SOS rule formats for convex and abstract probabilistic bisimulations
Probabilistic transition system specifications (PTSSs) in the ntμfθ/ntμxθ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the ntμfθ/ntμxθ, we obtain restricted formats that guarantee that three weaker bisimulation equivalences are congruences. We focus on (i) Segala's variant of bisimulation that considers combined transitions, which we call here convex bisimulation; (ii) the bisimulation equivalence resulting from considering Park & Milner's bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here probability obliterated bisimulation; and (iii) a probability abstracted bisimulation, which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we relate these bisimulation equivalences and provide a logic characterization for each of them.
12:30-14:30 Lunch Break
14:30-15.00 Kirstin Peters and Rob Van Glabbeek
Analysing and Comparing Encodability Criteria
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are augmented with quality criteria. There exists a bunch of different criteria and different variants of criteria in order to reason in different settings. This leads to incomparable results. Moreover it is not always clear whether the criteria used to obtain a result in a particular setting do indeed fit to this setting. We show how to formally reason about and compare encodability criteria by mapping them on requirements on a relation between source and target terms that is induced by the encoding function. In particular we analyse the common criteria full abstraction, operational correspondence, divergence reflection, success sensitiveness, and respect of barbs; e.g. we analyse the exact nature of the simulation relation (coupled simulation versus bisimulation) that is induced by different variants of operational correspondence. This way we reduce the problem of analysing or comparing encodability criteria to the better understood problem of comparing relations on processes.
15:00-15:30 Meike Hatzel, Christoph Wagner, Kirstin Peters and Uwe Nestmann
Encoding CSP into CCS
We present two encodings from CSP into asynchronous CSS with name passing and matching. By doing so we discuss two different ways to map between the different synchronisation mechanisms of CSP and CSS. Both encodings satisfy the criteria of Gorla except for compositionality, since both use an additional top-level context. Following the work of Parrow and Sjodin, the first encoding uses a central coordinator and establishes a variant of weak bisimulation between source terms and their translations. The second encoding is decentral, and thus more efficient, but ensures only a form of coupled similarity between source terms and their translations.
15:30-16:00 Reuben Rowe
Encoding the Factorisation Calculus

Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural completeness, i.e. it is able to represent any function on terms definable using pattern matching on arbitrary normal forms. In particular, it admits a term that can decide the structural equality of any two arbitrary normal forms.

Since SF-calculus is combinatorially complete, it is clearly at least as powerful as the more familiar and paradigmatic Turing-powerful computational models of Combinatory Logic and lambda-calculus. Its relationship to these models in the converse direction is less obvious, however. Jay and Given-Wilson have suggested that SF-calculus is strictly more powerful than the aforementioned models, but a detailed study of the connections between these models is yet to be undertaken.

This paper begins to bridge that gap by presenting a faithful encoding of the Factorisation Calculus into the lambda-calculus (and thus also into Combinatory Logic) preserving both reduction and strong normalisation. The existence of such an encoding is a new result. It also suggests that there is, in some sense, an equivalence between the former model and the latter. We discuss to what extent our result constitutes an equivalence by considering it in the context of some previously defined frameworks for comparing computational power and expressiveness.

16:00-16:30 Coffee Break

Proceedings

The workshop proceedings will be available as EPTCS 190.

Registration

Please register for EXPRESS/SOS 2015 via the registration page of CONCUR 2015.

Submissions

TBA We sollicit two types of submissions:

Paper submission is performed through Easychair. The programme committee will select submissions for presentation at the workshop.
The final versions of the accepted papers will be published in the EPTCS (Electronic Proceedings in Theoretical Computer Science). There is limited time between the notification of acceptance of submissions and the deadline for submission of camera-ready versions. Submissions are therefore requested to adhere to the EPTCS-style format. Please also note that after submitting the camera-ready version to EPTCS, usually some interaction between authors, editors and EPTCS staff is needed. At least one author should therefore be available in the week after submitting the camera-ready version. It is recommended that the final version of the paper includes as much as possible proofs and technical material.

Important Dates

Abstract submission: June 17, 2015
Paper submission: June 21, 2015 June 24, 2015
Notification of acceptance: July 19, 2015 July 25,2015
Final version due: July 31, 2015 August 7, 2015

Organizers

Silvia Crafa (University of Padova, Italy)
Daniel Gebler (VU University Amsterdam, The Nederlands)

Programme Committee

Johannes Borgström (Uppsala University, Sweden)
Matteo Cimini (Indiana University, Bloomington, Indiana)
Silvia Crafa (University of Padova, Italy)
Pedro R. D'Argenio (University of Cordoba, Argentina)
Daniel Gebler (VU University Amsterdam, The Nederlands)
Thomas Given-Wilson (Inria, France)
Thomas T. Hildebrandt (IT University of Copenhagen, Denmark)
Daniel Hirschkoff (ENS Lyon, France)
Stefan Milius (University of Erlangen-Nurnberg, Germany)
Mohammad R. Mousavi (Halmstad University, Sweden)
Kirstin Peters (Technical University of Berlin, Germany)
Damien Pous (ENS Lyon, France)
Irek Ulidowski (University of Leister, United Kingdom)

History

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. The second combined EXPRESS/SOS 2013 workshop was co-located with CONCUR 2013 in Buenos Aires, Argentina and was co-chaired by Johannes Borgström and Bas Luttik. The combined EXPRESS/SOS 2014 workshop was co-located with CONCUR 2014 in Rome, Italy and was co-chaired by Johannes Borgstrom and Silvia Crafa.

Page maintained by Silvia Crafa