Game Development Reference
In-Depth Information
have several sets F 1 ,...,F k of final states. A run is accepting if all sets
are visited infinitely often. Now, for each formula F ψ we introduce one
set of final states that contains all states in which ψ is true or F ψ is false.
This way, once F ψ is guessed to be true, ψ has to become true eventually,
because otherwise the set of final states for F ψ will not be visited anymore.
The same principle applies to sub-formulae with the until operator: A
formula ψ 1 U ψ 2 is true if either ψ 1 is true now and ψ 1 U ψ 2 is true again in
the next position, or if ψ 2 is true now.
In the first position the automaton has to guess that the whole formula ϕ is
true because it is supposed to accept exactly those words which satisfy the
formula.
Exercise 2.4 In the same way as for formulae F ψ we introduce a set of
final states for each sub-formula ψ 1 U ψ 2 . What should the definition of this
set of states look like?
Exercise 2.5 The construction from LTL formulae to automata explained
above yields a generalised Buchi automaton with several sets of states.
Find a construction that transforms a generalised Buchi automaton into an
equivalent Buchi automaton with only one set of final states.
Hint: Cycle through the different sets of final states by introducing copies
of the Buchi automaton.
Using the idea illustrated above, we obtain the following theorem:
Theorem 2.9 (Vardi and Wolper [1986])
For each LTL formula ϕ one can
construct an equivalent Buchi automaton
A ϕ of size exponential in ϕ.
Using the determinisation theorem for ω -automata and the method of
game reduction, we obtain the following theorem.
Theorem 2.10 Games ( G, ϕ ) with a winning condition given by an LTL
formula can be solved in doubly exponential time.
The theorem has been shown first by Pnueli and Rosner [1989] in a slightly
different formulation in the context of synthesising reactive programs. In
this setting the goal is to construct a program (such as a controller or
circuit) that reads inputs and produces outputs, as already explained in the
introduction. A specification is given that relates the input sequences to the
output sequences and the task is to synthesise the program automatically
from the specification. If this specification is given by an LTL formula, then
one can reformulate the problem as a game with LTL winning condition. The