Game Development Reference
In-Depth Information
simple backtracking games, i.e., the winning regions of simple backtracking
games are IFP-definable.
the formula defining winning regions in parity games. We take this formula
as a starting point for defining an IFP-formula deciding the winner of
backtracking games. To define strategies involving backtracking, we first need
some preparation. In particular, in order to measure distances we need an
ordering on the arenas.
It is easily seen that backtracking games are invariant under bisimulation.
Thus, it su ces to consider arenas where no two distinct nodes are bisimilar
(we refer to such arenas as bisimulation minimal ). The next step is to
define an ordering on the nodes in an arena. This is done by ordering the
bisimulation types realised in it.
Indeed, we have seen above that there is a formula ϕ ord ( x, y ) IFP
defining on every bisimulation minimal arena a linear order. As a result,
we can assume that the backtracking games are ordered and that we are
given an arithmetical predicate for addition with respect to the order defined
above.
Theorem 4.28, saying that there exist backtracking games whose winning
strategies require infinite memory, also applies to games with local strategies.
In general, the reason for the increased memory consumption is that when
the decision to backtrack is made, it is necessary to know which nodes
have been seen in the past, i.e., to which node a backtracking move is
possible. Furthermore, after a backtracking move occurred, both players
have to remember the backtracking distance, as this determines their further
moves. However, since here we consider strategies with local backtracking
only, it su ces to know the distance of the backtracking moves that are still
active, i.e., have not yet been released, whereas the history of the play in
terms of nodes visited may safely be forgotten. Thus we can capture all the
relevant information about a partial play π ending in position v by the tuple
( v, d π (0) ,...,d π ( k
1)), where d π denotes the distance function.
In a ba ck tracking game with priorities 0 ,..., k
1, a configuration is
) k . Let π be
a (partial) play ending in node v . The configuration of π is defined as the
tuple ( v, d π (0) ,...,d π ( k )).
Recall that in a simple backtracking game the distance of all backtracking
moves is at most n :=
a pair ( v, d ) consisting of a node v and a tuple d
(
N ∪ {∞}
. Furthermore we can assume that we are given a
linear order on the nodes of the game graph. Thus the configurati on of any
(partial) play π in a simple game can be represented by a pair ( v, d ) where
|G|