Game Development Reference
InDepth 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 finitestate automaton
M
ψ
which
accepts the language
L
ψ
. If the acceptance condition is Rabinchain (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 finitestate automata that
cannot be encoded as LTL formulae. We refer to Thomas [1991] for more
details.
There is a close connection between lineartime 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
finitestate 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 infinitestate games. Some
of the reasons are mentioned below.
×
•
For infinitestate 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 finitestate control, which can also encode the structure of
M
.
However, this does not necessarily work if the finitestate 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.
Search Nedrilad ::
Custom Search