Game Development Reference
In-Depth Information
0
@
1
A
0
@
1
A
0
@
1
A
0
@
1
A
0
@
1
A
0
@
1
A ···
1
0
1
0
1
0
0
0
1
0
0
1
1
1
1
0
1
0
α =
¬p 2
···
1
0
1
1
0
0
¬p 2 U p 1
···
1
0
1
1
1
0
X( ¬p 2 U p 1 )
···
0
1
1
1
0
1 ?
···
p 3 X( ¬p 2 U p 1 )
1
1
1
1
1
1 ?
···
G( p 3 X( ¬p 2 U p 1 ))
1 ?
1 ?
1 ?
1 ?
1 ?
1 ?
Figure 2.8 A Buchi automaton guesses valuations for sub-formulae
To be able to interpret LTL formulae in infinite plays we assume that the
set C of colours of the game graph is
n .
To apply the method of game reduction it su ces to construct an equiv-
alent automaton for a given formula. We explain the underlying idea for
transforming an LTL formula into an equivalent (non-deterministic) Buchi
automaton. The automaton 'guesses' for each sub-formula of the given for-
mula ϕ its truth value at the current position and verifies its guesses. Thus,
the states of the automaton are mappings that associate to each sub-formula
of ϕ a truth value 0 or 1. Figure 2.8 illustrates how the Buchi automaton
works. The question marks in the table indicate that the truth value of the
corresponding formulae cannot be verified within the shown prefix of α but
depend on the continuation of α .
The verification of guesses works as follows:
{
0 , 1
}
Atomic formulae and Boolean combinations can be verified directly because
the truth values of the atomic formulae are coded in the input letter by
definition.
The operators X, G can be verified using the transitions. If the automaton
guesses that a formula X ψ is true at the current position, then ψ has to
be true at the next position. If a formula G ψ is guessed to be true, then ψ
also needs to be true, and G ψ has to be true in the next position.
The operators F, U are verified using the acceptance condition. We explain
the principle for the operator F. This can easily be generalised to U.
If F ψ is guessed to be true, then either F ψ has to be true again in the
next position, or ψ itself has to be true in the current position. Using
the acceptance condition, the automaton has to ensure that the second
option is taken at some point, i.e., that ψ indeed becomes true eventually.
For this purpose, we use a slight generalisation of Buchi automata that