David Janin and Igor Walukiewicz
On the Expressive Completeness of the Propositional mu-Calculus with spect to Monadic Second Order Logic

Citation: This seminal paper relates the expressive power of monadic second-order logic and the mu-calculus, showing that the bisimulation-closed formulas monadic second-order logic are equivalent to the mu-calculus. This is a very deep and insightful result, providing a contribution of undational nature to the field of logic and computation. The paper's insight was one of the central factors contributing to the role of the mu-calculus in model checking, where it provides the computational counterpart to gics for expressing system properties. The relation between logics and the mu-calculus, which can in great part be traced to this paper, has been an extremely fruitful one, with implications in algorithms for the verification and analysis of transition systems, probabilistic systems, timed systems, games, and more.

Uwe Nestmann and Benjamin C. Pierce
Decoding Choice Encodings

Citation: This paper makes major strides in the study of the expressiveness of process calculi. It shows that, in a completely distributed and asynchronous setting, input-guarded choice can be simulated by parallel composition. More precisely, the paper constructs a fully distributed and divergence-free encoding from the input-choice pi-calculus into the asynchronous pi-calculus. The correctness of this encoding is demonstrated by establishing a semantic equivalence between a process and its encoding, thereby satisfying and strengthening the common quality criterion of full abstraction. As semantic equivalence it employs the asynchronous version of coupled simulation, and illuminates the surprising versatility of this notion by showing how it avoids the introduction of divergence in the encoding. This work formalizes ideas stemming from the programming language Pict, and has been very influential in the area of expressiveness in concurrency.

Ahmed Bouajjani, Javier Esparza, and Oded Maler
Reachability Analysis of Pushdown Automata: Application to Model-checking

Citation: This is a breakthrough paper that opened the way for the analysis of pushdown automata via model-checking techniques. The paper proposes a general class of alternating pushdown systems and defines new model checking algorithms for these systems against both linear and branching-time properties. The basic idea is simple, yet extremely elegant: using (regular) automata as representations for sets of states of pushdown automata. The paper proceeds to show that the representation is closed with respect to Boolean operators, makes membership of states decidable, and crucially, makes the predecessor operator easily computable. The approach proposed in this paper is so neat and natural that it has become a standard reference in the field of verification of infinite-state systems.

Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi
Alternating Refinement Relations

Citation: This paper introduces refinement relations, based on simulation and trace containment, for games, modeled as alternating transition systems. Refinement relations had been a foundational notion in formal methods, and much more broadly, in the theory of computation. In the years leading up to this paper, it had become evident that games provided the natural model for open systems, which communicate and are reactive to their environment; this paper extends the notion of simulation and trace containment to games. While conceived in a formal-methods and verification setting, the paper turned out to have broad implications, as these game refinement relations have implications for strategies in general games, and are closely related to notions of subtyping in game theory and in dynamic typing. The extension of refinement relations to games was thus a fundamental tassel in the understanding of dynamic systems, finally being put into place.