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
}