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

Abstract

Using the concept of a progress measure, a simplified proof is given of M. O. Rabin's (1969) fundamental result that the languages defined by tree automata are closed under complementation. To do this, it is shown that for infinite games based on tree automata, the forgetful determinacy property of Y. Gurevich and L. Harrington (1982) can be strengthened to an immediate determinacy property for the player who is trying to win according to a Rabin acceptance condition. Moreover, a graph-theoretic duality theorem for such acceptance conditions is shown. Also presented is a strengthened version of S. Safra's determinization construction. Together these results and the determinacy of Borel games yield a straightforward method for complementing tree automata.