Game Development Reference
In-Depth Information
Proof A detailed version of this proof can be found in Thomas [1997]. We
only give a brief sketch of the ideas.
From formulae to automata one uses an inductive translation, based
on the closure properties of automata. To make this approach work, one
first introduces a variant of S1S that uses only set variables (and has a
predicate saying that a set is a singleton and a predicate for set inclusion).
Atomic formulae are easily translated into equivalent automata. For the
Boolean combinations one uses the closure properties of automata, and for
the existential quantification the projection.
From Buchi automata to formulae one writes a formula that describes
the existence of an accepting run. For each state q one uses a set X q that
contains the positions of the run where the automaton is in state q . Then one
can easily express that the run starts in the initial state, that infinitely many
final states occur, and that the transitions are respected in each step.
As for LTL winning conditions, we can now consider games with win-
ning conditions specified by S1S formulae. Using the translation into non-
deterministic Buchi automata and the determinisation theorem we can solve
such games.
Theorem 2.12 For games ( G, ϕ ) with a winning condition given by an
S1S formula ϕ one can decide the winner and can compute a corresponding
winning strategy.
The complexity of the inductive translation of formulae into automata is
rather high because each negation in the formula requires a complementation
of the automaton, which is exponential. Thus, the complexity of our algorithm
is non-elementary in the size of the formula. From lower bounds on the
complexity of deciding S1S presented in Meyer [1975] it follows that we
cannot hope for an improvement.
Based on lower bound results for the translation of formulae into automata
(see Reinhardt [2002]) one can show that this also applies to the memory
required for winning strategies in S1S games. The size of the memory required
for a winning strategy in a game with an S1S winning condition cannot be
bounded by a function of the form
2 2 2 · · · 2 n k
for a fixed k .