Published: 23rd August 2021
DOI: 10.4204/EPTCS.339
ISSN: 2075-2180

EPTCS 339

Proceedings Combined 28th International Workshop on
Expressiveness in Concurrency
and 18th Workshop on
Structural Operational Semantics
Paris, France (online event), 23rd August 2021

Edited by: Ornela Dardha and Valentina Castiglioni

Preface
Invited Presentation: Semantic Soundness for Language Interoperability
Amal Ahmed
1
Invited Presentation: Infinite Choice and Probability Distributions. An Open Problem: The Real Hotel
Jan Friso Groote
2
Invited Presentation: Probabilistic Verification of Concurrent Autonomous Systems
David Parker
9
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
Eric Alsmann, Florian Bruse and Martin Lange
10
A Game Characterization for Contrasimilarity
Benjamin Bisping and Luisa Montanari
27
Language Transformations in the Classroom
Matteo Cimini and Benjamin Mourad
43
Minimal Translations from Synchronous Communication to Synchronizing Locks
Manfred Schmidt-Schauß and David Sabel
59
On Decidability of the Bisimilarity on Higher-order Processes with Parameterization
Xian Xu and Wenbo Zhang
76

Preface

This volume contains the proceedings of EXPRESS/SOS 2021, the Combined 28th International Workshop on Expressiveness in Concurrency (EXPRESS) and the 18th 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 2021 was held affiliated to CONCUR 2021, as part of QONFEST 2021. Due to the Covid-19 pandemic, all the events of QONFEST 2021, including our combined workshop, were held online as virtual events.

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

This volume contains revised versions of the five full papers selected by the Program Committee, as well as (extended) abstracts associated to the following three invited presentations:

Moreover, the scientific program of the workshop was nicely complemented by the following short paper selected by the Program Committee:

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 2021 and the QONFEST 2021 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.

Valentina Castiglioni and Ornela Dardha,
August 2021

Program Committee

Additional Reviewers

Sergueï Lenglet,
Srdjan Popov

Semantic Soundness for Language Interoperability

Amal Ahmed (Northeastern University, Boston, USA)

Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate features can make interoperability fraught, as type-based invariants from one language can easily be violated in the other. In their seminal 2007 paper, Matthews and Findler ([1]) proposed a multi-language construction that augments the interoperating languages with a pair of boundaries that allow code from one language to be embedded in the other. While this technique has been widely applied, their source-level interoperability doesn't reflect practical implementations, where the behavior of interaction is only defined after compilation to a common target, and any safety must be ensured by target-level ''glue code''.

In this talk, I will present a novel framework for the design and verification of sound language interoperability that follows an interoperation-after-compilation strategy. Language designers specify what data can be converted between types of the two languages $A$ and $B$ via a convertibility relation $\tau_A \sim \tau_B$ (''$\tau_A$ is convertible to $\tau_B$'') and specify target-level glue code implementing the conversions. Then, by giving a semantic model of source-language types as sets of target-language terms, we can establish not only the meaning of our source types, but also soundness of conversions: i.e., whenever $\tau_A \sim \tau_B$, the corresponding pair of conversions (glue code) convert target terms that behave like $\tau_A$ to target terms that behave like $\tau_B$, and vice versa. With this, we can prove semantic type soundness for the entire system. I will illustrate the framework via a series of case studies and show how the approach helps designers better take advantage of efficient enforcement mechanisms and opportunities for sound sharing that may not be obvious in a setting divorced from implementations.

This is joint work with Daniel Patterson, Noble Mushtak, and Andrew Wagner.

This talk describes work supported in part by the National Science Foundation (NSF grants CCF-1816837 and CCF-1453796).

References

  1. Jacob Matthews & Robert Bruce Findler (2007): Operational Semantics for Multi-Language Programs. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposyum on Principles of Programming Languages, POPL '07, Association for Computing Machinery, New York, NY, USA, pp. 3 – 10 doi:10.1145/1190216.1190220.

Probabilistic Verification of Concurrent Autonomous Systems

David Parker (University of Birmingham, UK)

Modern computing systems increasingly involve autonomous agents acting concurrently, which may either compete or collaborate to achieve their own objectives. Designing these systems is a challenge, particularly when they need to operate in uncertain or adversarial environments. Probabilistic model checking is a technique for formal modelling and analysis of such systems. Given a quantitative correctness specification expressed in temporal logic, it can either verify that the system behaves as intended, or synthesise a controller which guarantees that this will be the case.

This tutorial explains some of the recent advances in this area, with a particular focus on the use of stochastic games to verify multi-agent systems. This includes concurrent stochastic games, for more realistic modelling of agents acting concurrently, and Nash equilibria, for more expressive specification of agents with differing objectives. We summarise the key underlying theory and algorithms, and illustrate the applicability of the techniques with examples from a range of applications.