Game Development Reference

In-Depth Information

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 [1969], 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 [1972] 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

Search Nedrilad ::

Custom Search