Guidable automata and their index problem

Rabin's theorem relies on the equivalence between Monadic Second-Order logic and non-deterministic automata over infinite trees. The non-determinism of the involved model is known to be "inherent", both in terms of descriptive complexity and from the standpoint of uniformisability / unambiguity. As a consequence of this inherent non-determinism, all the standard notions of canonical representations fail for infinite trees (i.e. search of minimal objects, either in the algebraic or the automata-based sense). As a remedy, Colcombet and Loding proposed a notion of "guidable" automata. Such an automaton has at the same time: the most general, and the least required amount of "guessing" (which happens not to be contradictory). A crucial theorem about these automata states that every regular language of infinite trees can be recognised by some guidable automaton (SIC!). Although highly promising, this result has not been fully exploited so far... During the talk I will make us familiar with the notion of guidable automata and their relations to other models of limited non-determinism. Then I will move to a recent result (obtained jointly with Damian Niwiński) stating that the guidable index problem (i.e. the minimal index of a guidable automaton for a given language) is decidable. The proof relies on a game-based technique.