Game Development Reference
In-Depth Information
2
Infinite Games and Automata Theory
Christof Loding
RWTH Aachen University
Abstract
This chapter gives an introduction to the connection between automata
theory and the theory of two player games of infinite duration. We illustrate
how the theory of automata on infinite words can be used to solve games
with complex winning conditions, for example specified by logical formulae.
Conversely, infinite games are a useful tool to solve problems for automata
on infinite trees such as complementation and the emptiness test.
2.1 Introduction
The aim of this chapter is to explain some interesting connections between
automata theory and games of infinite duration. The context in which
these connections have been established is the problem of automatic circuit
synthesis from specifications, as posed by Church [1962]. A circuit can be
viewed as a device that transforms input sequences of bit vectors into output
sequences of bit vectors. If the circuit acts as a kind of control device, then
these sequences are assumed to be infinite because the computation should
never halt.
The task in synthesis is to construct such a circuit based on a formal
specification describing the desired input/output behaviour. This problem
setting can be viewed as a game of infinite duration between two players:
The first player provides the bit vectors for the input, and the second player
produces the output bit vectors. The winning condition of the game is given
by the specification. The goal is to find a strategy for the second player such
that all pairs of input/output sequences that can be produced according