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
.

Search Nedrilad ::

Custom Search