Combined 31st International Workshop on

Expressiveness in Concurrency

and 21st Workshop on

Structural Operational Semantics

Monday September 9, 2024
Calgary
Affiliated with CONCUR 2024
(as part of CONFEST 2024)

Scope and Topics

The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.

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

expressiveness and rigorous comparisons between models of computation (process algebras, event structures, Petri nets, rewrite systems)
expressiveness and rigorous comparisons between programming languages and models (distributed, component-based, object-oriented, service-oriented)
logics for concurrency (modal logics, probabilistic and stochastic logics, temporal logics and resource logics)
analysis techniques for concurrent systems
theory of structural operational semantics (metatheory, category-theoretic approaches, congruence results)
comparisons between structural operational semantics and other formal semantic approaches
applications and case studies of structural operational semantics
software tools that automate, or are based on, structural operational semantics

We especially welcome contributions bridging the gap between the above topics and neighbouring areas, such as:

computer security
multi-agent systems
programming languages and formal verification
reversible computation
knowledge representation

Invited Speakers

Clément Aubert

Dr. Clément Aubert is an Associate Professor in the School of Computer and Cyber Sciences and an associate faculty member of the Graduate School at Augusta University, USA. He obtained his B.Sc. degree in Philosophy from the University of Paris 1, his M.S. degree in Mathematics from the University of Paris 7, and his PhD in Computer Science from the University of Paris 13. His current research interests are in formal methods for concurrent systems, type systems for the study of complexity, and reversible concurrent systems.

Submissions

We solicit two types of submissions:

Full papers of up to 15 pages excluding references in EPTCS style.
(presented at the workshop and included in the proceedings)
Short papers of up to 5 pages excluding references in EPTCS style.
(presented at the workshop, but not included in the proceedings)

Submission is performed through the EXPRESS/SOS 2024 EasyChair server.

Important Dates

Monday June 24 July 1, 2024 (AoE, extended deadline)

Paper submission

Monday August 12, 2024

Notification to authors

Wednesday October 9, 2024

Final version due (Post-proceedings)

Proceedings

The workshop proceedings will be published in Electronic Proceedings in Theoretical Computer Science .

We are planning a special issue with selected papers from EXPRESS/SOS 2023 and EXPRESS/SOS 2024. More information will follow closer to the event.

Registration

EXPRESS/SOS 2024 is planned as a physical event,
with certain support for remote presence, for speakers and other participants who are unable or unwilling to come.
To register for EXPRESS/SOS 2024, please visit the registration page of CONFEST 2024.

Programme

Time	Authors	Details
08:50 - 09:00		Opening
09:00 - 10:00	Elli Anastasiadi	Joint invited talk with TRENDS - A view into hyperlogics Abstract: Hyperproperties are properties of sets of traces. Compared to simple trace properties, their satisfaction can depend on the traces in a set interacting with each other or, for example, the average of some quantity along individual traces. Temporal hyperlogics emerged to capture such properties by allowing the use of quantifiers. These logics allowed for viewing the verified set of traces independently of what system might be producing it, and this unlocked the possibility of using hyperlogics for expressing, for example, consensus-type properties. The verification for these two approaches, one where it is the set of traces produced by a single system and one where it is not, are also orthogonal. In this talk, we will set the foundations of this topic, understand the key attributes that make hyperlogics so fascinating, and look into some current trends.
10:00 - 10:30		Coffee break
10:30 - 11:00	Hans Hüttel, Lars Jensen, Chris Oliver Paulsen and Julian Jørgensen Teule	Functional Array Programming in an Extended Pi-Calculus Abstract: We study the data-parallel language BUTF, inspired by the FUTHARK language for array programming. We give a translation of BUTF into a version of the π-calculus with broadcasting and labelled names. The translation is both complete and sound. Moreover, we propose a cost model by annotating translated BUTF processes. This is used for an asymptotic complexity analysis of the translation.Remote talk
11:00 - 12:00	Simone Tini	Joint invited talk with TRENDS - Robustness Analysis in Biological Systems Abstract: We present the theory of the tool Bio-STARK, which allows for the simulation and analysis of biological systems. In particular, we show how the tool allows us to verify robustness properties in systems biology, by capturing the effects of (unpredictable) perturbations on species in biochemical networks, as well as on the oscillatory behaviour of gene regulatory networks.
12:00 - 12:30	Rose Bohrer and Hannah Gommerstadt	Linear Temporal Monitors for Session Types Abstract: We explore the application of finite-trace linear temporal logic in monitoring of session-typed languages. To enable this, we establish a bidirectional translation between session types and finite automata, to which linear temporal logic can be translated. We use a classical, synchronous, binary session type system. Using stacks and auctions as examples, we demonstrate the utility of monitoring temporal invariants beyond the invariants represented by standard session types. Remote talk
12:30 - 14:00		Lunch
14:00 - 15:00	Clément Aubert	Invited talk - Reverse My Computation? But Why? Abstract: 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 motivates the interests of reversible computation, and to discuss the new lights it shed on process algebras. Remote talk
15:00 - 15:30	Cinzia Di Giusto, Laetitia Laversa and Kirstin Peters	Synchronisability in Mailbox Communication Abstract: We revisit the problem of synchronisability for communicating automata, i.e., whether the language of send messages for an asynchronous system is the same as the language of a synchronous one. The un/decidability of the problem depends on the specific asynchronous semantics considered as well as the topology (the communication flow) of the system.Synchronisability is known to be undecidable under the peer-to-peer semantics, while it is still an open problem for mailbox communication. The problem was shown to be decidable for ring topologies. In this paper, we show that when restricting to automata with accepting states, synchronisability is undecidable under the mailbox semantics, this result is obtained by resorting to the Post Correspondence problem. In an attempt to solve the general problem, we also show that synchronisability is decidable for tree topologies (where, as well as for rings, peer-to-peer coincides with mailbox semantics). We also discuss synchronisability for multitrees in the mailbox setting.
15:30 - 16:00		Coffee Break
16:00 - 16:30	Rayhana Amjad, Rob van Glabbeek and Liam O'Connor.	Semantics for Linear-time Temporal Logic with Finite Observations Abstract: LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.
16:30 - 17:00	Marco Bernardo and Claudio Antares Mezzina.	Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings Abstract: Reversible systems exhibit both forward computations and backward computations, where the aim of the latter is to undo the effects of the former. Such systems can be compared via forward-reverse bisimilarity as well as its two components, i.e., forward bisimilarity and reverse bisimilarity. The properties of these equivalences have already been studied in the setting of sequential processes. In this paper we address concurrent processes and investigate compositionality and axiomatizations of forward bisimilarity, which is interleaving, and reverse and forward-reverse bisimilarities, which are truly concurrent. To uniformly derive expansion laws for the three equivalences, we develop encodings based on the proved trees approach. In the case of reverse and forward-reverse bisimilarities, we show that every action prefix in the expansion needs to be extended with the backward ready set of the state reached by the corresponding transition. Furthermore, we prove that forward-reverse bisimilarity augmented with a clause for backward ready multisets equality corresponds to hereditary history-preserving bisimilarity, thereby providing for the latter equivalence a new axiomatization as well as an operational characterization.
17:00 - 17:30	Benjamin Bisping and David N. Jansen.	One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics Abstract: We provide the first generalized game characterization of van Glabbeek’s linear-time–branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy–Milner logic that we characterize by eight dimensions of formula expressiveness.
17:30 - 17:40		Closing

