Published: 22nd November 2024 DOI: 10.4204/EPTCS.412 ISSN: 2075-2180 |
Preface Georgiana Caltais and Cinzia Di Giusto | |
Invited Presentation: Reverse My Computation? But Why? Clément Aubert | 1 |
Functional Array Programming in an Extended Pi-Calculus Hans Hüttel, Lars Jensen, Chris Oliver Paulsen and Julian Teule | 2 |
Synchronisability in Mailbox Communication Cinzia Di Giusto, Laetitia Laversa and Kirstin Peters | 19 |
Semantics for Linear-time Temporal Logic with Finite Observations Rayhana Amjad, Rob van Glabbeek and Liam O'Connor | 35 |
Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings Marco Bernardo, Andrea Esposito and Claudio A. Mezzina | 51 |
One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics Benjamin Bisping and David N. Jansen | 71 |
This volume contains the proceedings of EXPRESS/SOS 2024, the Combined 31th International Workshop on Expressiveness in Concurrency (EXPRESS) and the 21th 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 2024 was held affiliated to CONCUR 2024, as part of CONFEST 2024, in Calgary, Canada.
The topics of interest for the EXPRESS/SOS workshop include:
This volume contains revised versions of the 5 full papers, selected by the Program Committee, as well as the abstract of the invited presentation by Clément Aubert.
We would like to thank the authors of the submitted papers, the invited speaker, the members of the program committee, and their subreviewers for their contribution to both the meeting and this volume. We also thank the CONFEST 2024 organising 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 Cinzia Di Giusto, October 2024
A typical computer user knows the difference between what can be undone on a computer, and what cannot. They may be familiar with the "undo" feature of text editors but understand the impossibility of recovering an unsaved document after an emergency shutdown. Creating programs guaranteeing that any action can be undone requires to design and implement reversible programming languages. While such languages come with interesting built-in security features (because any past action can be investigated), they also raise challenges when it comes to concurrency. Indeed, undoing an action that involved synchronization between multiple actors requires all actors to agree to undo said action. Process algebras offer an interesting frame to study reversible computation, and reciprocally. Enriching process algebras such as CCS with memory, identifiers or keys, allowed to represent reversible computation, and in turn helped gained a finer understanding of causality, bisimulations, and other "true concurrency" notions. This talk offers to briefly motivate the interests of reversible computation, and to discuss the new lights it shed on process algebras.