Game Development Reference
In this chapter we have introduced automata on infinite words and on infinite
trees and have illustrated how they are connected to the theory of infinite
games. In particular, automata on infinite words are useful for transforming
complex winning conditions of infinite games into simpler ones (at the
price of increasing the size of the game graph). For automata on infinite
trees one can use results from game theory to prove the correctness of the
complementation construction, and also to solve algorithmic problems like
the emptiness problem. When going beyond finite automata, the problems
become more di cult, but we have seen that some decidability results can be
retained if the specifications are given by deterministic pushdown automata
on infinite words.
The presentation in this chapter is given on a rather informal level. Many
constructions are explained using examples without giving precise definitions
and proofs. For the interested reader we give some references to other surveys
that cover material presented in this chapter: A survey on infinite games
and their connection to tree automata is given by Zielonka , containing
many algorithms for solving infinite games and problems for tree automata,
and a precise analysis of memory requirements for different types of winning
conditions. The survey by Thomas  has already been mentioned several
times in this chapter. It gives a nice overview of the main constructions
in the theory of automata on infinite words and trees, the connections to
logic, and also some basics on infinite games. The seminar volume by Gradel
et al.  contains many articles on various topics concerning automata
on infinite objects, infinite games, and logic. The textbook by Perrin and
Pin  covers many aspects of the theory of automata on infinite words.
Furthermore, similar to the theory of regular languages of finite words, the
topic also explains the basics of the algebraic theory of languages of infinite
words. Finally, we mention the recent and very detailed survey on automata
and logics for infinite words and trees that is given by Vardi and Wilke .
A.-J. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with unboundedness
and regular conditions. In Proceedings of FST TCS 2003: Foundations of Soft-
ware Technology and Theoretical Computer Science, 23rd Conference , volume
2914 of Lecture Notes in Computer Science , pages 88-99. Springer, 2003.
J. R. Buchi. On a decision method in restricted second order arithmetic. In
International Congress on Logic, Methodology and Philosophy of Science , pages
1-11. Stanford University Press, 1962.