Published: 14th September 2023
DOI: 10.4204/EPTCS.387
ISSN: 2075-2180


Proceedings Combined 30th International Workshop on
Expressiveness in Concurrency
and 20th Workshop on
Structural Operational Semantics
Antwerp, Belgium, 18th September 2023

Edited by: Claudio Antares Mezzina and Georgiana Caltais

Georgiana Caltais and Claudio Antares Mezzina
Invited Presentation: Timed Actors and Their Formal Verification
Marjan Sirjani and Ehsan Khamespanah
Invited Contribution: EXPRESSing Session Types
Ilaria Castellani, Ornela Dardha, Luca Padovani and Davide Sangiorgi
Invited Contribution: The Way We Were: Structural Operational Semantics Research in Perspective
Luca Aceto, Pierluigi Crescenzi, Anna Ingólfsdóttir and Mohammad Reza Mousavi
Accepted Abstract: Comparing Deadlock-Free Session Processes, Revisited (Short Paper)
Channa Dias Perera and Jorge A. Pérez
A Cancellation Law for Probabilistic Processes
Rob van Glabbeek, Jan Friso Groote and Erik de Vink
A Lean-Congruence Format for EP-Bisimilarity
Rob van Glabbeek, Peter Höfner and Weiyou Wang
Using Pi-Calculus Names as Locks
Daniel Hirschkoff and Enguerrand Prebet
Deriving Abstract Interpreters from Skeletal Semantics
Thomas Jensen, Vincent Rébiscoul and Alan Schmitt
Parallel Pushdown Automata and Commutative Context-Free Grammars in Bisimulation Semantics (Extended Abstract)
Jos C. M. Baeten and Bas Luttik
Quantifying Masking Fault-Tolerance via Fair Stochastic Games
Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi and Luciano Putruele
CRIL: A Concurrent Reversible Intermediate Language
Shunya Oguchi and Shoji Yuen


This volume contains the proceedings of EXPRESS/SOS 2023, the Combined 30th International Workshop on Expressiveness in Concurrency (EXPRESS) and the 20th Workshop on Structural Operational Semantics (SOS).

The first edition of EXPRESS/SOS was held in 2012, when the EXPRESS and SOS communities decided to organise an annual combined workshop bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. Since then, EXPRESS/SOS was held as one of the affiliated workshops of the International Conference on Concurrency Theory (CONCUR). Following this tradition, EXPRESS/SOS 2023 was held affiliated to CONCUR 2023, as part of CONFEST 2023, in Antwerp, Belgium. This year's edition marks two important anniversaries: EXPRESS turns 30 and SOS 20. In celebration of this dual anniversary, and to offer an overview of the past and future of these workshops, we are delighted to present two contributions from distinguished members of both communities in these proceedings:

The topics of interest for the EXPRESS/SOS workshop include (but are not limited to):

This volume contains revised versions of the 7 full papers and one abstract, selected by the Program Committee, as well as the following two invited papers, related to the topics presented by our invited speakers: We would like to thank the authors of the submitted papers, the invited speakers, the members of the program committee, and their subreviewers for their contribution to both the meeting and this volume. We also thank the CONCUR 2023 and the CONFEST 2023 organizing committees for hosting the workshop. Finally, we would like to thank our EPTCS editor Rob van Glabbeek for publishing these proceedings and his help during the preparation.

Georgiana Caltais and Claudio Antares Mezzina,
August 2023

Program Committee

Additional Reviewers

Andrea Esposito, Univerity of Urbino, Italy

Comparing Deadlock-Free Session Processes, Revisited (Short Paper)

Channa Dias Perera (University of Groningen)
Jorge A. Pérez (University of Groningen)

We are interested in type systems that enforce the deadlock-freedom property for pi-calculus processes. Several different type systems have been proposed, which consider different dialects of the pi-calculus and use different insights to rule out the circular dependencies that induce deadlocks.

Prior work by Dardha and P\'erez rigorously compared two kinds of type systems: (i) type systems based on priorities, as pioneered by Kobayashi; and (ii) type systems based on Curry-Howard interpretations of linear logic propositions as session types. They show that the former subsume the latter, i.e., type systems based on linear logic induce a class of deadlock-free processes that is strictly included in the class induced by priority-based systems. Dardha and P\'erez's comparison considers languages with similar (reduction) semantics, which admit the same definition of deadlock-freedom.

In our presentation, we report on ongoing work aimed at extending Dardha and P\'erez's classification to consider a class of deadlock-free processes with a self-synchronizing transition semantics, which is induced by presentations of linear logic based on hypersequents. Integrating this class into a formal comparison is interesting but subtle, as trivially deadlocked-processes in Dardha and P\'erez's setting actually enjoy the deadlock-freedom property under the self-synchronizing regime.