Automata, Trees, and Games
Yuri G. Gurevich, Leo A. Harrington · Symposium on the Theory of Computing · 1982
We prove a forgetful determinacy theorem saying that, for a wide class of infinitary games, one of the players has a winning strategy that is virtually memoryless: the player has to remember only bounded many bits of information. We use forgetful determinacy to give a transparent proof of Rabin’s celebrated result that the monadic second-order theory of the infinite tree is decidable.