Game Development Reference
InDepth 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 finitestate stochastic turnbased 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 finitestate 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
onecounter 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
.
Search Nedrilad ::
Custom Search