Game Development Reference

In-Depth Information

simple backtracking games, i.e., the winning regions of simple backtracking

games are IFP-definable.

Since backtracking games are extensions of parity games we start with

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|

Search Nedrilad ::

Custom Search