Game Development Reference
InDepth 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)
modelchecking
game
for
μX.
(
P
∨
2
·
♦
X
)
and forth. We have seen that quantitative parity games are appropriate
modelchecking games for the evaluation of
Qμ
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
Qμ
. 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
Qμ
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.
Search Nedrilad ::
Custom Search