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

# Proceedings Combined 28th International Workshop onExpressiveness 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):

• expressiveness and rigorous comparisons between models of computation;
• expressiveness and rigorous comparisons between programming languages and models;
• logics for concurrency;
• analysis techniques for concurrent systems;
• 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.

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:

• Semantic soundness for language interoperability, by Amal Ahmed (Northeastern University, USA)
• Infinite choice and probability distributions. An open problem: The real hotel, by Jan Friso Groote (TU Eindhoven, The Netherlands)
• Probabilistic verification of concurrent autonomous systems, by Dave Parker (University of Birmingham, UK)
Moreover, the scientific program of the workshop was nicely complemented by the following short paper selected by the Program Committee:
• Minimal session types for the $\pi$-calculus, by Alen Arslanagic, Anda-Amelia Palamariuc and Jorge A. Pérez

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

• Ahmed Bouajjani, IRIF and University of Paris Diderot, France
• Valentina Castiglioni (co-chair), Reykjavik University, Iceland
• Ornela Dardha (co-chair), University of Glasgow, UK
• Yuxin Deng, East China Normal University, China
• David de Frutos-Escrig, Complutense University of Madrid, Spain
• Silvia Ghilezan, University of Novi Sad, Serbia
• Paola Giannini, University of Piemonte Orientale, Italy
• Karoliina Lehtinen, CNRS, Aix-Marseille Université, LIS, France
• Hernan Melgratti, University of Buenos Aires, Argentina
• Valeria de Paiva, Samsung Research America, USA, and University of Birmingham, UK
• Tatjana Petrov, University of Konstanz, Germany
• Sabina Rossi, University Ca' Foscari Venice, Italy
• Jurriaan Rot, Radboud University, The Netherlands

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.