Game Development Reference

In-Depth Information

2.6 Conclusion

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 [1998], 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 [1997] 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. [2002] contains many articles on various topics concerning automata

on infinite objects, infinite games, and logic. The textbook by Perrin and

Pin [2004] 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 [2007].

References

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.

Search Nedrilad ::

Custom Search