Programme Committee

Georgiana Caltais , (co-chair) University of Twente, The Netherlands
Cinzia Di Giusto , (co-chair) Université Côte d'Azur, France / CNRS, France
Elli Anastasiadi Uppsala University, Sweden
Matteo Cimini University of Massachusetts Lowell, USA
Wan Fokkink , Vrije Universiteit Amsterdam, The Netherlands
Adrian Francalanza University of Malta
Fatemeh Ghassemi University of Tehran, Iran
Lorenzo Gheri University of Liverpool
Eva Graversen University of Southern Denmark, Denmark
Jean Krivine CNRS, Paris, France
Sergueï Lenglet Université de Lorraine
Doriana Medic University of Turin, Italy
Maurizio Murgia Gran Sasso Science Institute
António Ravara Universidade NOVA de Lisboa, Portugal
Marjan Sirjani Malardalen University, Sweden
Felix Stutz University of Luxembourg, Luxembourg
Emilio Tuosto Gran Sasso Science Institute, Italy
Frank Valencia LIX, Ecole Polytechnique, France
Daniele Varacca LACL - Université Paris Est Créteil, France
Gianluigi Zavattaro Department of Computer Science and Engineering - University of Bologna, Italy

Organisers

For questions, please contact:

Georgiana Caltais , University of Twente, The Netherlands
Cinzia Di Giusto , Université Côte d'Azur, France

History

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. This year marks the 30th edition of EXPRESS and the 20th edition of SOS.

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.

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 Borgström 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. The combined EXPRESS/SOS 2017 workshop was co-located with CONCUR 2017 in Berlin, Germany and was co-chaired by Kirstin Peters and Simone Tini. The combined EXPRESS/SOS 2018 workshop was co-located with CONCUR 2018 in Beijing, China and was co-chaired by Jorge Perez and Simone Tini. The combined EXPRESS/SOS 2019 workshop was co-located with CONCUR 2019 in Amsterdam, The Netherlands and was co-chaired by Jorge Perez and Jurriaan Rot. The combined EXPRESS/SOS 2020 workshop was co-located with CONCUR 2020 in Vienna, Austria, held on-line, and was co-chaired by Ornela Dardha and Jurriaan Rot. The combined EXPRESS/SOS 2021 workshop was co-located with CONCUR 2021, as part of CONFEST 2021, in Paris, France, held on-line, and was co-chaired by Valentina Castiglioni and Ornela Dardha. The combined EXPRESS/SOS 2022 workshop was co-located with CONCUR 2022, as part of CONFEST 2022, in Warsaw, Poland, and was co-chaired by Valentina Castiglioni and Claudio Antares Mezzina. The combined EXPRESS/SOS 2023 workshop was co-located with CONCUR 2023, as part of CONFEST 2023, in Antwerp, Belgium, and was co-chaired by Georgiana Caltais and Claudio Antares Mezzina.

In these years some journal special issues dedicated to the mentioned events have been organised. A special issue of 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. Special issues devoted to EXPRESS 2010 and 2011 were both published in the journal Mathematical Structures in Computer Science. A special issue of the Acta Informatica dedicated to EXPRESS/SOS 2016-2017 appeared in 2020. A special issue of Information & Computation dedicated to EXPRESS/SOS 2018 appeared in 2019. A special issue of Information & Computation dedicated to EXPRESS/SOS 2021-2022 appeared in 2023.