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
Qμ

Given a quantitative transition system

=(
S, T, δ
S
,P
i
) and a
Qμ
-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
),

Search Nedrilad ::

Custom Search