Progress measures, immediate determinacy, and a subset construction for tree automata

Using the concept of progress measure, we give a new proof of Rabin's fundamental result that the languages defined by tree automata are closed under complementation. To do this we show that for certain infinite games based on tree automata, an immediate determinacy property holds for the player who is trying to win according to a Rabin acceptance condition. Immediate determinacy is stronger than the forgetful determinacy of Gurevich and Harrington, which depends on more information about the past, but applies to another class of games. Next, we show a graph theoretic duality theorem for winning conditions. Finally, we present an extended version of Safra's determinization construction. Together, these ingredients and the determinacy of Borel games yield a straightforward recipe for complementing tree automata. Our construction is almost optimal, i.e. the state space blow-up is essentially exponential --- thus roughly the same as for automata on finite or infinite words. To our knowledge, no prior constructions have been better than double exponential.