The purpose of the award is to recognize important achievements in Concurrency Theory that were published at the CONCUR conference and have stood the test of time.
In 2022, four papers were chosen to receive the CONCUR Test-of-Time Awards for the periods 1998–2001 and 2000–2003. The jury of the Test-of-Time award consisted of Ilaria Castellani (chair), Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi.
Period 1998–2001
Christel Baier, Joost-Pieter Katoen, Holger Hermanns.
Approximate symbolic model checking of continuous-time Markov chains.
CONCUR 1999.
The paper presented the first symbolic model-checking algorithm for systems that combine probabilistic and real-time behaviors. Specifically, the model-checking algorithm handles real-time probabilistic systems, modeled 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 which 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 generalization of BDDs, to MTDDs (multi-terminal decision diagrams), which allow both Boolean and real-valued variables, and which enables symbolic reasoning.
The interview with the award recipients at the Process Algebra Diary.
Franck Cassez, Kim Larsen.
The Impressive Power of Stopwatches.
CONCUR 2000.
The 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.
The interview with the award recipients at the Process Algebra Diary.
Period 2000–2003
James J. Leifer, Robin Milner.
Deriving Bisimulation Congruences for Reactive Systems.
CONCUR 2000.
The 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.
The interview with James Leifer at the Process Algebra Diary.
Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga.
The Element of Surprise in Timed Games.
CONCUR 2003.
The 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.
The interview with the award recipients at the Process Algebra Diary.