Saturday, March 12, 2022

FOCS 2021 Test-of-Time Award winners (and one deserving paper that missed out)

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.

Sunday, March 06, 2022

HALG 2022: Call For Submissions of Short Contributed Presentations

On behalf of Keren Censor-Hillel, PC chair for HALG 2022, I am happy to post the call for submissions of short contributed presentations for that event. I encourage all members of the algorithms community to submit their contributed presentations. HALG has rapidly become a meeting point for that community in a relaxed workshop-style setting.

The 7th Highlights of Algorithms conference (HALG 2022) 

London, June 1-3, 2022 

https://www.lse.ac.uk/

HALG-2022 The Highlights of Algorithms conference is a forum for presenting the highlights of recent developments in algorithms and for discussing potential further advances in this area. The conference will provide a broad picture of the latest research in algorithms through a series of invited talks, as well as the possibility for all researchers and students to present their recent results through a series of short talks and poster presentations. Attending the Highlights of Algorithms conference will also be an opportunity for networking and meeting leading researchers in algorithms.  

Call For Submissions of Short Contributed Presentations: The HALG 2022 conference seeks submissions for contributed presentations. Each presentation is expected to consist of a poster and a short talk (serving as an invitation to the poster). There will be no conference proceedings, hence presenting work already published at a different venue or journal (or to be submitted there) is welcome. 

If you would like to present your results at HALG 2022, please submit their details: the abstract, the paper and the speaker of the talk via EasyChair: https://easychair.org/conferences/?conf=halg2022 

The abstract should include (when relevant) information where the results have been published/accepted (e.g., conference), and where they are publicly available (e.g., arXiv). All submissions will be reviewed by the program committee, giving priority to work accepted or published in 2021 or later. 

Submissions deadline: March 27, 2022. 

Acceptance/rejection notifications will be sent in early April.

Friday, March 04, 2022

Combinatorial Exploration: An algorithmic framework to automate the proof of results in combinatorics

Are you interested in combinatorial mathematics? If so, I am happy to welcome you to the future! 

I am proud to share with you a new, 99-page preprint by three colleagues from my department (Christian Bean, Émile Nadeau and Henning Ulfarsson) and three of their collaborators (Michael Albert, Anders Claesson and Jay Pantone) that is the result of years of work that led to the birth of Combinatorial Exploration. Combinatorial Exploration is an algorithmic framework that can prove results that so far have required the ingenuity of human combinatorialists. More specifically, it can study, at the press of a button, the structure of combinatorial objects and derive their counting sequences and generating functions. The applicability and power of Combinatorial Exploration are witnessed by the applications to the domain of permutation patterns given in the paper. My colleagues use it to re-derive hundreds of results in the literature in a uniform manner and prove many new ones. See the Permutation Pattern Avoidance Library (PermPAL) and Section 2.4 of the article for a more comprehensive list of notable results. The paper also gives three additional proofs-of-concept, showing examples of how Combinatorial Exploration can prove results in the domains of alternating sign matrices, polyominoes, and set partitions. Last, but by no means least, the github repository at https://github.com/PermutaTriangle/comb_spec_searcher contains the open-source python framework for Combinatorial Exploration, and the one at https://github.com/PermutaTriangle/Tilings contains the code needed to apply it to the field of permutation patterns. 

 "Det er svært at spå, især om fremtiden", as Niels Bohr and Piet Hein famously said. However, let me stick my neck out and predict that this work will have substantial impact and will be the basis for exciting future work. 

 Congratulations to my colleagues! With my department chair hat on, I am very proud to see work of this quality stem from my department and humbled by what my colleagues have achieved already. As an interested observer, I am very excited to see what their algorithms will be able to prove in the future. For the moment, let's all enjoy what they have done already.