Published: 23rd August 2021|
|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|
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:
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,
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 () 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).
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.