Game Development Reference
In-Depth 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 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
well-behaved negation operator (with [[ ¬ϕ ]] K =1 / [[ ϕ ]] K ) and which gives us
the dualities that are needed for natural model-checking games.
Note that all operators in are monotone. This guarantees the existence
of the least and greatest fixed-points, and their inductive definition according
to the Knaster-Tarski 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