CONCUR Test-Of-Time Award 2022

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, Davide Sangiorgi

► To cite this version:

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, Davide Sangiorgi. CONCUR Test-Of-Time Award 2022. 33rd International Conference on Concurrency Theory (CONCUR 2022), Bartek Klin, Slawomir Lasota, Anca Muscholl, Sep 2022, Warsaw (Poland), Poland. pp.1:1-1:3, 10.4230/LIPIcs.CONCUR.2022.1 . hal-03970965

HAL Id: hal-03970965

https://inria.hal.science/hal-03970965

Submitted on 3 Feb 2023

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
CONCUR Test-Of-Time Award 2022

Ilaria Castellani ☐

INRIA Sophia Antipolis Méditerranée, France

Paul Gastin ☐

Université Paris-Saclay, ENS Paris-Saclay, CNRS, France

Orna Kupferman ☐

School of Computer Science and Engineering, Hebrew University of Jerusalem, Israel

Mickael Randour ☐

F.R.S.-FNRS & UMONS - Université de Mons, Belgium

Davide Sangiorgi ☐

Department of Computer Science, University of Bologna, Italy

Abstract

This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four
papers that received the Award in 2022.

2012 ACM Subject Classification Theory of computation → Concurrency

Keywords and phrases CONCUR Test-of-Time Award

Digital Object Identifier 10.4230/LIPIcs.CONCUR.2022.1

Category Invited Paper

**Acknowledgements** We thank Javier Esparza (chair of the CONCUR Steering Committee), Pedro d'Argenio and Ana Sokolova (chair and secretary of the IFIP Working Group 1.8 on Concurrency Theory), and Bartek Klin, Sławomir Lasota and Anca Muscholl (chairs of the CONCUR 2022 Programme Committee) for their assistance throughout our work as a jury for this year's award.

1 Introduction

The CONCUR Test-of-Time Award was established in 2020 by the Steering Committee of the CONCUR conference and by the IFIP Working Group 1.8 on Concurrency Theory. Its purpose is to recognise important achievements in Concurrency Theory that were published at CONCUR and have stood the test of time. At its normal pace, starting from 2024, the CONCUR Test-of-Time Award will be attributed every other year, during the CONCUR conference, to one or two papers published in the 4-year period from 20 to 17 years earlier. In the transient period from 2020 to 2023, on the other hand, two such awards are attributed every year, in order to catch up with papers published in the first fifteen years of the conference, namely between 1990 and 2004. At CONCUR 2020 two awards were given, each rewarding two papers published in the period 1990–1995. Similarly, at CONCUR 2021 two awards were given, each rewarding two papers published in the period 1994–1999.

We had the honour to serve as members of the third CONCUR Test-of-Time Award Jury. All papers published at CONCUR in the period 1998-2003 were eligible, and we were asked to select one or two papers for each of the two periods 1998-2001 and 2000-2003 (the overlap between the two periods allowing for some variability in the number of selected papers over the years). After setting up a shortlist of candidate papers and discussing their relative merits and influence on the CONCUR research community and beyond, we selected the four papers described below for the Award, out of a number of excellent candidates.

<figure><img src="image_2.png" /></figure>

© Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi;
licensed under Creative Commons License CC-BY 4.0

33rd International Conference on Concurrency Theory (CONCUR 2022).

Editors: Bartek Klin, Sławomir Lasota, and Anca Muscholl; Article No. 1; pp. 1:1–1:3

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
The presentation of the Award will take place during CONCUR 2022, the 33th edition of the CONCUR conference, which is co-chaired by Bartek Klin, Sławomir Lasota and Anca Muscholl, and will be held in Warsaw.

## 2 The Award Winning Contributions

### 2.1 Period 1998–2001

- Christel Baier, Joost-Pieter Katoen & Holger Hermanns. *Approximate symbolic model checking of continuous-time Markov chains*. CONCUR 1999.

https://doi.org/10.1007/3-540-48320-9_12

