Game Development Reference

In-Depth Information

If
C
contains
n
colours, then we assign the priorities as follows:

d
n
,h
]) =
2
h −
1

{d
1
,...,d
h
} /∈F
,

c
LAR
([
d
1
···

2
h

{

d
1
,...,d
h
}∈F

.

In the example from Figure 2.7 this is shown for the Muller condition

F

.

Combining all this we obtain the LAR automaton

=

{{

b, d

}

,

{

a, b, c

}}

A
LAR
=(
LAR
(
C
)
,C,q
0
,δ
LAR
,c
LAR
)

and the following theorem:
3

Theorem 2.7
(Buchi [1983], Gurevich and Harrington [1982])

For a Muller

condition

F

over C the corresponding deterministic parity automaton

A

LAR

C
ω
that satisfy the Muller condition

accepts precisely those α

.

Now, given a Muller game, we can take the product with the LAR automa-

ton. This results in a parity game for which we can compute the winner and

a positional winning strategy. This winning strategy can be implemented

over the Muller game using the LAR automaton as memory.

∈

F

Theorem 2.8
(Buchi [1983], Gurevich and Harrington [1982])

Muller

games are determined with the LAR automaton as memory.

2.3.3 Logical winning conditions

In this section we show examples for game reductions where the winning

conditions of the games are given by logical formulae. We consider two logics:

the linear time temporal logic LTL introduced by Pnueli [1981], and monadic

second-order logic over infinite words (Buchi [1962]). LTL is widely used in

verification, for example the model checker SPIN can verify LTL properties

on finite systems (Holzmann [2003]). The interest in monadic second-order

logic is more of a theoretical nature. This logic is often used as a yardstick

for expressive power because it subsumes many specification logics.

Linear temporal logic

The formulae of LTL are defined over a set
P
=

of atomic

propositions, and are evaluated over infinite sequences of vectors of size
n
.

The
i
th entry of such a vector codes the truth value of
p
i
(1 = true, 0 =

false).

LTL formulae are built up from

3
The parity condition is not used by Buchi [1983], Gurevich and Harrington [1982] because it

has been introduced later but the statement can easily be derived from these papers.

{

p
1
,...,p
n

}

Search Nedrilad ::

Custom Search