Game Development Reference
In-Depth Information
μX. ( P
2 X ) , 1
a )
b )
Q
=
1
2
P, 1
P
2 X, 1
2
2
X, 2
2 X, 1
X, 1
P
2 X, 2
μX. ( P
2 X ) , 2
P, 2
2 X, 2
0
Figure
4.1 Example
(a)
QTS
and
(b)
model-checking
game
for
μX. ( P
2
·
X )
and forth. We have seen that quantitative parity games are appropriate
model-checking games for the evaluation of -formulae on quantitative
transition systems. For the other direction, we now show that values of
positions in quantitative parity games (with a bounded number of priorities)
are definable in . It is convenient to describe a quantitative parity game
G
=( V,V 0 ,V 1 ,E,δ G ,λ, Ω G ) with priorities in
{
0 ,...d
1
}
by a quantitative
transition system
for positions
of Player i , and V i ( v ) = 0 otherwise, where Ω( v )=Ω G ( v ) when vE
Q G =( V,E,δ,V 0 ,V 1 , Λ , Ω), where V i ( v )=
=
and
Ω( v )= d otherwise, with discount function
δ ( v, w )= δ G ( v, w )
for v
V 0 ,
( δ G ( v, w )) 1
for v
V 1
and with payoff predicate Λ( v ):= λ ( v ) in case vE =
and is Λ( v )=0
otherwise.
We then modify the L μ -formulae Win d constructed in Section 4.5.1 to
quite similar -formulae
d− 1
QWin d = νX 0 μX 1 νX 2 ...λX d− 1
(( V 0
P j
X j )
( V 1
P j
X j ))
Λ ,
j =0
where P i :=
when Ω( v )= i
and P i ( v ) = 0 otherwise. The formula QWin d is therefore analogous to the
formula Win d in the qualitative case.
¬
( μX. (2
·
X
∨|
Ω
i
|
)). Note that P i ( v )=
Theorem 4.36
For every d
N
, the value of any quantitative parity game
with priorities in
{
0 ,...d
1
}
coincides with the value of QWin d on the
associated transition system.