The Edsger W. Dijkstra Prize in Distributed Computing is awarded for outstanding papers on the principles of distributed computing, whose significance and impact on the theory or practice of distributed computing have been evident for at least a decade. It is sponsored jointly by the ACM Symposium on Principles of Distributed Computing (PODC) and the EATCS Symposium on Distributed Computing (DISC). The prize is presented annually, with the presentation taking place alternately at PODC and DISC. The committee decided to award the 2021 Edsger W. Dijkstra Prize in Distributed Computing to
Paris C. Kanellakis and Scott A. Smolka
for their paper:
CCS Expressions, Finite State Processes, and Three Problems of Equivalence
Information and Computation, Volume 86, Issue 1, pages 43–68, 1990.
A preliminary version of this paper appeared in the proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing (PODC) 1983, pages 228–240.
This paper was a foundational contribution to the fundamental challenge of assigning semantics to concurrent processes, for specification and verification. It addressed the computational complexity of the previously introduced celebrated notion of behavioral equivalence, a cornerstone of Milner’s Calculus of Communicating Systems (CCS), aimed at tackling semantics by considering equivalence classes.
With the publication of their PODC 1983 paper, Kanellakis and Smolka pioneered the development of efficient algorithms for deciding behavioral equivalence of concurrent and distributed processes, especially bisimulation equivalence, which is the cornerstone of the process-algebraic approach to modeling and verifying concurrent and distributed systems. Specifically, the main result of their paper is what has come to be known as the K-S Relational Coarsest Partitioning algorithm, which at the time was a new combinatorial problem of independent interest.
The paper also presented complexity results that showed certain behavioral equivalences are computationally intractable. Collectively, Kanellakis and Smolka’s results founded the subdiscipline of algorithmic process theory, and helped jump-start the field of Formal Verification.
2021 Award Committee:
Keren Censor-Hillel (chair), Technion
Pierre Fraigniaud, Université de Paris and CNRS
Cyril Gavoille, LaBRI — Université de Bordeaux
Seth Gilbert, National University of Singapore
Andrzej Pelc, Université du Québec en Outaouais
David Peleg, Weizmann Institute of Science