Game Development Reference

In-Depth Information

•

For infinite-state games, the reduction to
ω
-regular payoffs described above

can be problematic also because optimal maximising/minimising strategies

in infinite-state games with
ω
-regular payoffs (even reachability payoffs)

do not necessarily exist. For example, even if we somehow check that the

value of (
v, q
0
)in
G

×

M
is 1, this does yet mean that player

has a

(
P
=1
M
)-winning strategy in
v
.

•

For finite-state games, the two problems discussed above usually disappear.

However, there are still some issues related to complexity. In particular,

the results about the type of optimal strategies in
G

M
do not carry over

to
G
. For example, assume that we are given a linear-time objective
P
=1
M

where
M
is a deterministic Rabin-chain automaton. If
G
has finitely many

states, then
G×M
is also finite-state and hence we can rely on the results

presented by McIver and Morgan [2002] and Chatterjee et al. [2004b] and

conclude that the value of (
v, q
0
) is computable in time polynomial in

the size of
G

×

M
and there is an optimal maximising MD strategy
σ

computable in polynomial time. From this we can deduce that the existence

of a (
P
=1
M
)-winning strategy for player

×

in
v
is decidable in polynomial

time. However, since the optimal MD strategy
σ
may depend
both
on the

current vertex of
G
and the current state of
M
, we cannot conclude that

if player

has some (
P
=1
M
)-winning strategy in
v
, then he also has an

MD (
P
=1
M
)-winning strategy in
v
(still, the strategy
σ
can be translated

into a FD (
P
=1
M
)-winning strategy which simulates the execution of
M

on the history of a play).

To sum up, linear-time objectives
are
closely related to
ω
-regular payoffs,

but the associated problems cannot be seen as 'equivalent' in general.

Branching-time logics

Branching-time logics such as CTL, CTL
∗
, or ECTL
∗
(see, e.g., Emerson

[1991]) allow explicit existential/universal quantification over runs. Thus,

one can express that a given
path formula
holds for some/all runs initiated

in a given state.

In the probabilistic setting, the existential/universal path quantifiers are

replaced with the
probabilistic operator
P
introduced in the previous

section. In this way, every (non-probabilistic) branching-time logic determines

its probabilistic counterpart. The probabilistic variants of CTL, CTL
∗
, and

ECTL
∗
are denoted by PCTL, PCTL
∗
, and PECTL
∗
, respectively (see

Hansson and Jonsson [1994]).

The syntax of PCTL
∗
path
and
state
formulae is defined by the following

Search Nedrilad ::

Custom Search