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

Search Nedrilad ::

Custom Search