This paper presents the first symbolic model-checking algorithm for systems that combine probabilistic and real-time behaviours. Specifically, the model-checking algorithm handles real-time probabilistic systems, modelled by continuous-time Markov chains systems, and specifications in CSL – a branching and continuous-time stochastic logic. This setting significantly extends the scope of systems to which automatic model-checking can be applied. Beyond the new model-checking algorithm, the paper introduces several ideas that have been extensively used since their introduction in the paper. This includes a reduction from a quantitative model-checking problem to the problem of solving a system of equations, as well as a generalisation of BDDs to MTDDs (multi-terminal decision diagrams, which allow both Boolean and real-valued variables), which enables symbolic reasoning.

- Franck Cassez & Kim Larsen. *The Impressive Power of Stopwatches*. CONCUR 2000.

https://doi.org/10.1007/3-540-44618-4_12

This paper studies the expressive power of timed automata enriched with stopwatches and unobservable behaviours. Surprisingly, it is proved with smart constructions that this seemingly mild extension already reaches the full expressive power of linear hybrid automata, a very powerful model using a finite discrete control together with continuous variables, linear guards and linear updates. An important consequence is the reduction of the reachability analysis of linear hybrid automata to that of stopwatch automata. Even though both problems are undecidable, approximate reachability for stopwatch automata is easier to develop and implement. Stopwatch automata find another very important application in the field of scheduling problems for timed pre-emptive systems.

### 2.2 Period 2000–2003

- James J. Leifer & Robin Milner. *Deriving Bisimulation Congruences for Reactive Systems*. CONCUR 2000.

https://doi.org/10.1007/3-540-44618-4_19

This paper presents a uniform approach for deriving a Labelled Transition System (LTS) semantics from a reduction semantics, in such a way that the resulting bisimilarity is a congruence. LTS semantics, inspired by automata theory, specifies the interactive behaviour of systems, while reduction semantics specifies their internal evolution and is closer to the operational semantics of sequential programs. LTS semantics has been favoured in early work on process calculi, as it lends itself to the definition of a variety of behavioural equivalences that are easy to work with. Subsequently, a wealth of process calculi have been proposed, tailored to specific features (mobility, locations, security, sessions, etc). In these more complex calculi, it became more debatable what to adopt as labels or “observables” for the LTS semantics, and this motivated the shift towards a reduction semantics in conjunction with a structural congruence, allowing for a compact semantic description.
The thrust to retrieve an LTS semantics from a reduction semantics is an important one, and this paper is a milestone in this line of work. The solution proposed is robust, i.e., broadly applicable. It is also mathematically elegant, formulated using the categorical notion of relative pushout (RPO). The paper has spurred a whole trend of research on congruence properties for bisimilarity in which RPOs constitute the key notion. Good examples are applications to bigraphs, graph rewriting and name calculi.

Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar & Mariëlle Stoelinga. *The Element of Surprise in Timed Games*. CONCUR 2003.
https://doi.org/10.1007/978-3-540-45187-7_9

This paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. A key contribution of the paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise as they are played "faster", and the definition of natural concepts of winning conditions for the two players – ensuring that players can win only by playing according to a physically meaningful strategy. This approach provides a clean answer to the problem of time convergence, and the responsibility of the players in it. For this reason, it has since been the basis of numerous works on timed games. The algorithm established in the paper to study omega-regular conditions in this neat model of timed games is also enticing, resorting to mu-calculus on a cleverly enriched structure.

### 3 Concluding Remarks

Interviews with the award recipients, which give some information on the historical context that led them to develop their award-winning work and on their research philosophy, have been conducted by Luca Aceto with the help of some jury members. The interviews are accessible as blog posts in the Process Algebra Diary maintained by Luca Aceto at https://processalgebra.blogspot.com/. Links to these interviews may also be found on the award's webpage https://concur2022.mimuw.edu.pl/tot-award/.