Test of Time Award

3 minute read

The CONCUR conference and the IFIP 1.8 Working Group on Concurrency Theory are happy to announce the first edition of the CONCUR Test-of-Time Award. 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. All papers published in CONCUR between 1990 and 1995 are eligible.

The award winners for the CONCUR ToT Awards 2020 have been selected by a Jury composed of Luca Aceto (Chair), Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva. The list of papers selected for the CONCUR ToT Awards 2020, together with their citations, are:

Period 1990-1993

Rob van Glabbeek. The Linear Time-Branching Time Spectrum

Citation: The companion papers on “The Linear Time-Branching Time Spectrum”, published by Rob van Glabbeek at CONCUR 1990 and 1993, jointly receive one award for offering a highly influential taxonomy of the menagerie of process semantics, both in a setting where every system action is observable and in the presence of silent moves. Each of the plethora of studied semantics comes equipped with a variety of elegant characterisations in terms of modal logics, testing scenarios, relations, and complete axiomatisations. The encyclopedic nature of the above-mentioned papers has made them a must read for researchers in concurrency theory for nearly 30 years.

Check the interview with Rob van Glabbeek by Luca Aceto.

Søren Christensen, Hans Hüttel and Colin Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes

Citation: The paper “Bisimulation Equivalence is Decidable for all Context-Free Processes”, published by Søren Christensen, Hans Hüttel and Colin Stirling at CONCUR 1992, receives one award for extending and simplifying the seminal result by Baeten, Bergstra and Klop, who proved the decidability of bisimilarity over normed context-free processes. The CONCUR’92 paper has paved the way to further decidability and complexity results for a variety of classes of infinite-state processes. This includes the 2-EXPTIME algorithm for bisimilarity over BPA presented by Burkart, Caucal and Steffen in a paper published at MFCS 1995, and the work by Senizergues in papers at FOCS 1998 and in the SIAM Journal on Computing in 2005, presenting decidability results for all “equational graphs” with finite out-degree.

Check the interview with Hans Hüttel by Luca Aceto.

Period 1992-1995

Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes

Citation: The paper “Probabilistic simulations for probabilistic processes”, published by Roberto Segala and Nancy Lynch at CONCUR 1994, receives one award for introducing the ‘simple’ probabilistic automata model. Unlike earlier attempts to embrace probabilities, transition targets here are probability distributions over states, and this makes it possible to lift core process algebraic results in a very elegant manner. Probabilistic automata have quickly been recognised as the pivotal link between classical concurrency theory and the theory of discrete-state Markov processes. They have become the central subjects of probabilistic model checking, and are echoed in a range of very influential modelling formalisms including probabilistic timed automata, probabilistic hybrid automata, and Markov automata.

Check the interview with Roberto Segala and Nancy Lynch by Luca Aceto.

Davide Sangiorgi. A Theory of Bisimulation for the pi-Calculus

Citation: The paper “A Theory of Bisimulation for the pi-Calculus”, published by Davide Sangiorgi in CONCUR 1993, receives one award for introducing the notion of open bisimilarity, which, unlike early and late bisimilarity, is a congruence for the pi-calculus. Open bisimilarity makes it possible to view most names as uninstantiated variables, and this allows for the development of efficient tools based on a kind of symbolic state-space exploration. Open bisimilarity and tools based on it have, for instance, played an important role in research on cryptographic protocols modelled using extensions of the pi-calculus. For a recent example, Horne has used open bisimilarity as the appropriate way to model the capabilities of an attacker trying to get confidential information, with a real-world application to finding and fixing a privacy flaw in e-passports presented by Filimonov et al. at ESORICS 2019.

Check the interview with Davide Sangiorgi by Luca Aceto.