Game Development Reference
In-Depth Information
π = v 0 ...v k , ending at a terminal position v k is computed by multiplying
all discount factors seen in the play with the payoff value at the final node,
p ( v 0 v 1 ...v k )= δ ( v 0 ,v 1 ) · δ ( v 1 ,v 2 ) · ...· δ ( v k− 1 ,v k ) · λ ( v k ) .
The outcome of an infinite play depends only on the lowest priority seen
infinitely often. We assign the value 0 to every infinite play in which the
lowest priority seen infinitely often is odd, and
to those in which it is
even. Player 0 wants to maximise the outcome whereas Player 1 wants to
minimise it.
Determinacy. A quantitative game is determined if, for each position v ,
the highest outcome that Player 0 can enforce from v and the lowest outcome
Player 1 can assure converge,
sup
σ∈ Γ 0
inf
ρ∈ Γ 1
p ( π σ,ρ ( v )) = inf
ρ∈ Γ 1
sup
σ∈ Γ 0
p ( π σ,ρ ( v )) =: val
G
( v ) ,
where Γ 0 , Γ 1 are the sets of all possible strategies for Player 0, Player 1. The
outcome defined in this way is the value of
at v .
One of the fundamental properties of qualitative parity games is the posi-
tional determinacy . Unfortunately, this does not generalise to quantitative
parity games. Example 4.33 shows that there are simple quantitative games
where no player has a positional winning strategy. In the depicted game there
is no optimal strategy for Player 0, and even if one fixes an approximation of
the game value, Player 0 needs infinite memory to reach this approximation,
because she needs to loop in the second position as long as Player 1 looped
in the first one to make up for the discounts. (By convention, we depict
positions of Player 0 with a circle and of Player 1 with a square and the
number inside is the priority for non-terminal positions and the payoff in
terminal ones.)
G
Example 4.33
1
2
2
0
1
1
4.7.3 model-checking games for
Given a quantitative transition system
=( S, T, δ S ,P i ) and a -formula
ψ in negation normal form, we define the model-checking game MC[
K
K
]=
( V,V 0 ,V 1 ,E,δ,λ, Ω), as a quantitative parity game.
Positions and moves. As in games for L μ , positions are the pairs ( ϕ, s ),