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:

  -  Main definitions and examples : infinite trees, parity tree automata and regular tree languages
  -  Basic recalls on positional determinacy of two-player parity games on graphs (see previous LAAG seminar by Nathanaël Fijalkow)
  -  Acceptance game and emptiness game/test for parity tree automata
  -  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.