EXPRESS/SOS 2015Combined 22th International Workshop on
Expressiveness in Concurrencyand 12th Workshop on
Structural Operational Semantics
Affiliated with CONCUR 2015
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):
|Davide Sangiorgi (University of Bologna, Italy)|
|9.30-10.30:||Davide Sangiorgi (invited presentation)|
|Bisimulation techniques in probabilistic higher-order languages|
|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.|
|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.|
|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.
The workshop proceedings will be available as EPTCS 190.
TBA We sollicit two types of submissions:
|Abstract submission:||June 17, 2015|
|Notification of acceptance:|
|Final version due:|
|Silvia Crafa (University of Padova, Italy)|
|Daniel Gebler (VU University Amsterdam, The Nederlands)|
|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)|
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|