In 1969, Michael O. Rabin established that the class of regular tree languages (i.e. languages of infinite node-labelled complete binary trees accepted by non-deterministic tree automata) form a Boolean algebra. The goal of this talk is to present the underlying objects of this statement as well as a complete proof of it.

Hence, the structure of the talk will be as follows:

  1. Main definitions and examples : infinite trees, parity tree automata and regular tree languages
  2. Basic recalls on positional determinacy of two-player parity games on graphs (see previous LAAG seminar by Nathanaƫl Fijalkow)
  3. Acceptance game and emptiness game/test for parity tree automata
  4. Complementation of parity tree automata relying on positional determinacy and determinisation of automata on infinite words (see previous LAAG seminar).

I will assume no specific knowledge on automata nor games for that talk.