Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics
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):
Mohammad R. Mousavi (University of Leicester, UK and Halmstad University, Sweden)
Rob van Glabbeek (CSIRO, Sydney, Australia)
| Time | EXPRESS/SOS |
| 9:00 | Registration |
| 9:20 | Opening |
| 9:30 | Invited Talk SOS with Data: Bisimulation, Rule Formats, and Axiomatization Mohammad R. Mousavi The notion of store or data is intrinsic to the semantic description of many specification and programming languages. The configuration of the operational state of many timed, hybrid, or distributed formalisms also contains different forms of store, e.g., for recording the time, the valuation of continuous variables, or locations and distribution of processes. In this talk, we study 3 notions of bisimulation that are defined on semantics with an explicit notion of data and store and compare their applicability. Then we introduce rule formats for these 3 notions and finally, we present initial results about generating ground-complete axiomatizations from SOS specification with data. |
| 10:30 | Short Paper Delayed-choice semantics for pomset families and message sequence graphs Clemens Dubslaff Christel Baier Message sequence charts (MSCs) are diagrams widely used to describe communication scenarios. Their higher-order formalism is provided by graphs over MSCs, called message sequence graphs (MSGs), which naturally induce a non-interleaving linear-time semantics in terms of a pomset family. Differently, the operational semantics for MSGs was standardized by the ITU-T as an interleaving branching-time semantics using a process-algebraic approach. A key ingredient in the latter semantics is delayed choice, formalizing that choices between communication scenarios are only made when they are inevitable. In this presentation, we propose an alternative approach towards branching-time semantics that applies the concept of delayed choice directly on pomset families. First, we introduce transition-system semantics for pomset families where global states comprise cuts of pomsets represented either by suffixes and prefixes of family members. Second, we provide a flow-event-structure semantics for MSGs compatible with delayed choice those benefit is to maintain the causal dependencies of events provided by the standard pomset semantics for MSGs. |
| 11:00 | Coffee Break |
| 11:30 | CCS with Signals, Used for Analysing Mutual Exclusion Victor Dyseryn Rob van Glabbeek Peter Höfner In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems contra-intuitive. We introduce a signalling operator, which can be combined with CCS or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion. In this framework we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, and less realistic, assumptions on the underlying memory model. Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees James Ferlez Rance Cleaveland Steven Marcus In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importantly, this logic suggests a strong relationship between (weak) bisimulation for GSTs and ordinary bisimulation for Synchronization Trees (STs). We demonstrate that this relationship can be used to define the GST analog for image-finiteness of STs. Furthermore, we demonstrate that certain maximal Hennessy-Milner classes of STs have counterparts in maximal Hennessy-Milner classes of GSTs with respect to GST weak bisimulation. We also exhibit some interesting characteristics of these maximal Hennessy-Milner classes of GSTs. Using Session Types for Reasoning About Boundedness in the Pi-Calculus Hans Hüttel Depth-bounded and name-bounded processes are π-calculus processes for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction sequence for P contains successor processes with at most k active nested restrictions. P is name-bounded at level k if every reduction sequence for P contains successor pro- cesses with at most k active bound names. We use binary session types to formulate a type system that gives a sound characterization of depth-boundedness: If a process is well-typed, it is depth-bounded. Next, we show how to strengthen the type system to ensure that any well-typed process will also be name-bounded. |
| 13:00 | Lunch Break |
| 14:30 | Invited Tutorial Rule Formats in Structural Operational Semantics Rob van Glabbeek This tutorial presents an introduction to some key concepts in structural operational semantics, focusing on congruence formats. In particular I will define the ntyft/ntyxt format, and state how it guarantees that the bisimulation preorder is a precongruence. In doing so, I consider the congruence property not only for operators, but also for recursion. Congruence formats also exists for many preorders and equivalences coarser than bisimilarity, and I will give a representative example. I briefly list rule formats for other properties that being a congruence, and generalisations to semantics featuring time, probabilities and data. |
| 15:30 | Short Paper Branching Cell Decomposition, Confusion Freeness and Probabilistic Nets Roberto Bruni Hernan Melgratti Ugo Montanari The problem addressed is a foundational one: can concurrency and general probabilistic distributions coexist in Petri nets? If so, under which circumstances? We provide a positive answer for the case of finite occurrence nets (also in the presence of confusion): given any such net we show how to construct another net where probability distributions can be assigned unambiguously to any decision point and independent distributions are assigned to concurrent decisions. Our construction is structural and compositional and it is shown to match the one recently proposed by Abbes and Benveniste for event structures. |
| 16:00 | Coffee Break |
| 16:30 | Sequential composition in the presence of intermediate termination Jos Baeten Bas Luttik Fei Yang The standard operational semantics of the sequential composition operator gives rise to unbounded branching and forgetfulness when transparent process expressions are put in sequence. Due to transparency, the correspondence between context-free and push-down processes fails modulo bisimilarity, and it is not clear how to specify an always terminating half counter. We propose a revised operational semantics for the sequential composition operator in the context of intermediate termination. With the revised operational semantics, we eliminate transparency. As a consequence, we establish a correspondence between context-free processes and pushdown processes. Moreover, we prove the reactive Turing powerfulness of TCP with iteration and nesting with the revised operational semantics for sequential composition. Reversing Imperative Parallel Programs James Hoey Irek Ulidowski Shoji Yuen We propose two approaches for reversing imperative programs. Firstly, we produce both an augmented version and a corresponding inverted version of the original program. Augmentation saves reversal information into an auxiliary data store, maintaining segregation between this and the program state, while never altering the data store in any other way than that of the original program. Inversion uses this information to revert the final program state to the state as it was before execution. We prove that augmentation and inversion work as intended, and illustrate our approach with several examples. We also suggest a modification to our first approach to support non-communicating parallelism. Execution interleaving introduces a number of challenges, each of which our second approach overcomes. We define annotation and redefine inversion to use a sequence of statement identifiers, making the interleaving order deterministic in reverse. Distributive Laws for Monotone Specifications Jurriaan Rot Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications - that disallow negative premises - do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation. |
| 18:00 | Closing |
The workshop proceedings are available as EPTCS 222.
Please register for EXPRESS/SOS 2017 via the registration page of CONCUR 2017.
We solicit 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.
| Paper submission: | |
| Notification date: | July 31 |
| Camera ready version: | |
| Workshop: | September 4 |
Kirstin Peters (TU Berlin, Germany)
Simone Tini (Università degli Studi dell’Insubria, Italy)
Giorgio Bacci (Aalborg University, Denmark)
Ilaria Castellani (INRIA, France)
Silvia Crafa (Università di Padova, Italy)
Pedro R. D’Argenio (Universidad Nacional de Córdoba, Argentina)
Erik de Vink (Eindhoven University of Technology, The Netherlands)
Álvaro García-Pérez (IMDEA, Spain)
Bartek Klin (Warsaw University, Poland)
Stephan Mennicke (TU Braunschweig, Germany)
Kirstin Peters (TU Berlin, Germany)
Johannes Åman Pohjola (Chalmers University of Technology, Sweden)
Pawel Sobocinski (University of Southampton, UK)
Simone Tini (Università degli Studi dell’Insubria, Italy)
Irek Ulidowski (University of Leicester, UK)
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. The next year the combined EXPRESS/SOS 2015 workshop was co-located with CONCUR 2015 in Madrid, Spain and was co-chaired by Silvia Crafa and Daniel Gebler. The combined EXPRESS/SOS 2016 workshop was co-located with CONCUR 2016 in Québec City, Canada and was co-chaired by Daniel Gebler and Kirstin Peters.