Game Development Reference
In-Depth Information
1
2
1
2
v
u a
v 1
u b
u c
v 2
u d
1
1
1
1
Let
ϕ ≡ P =1 F ( a ∨ c ) P =1 F ( b ∨ d ) ( P > 0 F c ) ( P > 0 F d ) .
Assume that player has a ϕ -winning strategy σ in v . The strategy σ
cannot randomise at v 1 , because then both of the subformulae P =1 F ( a ∨ c )
and P =1 F ( b
d ) become invalid in v , and player
can always falsify the
subformula ( P > 0 F c )
( P > 0 F d ). Hence, the strategy σ must choose one of the
transitions v 1
u a , v 1
u b with probability one. For each of these choices,
player
can falsify the formula ϕ , which means that σ is not ϕ -winning.
Similarly, one can show that player
does not have a
¬
ϕ -winning strategy
in v (in particular, note that player
cannot randomise at v 2 , because this
would make the subformula ( P > 0 F c )
( P > 0 F d ) valid).
In Brazdil et al. [2006], it was also shown that for PCTL objectives, the
existence of a ϕ -winning MD strategy for player
in a given vertex of
a finite-state stochastic turn-based game is Σ 2 = NP NP -complete, which
complements the aforementioned result for MDPs. Further, it was shown that
the existence of a ϕ -winning HR (or HD) strategy in a given vertex of a finite-
state MDP is highly undecidable (i.e., beyond the arithmetical hierarchy). The
proof works even for a fixed quantitative PCTL formula ξ . The use of a non-
qualitative probability constraint in ξ is in fact unavoidable -as it was shown
later by Brazdil et al. [2008], the existence of a ϕ -winning HR (or HD) strategy
in finite-state MDPs with qualitative PCTL and PECTL objectives is
EXPTIME -complete and 2 - EXPTIME -complete, respectively. It is worth
noting that these algorithms are actually polynomial for every fixed qualitative
PCTL or PECTL formula. A HR (or HD) ϕ -winning strategy for player
may require infinite memory, but it can always be implemented by an
effectively constructible one-counter automaton which reads the history of a
play. To get some intuition, consider the following game, where ν ( u a )=
{
a
}
and ν ( y )=
for all vertices y different from u a .

Custom Search