Determinization and Memoryless Winning Strategies

Abstract

We show that Safra's determinization of ω-automata with Streett (strong fairness) acceptance condition also gives memoryless winning strategies in infinite games, for the player whose acceptance condition is the complement of the Streett condition. Both determinization and memorylessness are essential parts of known proofs of Rabin's tree automata complementation lemma. Also, from Safra's determinization construction, along with its memoryless winning strategy extension, a single exponential complementation of Streett tree automata follows. A different single exponential construction and proof first appeared in [N. Klarlund (1992), Progress measures, immediate determinacy, and a subset construction for tree automata, in "Proceedings, 7th IEEE Symposium on Logics in Computer Science"]. © 1997 Academic Press.