Game Development Reference
InDepth Information
is a function [[
ϕ
]]
K
:
(
V,E,δ,
(
P
i
)
i∈I
). The meaning of a formula
ϕ
in
K
+
∞
+
∞
V
→
R
. We write
F
for the set of functions
f
:
V
→
R
, with
f
1
≤
f
2
if
f
1
(
v
)
≤
f
2
(
v
) for all
v
. Then (
F
,
≤
) forms a complete lattice with the
constant functions
f
=
as
f
= 0 as top and bottom elements.
The interpretation [[
ϕ
]]
K
:
V
∞
+
∞
→
R
is defined as follows:
]]
K
(
v
):=
(1) [[

P
i
−
c


P
i
(
v
)
−
c

,
ϕ
2
]]
K
:= min
[[
ϕ
1
]]
K
,
[[
ϕ
2
]]
K
}
(2) [[
ϕ
1
∧
{
and
ϕ
2
]]
K
:= max
[[
ϕ
1
]]
K
,
[[
ϕ
2
]]
K
}
[[
ϕ
1
∨
{
,
ϕ
]]
K
(
v
):=sup
v
∈vE
δ
(
v, v
)
[[
ϕ
]]
K
(
v
) and
(3) [[
♦
·
ϕ
]]
K
(
v
):=inf
v
∈vE
δ
(
v,v
)
[[
ϕ
]]
K
(
v
),
1
[[
ϕ
]]
K
(
v
):=
d
[[
ϕ
]]
K
(
v
),
(4) [[
d
·
·
(5) [[
μX.ϕ
]]
K
:= inf
:
f
=[
ϕ
]]
K
[
X←f
]
{
f
∈F
}
, and
[[
νX.ϕ
]]
K
= sup
:
f
=[
ϕ
]]
K
[
X←f
]
{
f
∈F
}
.
When interpreted over qualitative transition systems
Qμ
coincides with
the classical
μ
calculus and we say that
K
,v
is a model of
ϕ
,
K
,v

=
ϕ
if
[[
ϕ
]]
K
(
v
)=
∞
. For discounted systems we take the natural definition for
♦
1
and use the dual one for
δ
factor. It has been proved
by Fischer et al. [2009] that this is the only definition for which there is a
wellbehaved negation operator (with [[
¬ϕ
]]
K
=1
/
[[
ϕ
]]
K
) and which gives us
the dualities that are needed for natural modelchecking games.
Note that all operators in
Qμ
are monotone. This guarantees the existence
of the least and greatest fixedpoints, and their inductive definition according
to the KnasterTarski Theorem: Given a formula
μX.ϕ
and a quantitative
transition system
K
, we obtain the inductive sequence of functions
g
α
(for
ordinals
α
) where
g
0
:= 0,
g
α
+1
:= [[
ϕ
]]
K
[
X←g
α
]
,and
g
λ
:= lim
α<λ
[[
ϕ
]]
K
[
X←g
α
]
for limit ordinals
λ
. Then [[
μX.ϕ
]]
K
=
g
γ
for the minimal ordinal
γ
with
g
γ
=
g
γ
+1
.For
νX.ϕ
the dual induction applies, starting with
g
0
:=
which motivates the
∞
.
4.7.2 Quantitative parity games
Quantitative parity games are modest modifications of classical parity games.
Quantitative values are assigned to final positions, where they are interpreted
as the payoff for Player 0 at that position, and to moves, where they are
interpreted as discounts to the payoff when the play goes through that move.
A
quantitative parity game
is a tuple
=(
V,V
0
,V
1
,E,δ,λ,
Ω) extend
ing a classical parity game by two functions
δ
:
E
G
+
, assigning to every
→
R
+
∞
move a
discount factor
, and
λ
:
assigning to
every terminal position a
payoff value
. The
outcome
p
(
π
) of a finite play
{
v
∈
V
:
vE
=
∅} →
R
Search Nedrilad ::
Custom Search