Game Development Reference
In-Depth Information
= ν M iff w is accepted by M , where w is the infinite word defined
by w ( i )= ν ( w ( i ))
that w
|
Ap ( M ). Let us note that every LTL formula ψ can be
effectively translated into an equivalent finite-state automaton M ψ which
accepts the language L ψ . If the acceptance condition is Rabin-chain (or
more powerful), the automaton M ψ can be effectively transformed into an
equivalent deterministic automaton with the same acceptance condition. In
general, the cost of translating ψ into M ψ is at least exponential. On the
other hand, there are properties expressible by finite-state automata that
cannot be encoded as LTL formulae. We refer to Thomas [1991] for more
details.
There is a close connection between linear-time objectives and the ω -regular
payoffs introduced in the previous section. Since this connection has several
subtle aspects that often lead to confusion, it is worth an explicit discussion.
Let M =( Q, 2 Ap ( M ) ,
,q 0 , Acc )bea deterministic finite-state automaton,
where Q is a finite set of control states, 2 Ap ( M ) is the input alphabet,
−→⊆
Q × 2 Ap ( M )
× Q is a total transition function, and Acc some acceptance
criterion. Then we can construct a synchronous product of the game G and
M , which is a stochastic game G × M where V × Q is the set of vertices
partitioned into ( V ×Q, V ×Q, V ×Q ) and ( v, q ) ( v ,q )iff v → v and
q A
−→ q where A = ν ( q ) ∩Ap ( M ). Since M is deterministic and the transition
function of M is total, the probability assignment is just inherited from
G (i.e., ( v, q )
x
x
→ v ). Further, the acceptance criterion
of M is translated into the corresponding ω -regular payoff over the runs
of G
( v ,q ) only if v
M is constructed so that
M just observes the runs of G and the constructed ω -regular payoff just
reflects the accepting/rejecting verdict of this observation. Thus, we can
reduce the questions about the existence and effective constructibility of a
( P M )-winning strategy for player
×
M in the natural way. Note that G
×
in a vertex v of G to the questions
about the value and effective constructibility of an optimal maximising
strategy in the vertex ( v, q 0 )of G
M . However, this reduction does not
always work completely smoothly, particularly for infinite-state games. Some
of the reasons are mentioned below.
×
For infinite-state games, the product G × M is not necessarily definable
in the same formalism as the original game G . Fortunately, most of the
studied formalisms correspond to abstract computational devices equipped
with a finite-state control, which can also encode the structure of M .
However, this does not necessarily work if the finite-state control is trivial
(i.e., it has just one or a fixed number of control states) or if it is required
to satisfy some special conditions.