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

Search Nedrilad ::

Custom Search