Game Development Reference
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
( 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  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
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 such as CTL, CTL ∗ , or ECTL ∗ (see, e.g., Emerson
) 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 ).
The syntax of PCTL ∗ path and state formulae is defined by the following