Trees, automata, and games

In 1969 Rabin introduced tree automata and proved one of the deepest decidability results. If you worked on decision problems you did most probably use Rabin's result. But did you make your way through Rabin's cumbersome proof with its induction on countable ordinals? Building on ideas of our predecessors-and especially those of B-chi-we give here an alternative and transparent proof of Rabin's result. Generalizations and further results will be published elsewhere.