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

Search Nedrilad ::

Custom Search