Game Development Reference
In-Depth Information
where ϕ is a subformula of ϕ , and s
S is a state of the
K
; in addition we
have two special positions (0) and (
)
are terminal positions. Moves are defined as in the games for L μ , with the
following modifications: positions of the form (
). Positions (
|
P i
c
|
,s ) , (0) , and (
ψ, s ) have either a single
, or one successor ( ψ, s )
successor (0), in case s is a terminal state in
K
for every s
sT . Analogously, positions of the form (
ψ, s ) have a single
, or one successor ( ψ, s ) for every s
successor (
), if sT =
sT otherwise.
ψ, s ) have a unique successor ( ψ, s ). Priorities are
assigned in the same way as in the model-checking games for L μ .
Discounts and payoffs. The discount of an edge is d for transitions from
positions ( d
Positions of the form ( d
·
ψ, s ), it is δ S ( s, s ) for transitions from (
ψ, s )to( ψ, s ), it
·
is 1 S ( s, s ) for transitions from (
ψ, s )to( ψ, s ), and 1 for all outgoing
transitions from other positions. The payoff function λ assigns
|
[[ P i ]] ( s )
c
|
to all positions ( |P i − c|,s ), to position ( ), and 0 to position (0).
To prove that MC( K,ψ ) is indeed an appropriate model-checking game
it must be shown that the value of the game starting from v coincides with
the value of the formula evaluated on
at v . In the qualitative case, that
K
,v if Player 0 wins in
means, that ψ holds in
K
G
from v .
Theorem 4.34
For every formula ψ in Qμ, every quantitative transition
system
K
, and v
∈K
, the game MC [
K
] is determined and
]( ψ, v )=[ ψ ]] K ( v ) .
valMC [
K
This is shown by Fischer et al. [2009] using a generalisation of the unfolding
method for parity games.
Example 4.35
A model-checking game for ϕ = μX. ( P
2
·
X )onthe
QTS
shown in Figure 4.1(a), with P (1) = 0, P (2) = 1, is depicted in
Figure 4.1(b). The nodes are labelled with the corresponding subformulae of
ϕ , and the state of
Q
Q
. Only the edges with discount factor different from 1
are labelled.
Note that in this game only Player 0 is allowed to make any choices. When
we start at the top node, corresponding to an evaluation of ϕ at 1 in
, the
only choice she has to make is either to keep playing (by looping), or to end
the game by moving to a terminal position.
Q
4.7.4 Defining game values in
As in the case of parity games and LFP (and ), also the connection
between quantitative parity games and quantitative μ -calculus goes back
Search Nedrilad ::




Custom Search