Game Development Reference
to the strategy satisfy the specification. Such a strategy can be seen as a
realisation of the specification.
This approach using games as a model for the synthesis problem has
been taken by Buchi and Landweber , where it is shown that the
synthesis problem can be solved by an algorithm for specifications that
are written in monadic second-order logic. As a tool they use automata
on infinite words: The formula defining the specification is translated into
a deterministic automaton over infinite words that accepts precisely those
pairs of input/output sequences that satisfy the formula. This reduces the
synthesis problem to the computation of a strategy on a finite game graph
(composed of the transition structure of the automaton and the choices of
the bit vectors by the two players) with a winning condition derived from
the acceptance condition of the automaton, usually expressed in terms of
the vertices that occur infinitely often during a play on the graph.
Another approach to solve the synthesis problem for monadic second-order
logic has been taken by Rabin  using automata on infinite trees. The
idea is that the behaviour of a circuit can be represented by an infinite
ordered labelled tree of a suitable branching degree: The input sequences
are coded by the paths through the tree, where the direction the path takes
determines the next input bit vector, and the labels of the nodes along the
path determine the outputs produced by the circuit. The key result shows that
a monadic second-order specification of admissible input/output sequences
can be translated into a finite automaton running on infinite trees such that
precisely those trees are accepted that represent circuit behaviours which
are admissible w.r.t. the specification. In this way the synthesis problem is
reduced to the emptiness problem for automata on infinite trees. It turns
out that games are a useful tool to solve these kinds of emptiness problems.
The above descriptions illustrate the interplay between games of infinite
duration and different types of automata. The goal of this chapter is to study
this relationship in more depth, in particular the following two aspects:
1 How can we use automata to solve problems that arise in the theory of
infinite duration games?
2 How can we use games to solve problems that arise in automata theory?
After having introduced the central objects of this chapter, namely games
and strategies, in Section 2.2, we consider the first question in Section 2.3:
We show how to use automata on infinite words to compute strategies in
games with complex winning conditions, e.g., defined in logical formalisms.
Section 2.4 is dedicated to the second question: We explain how results on
infinite games can help us to obtain results for automata on infinite trees. In