As members of the TCS community will most likely know, FOCS established Test-of-Time Awards from its 2021 edition to celebrate contributions published at that conference 30, 20 and 10 years before. The first list of selected winners is, as one might have expected, stellar:
- Uriel Feige, Shafi Goldwasser, László Lovász, Shmuel Safra, Mario Szegedy:
Approximating Clique is Almost NP-Complete.
FOCS 1991 - David Zuckerman:
Simulating BPP Using a General Weak Random Source.
FOCS 1991 - Serge A. Plotkin, David B. Shmoys, Éva Tardos:
Fast Approximation Algorithms for Fractional Packing and Covering Problems.
FOCS 1991 - Ran Canetti:
Universally Composable Security: A New Paradigm for Cryptographic Protocols.
FOCS 2001 - Boaz Barak:
How to Go Beyond the Black-Box Simulation Barrier.
FOCS 2001 - Amit Chakrabarti, Yaoyun Shi, Anthony Wirth, Andrew Chi-Chih Yao:
Informational Complexity and the Direct Sum Problem for Simultaneous Message Complexity.
FOCS 2001 - Zvika Brakerski, Vinod Vaikuntanathan:
Efficient Fully Homomorphic Encryption from (Standard) LWE.
FOCS 2011
FWIW, I offer my belated congratulations to all the award recipients, whose work has had, and continues to have, a profound influence on the "Volume A" TCS community.
Apart from celebrating their achievement, the purpose of this post is to highlight a paper from FOCS 1991 that missed out on the Test-of-Time Award, but that, IMHO, would have fully deserved it.
I am fully aware that the number of deserving papers/scientists is typically larger, if not much larger, than the number of available awards. Awards are a scarce resource! My goal with this post is simply to remind our community (and especially its younger members) of a seminal contribution that they might want to read or re-read.
The paper in question is "Tree automata, mu-calculus and determinacy" by Allen Emerson and Charanjit S. Jutla, which appeared at FOCS 1991. (Emerson shared the 2007 A.M. Turing Award for the invention of model checking and Jutla went on to doing path-breaking work in cryptography.) That paper is absolutely fundamental for the mu-calculus, but also for automata theory, and verification in general. It introduced many ideas and results that became the basis for extensive research.
As a first contribution, the article introduced parity games and proved their fundamental properties. The parity condition was a missing link in automata theory on infinite objects. It made the whole theory much simpler than that proposed in earlier work. Technically, the parity condition is both universal and positional. Universal means that tree automata with parity conditions are as expressive as those with Rabin or Muller conditions. Positional means that in the acceptance game if a player has a winning strategy then she has one depending only on the current position and not on the history of the play so far. This is a huge technical advance for all automata-theoretic constructions and for the analysis of infinite-duration games. It allows one, for instance, to avoid the complicated arguments of Gurevich and Harlington in their seminal STOC 1982 article, which were already a huge simplification of Rabin's original argument from 1969 proving the decidability of the monadic second-order theory of the infinite binary tree and much more. In passing, let me remark that Rabin has gone on record saying that "I consider this to be the most difficult research I have ever done." See this interview in CACM.
The second main contribution of that paper is the discovery of the relation between parity games and the mu-calculus. The authors show how a mu-calculus model-checking problem can be reduced to solving a parity game, and conversely, how the set of winning positions in a parity game can be described by a mu-calculus formula. This result is the birth of the "model-checking via games" approach. It also shows that establishing a winner in parity games is contained both in NP and in co-NP. As a corollary, the model-checking problem is as complex as solving games. It is still not known if the problem is in PTIME. A recent advance from STOC'17 gives a quasi-polynomial-time algorithm. (See this blog post for a discussion of that result, which received the STOC 2017 best paper award and was immediately followed up by a flurry of related papers.)
Finally, the paper also shows how to prove Rabin's complementation lemma, which is the most difficult step in his celebrated aforementioned decidability result, with the help of parity conditions. The proof is radically simpler than previous approaches. The paper puts this contribution most prominently, but actually the conceptual and technical contributions presented later in the paper turned out to be most important for the community.
Overall, the above-mentioned paper by Emerson and Jutla is a truly seminal contribution that has stood the test of time, has sown the seeds for much research over the last thirty years (as partly witnessed by the over 1,130 citations it has received so far) and is still stimulating advances at the cutting edge of theoretical computer science that bridge the Volume A-Volume B divide.
I encourage everyone to read it!
Acknowledgement: I have learnt much of the content of this post from Igor Walukiewicz. The responsibility for any infelicity is mine alone.
No comments:
Post a Comment