Game Development Reference

In-Depth Information

4.6.4 Definability of winning regions in backtracking games

We have seen that backtracking games can be used as model-checking games

for IFP. We will now identify a natural subclass of backtracking games,

which we call
simple
which is balanced with IFP. This means that for every

formula
ϕ

,ϕ
) can trivially be

modified to fall within this class and, on the other hand, for every
d

∈

IFP and finite structure

A

, the game

G

(

A

∈
N

there is a formula
ϕ

IFP defining the winning region for Player 0 in any

simple backtracking game with at most
d
priorities. In this sense, simple

backtracking games precisely capture IFP model-checking.

Consider the model-checking game

∈

,ϕ
) and the way backtracking was

used there: if Player
0
wa
n
ted to backtrack it was always after opening
a

fixed-point, say [
ifp
Rx.Rx

G

(

A

ϕ
]. She then looped
α
times through the
Rx

sub-formula and backtracked. By choosing the
α
she e
sse
ntially picked a

stage of the fixed-point induction on
ϕ
and claimed that
x

∨

ϕ
α
. From this

observation we can derive two important consequences. As every inflationary

fixed-point induction must close after polynomially many steps in the size of

the structure

∈

and therefore in linearly many steps in terms of the game

graph, there is no need for Player 0 to backtrack more than
n
steps, where

n
is the size of the game graph. Further, the game can easil
y
be modified

such that inst
e
ad of having the nodes for the disjunction
Rx

A

ϕ
and the

sub-formula
Rx
, we simply have a node for
ϕ
with a self-loop. In this modified

game graph, not only is it su
cient for Player 0 to backtrack no more than

n
steps, we can, in addition, require that whenever she backtracks from

anode
v
,itmustbeto
v
again, i.e., when she decides to backtrack from

a node corresponding to the formula
ϕ
, she loops
α
times through
ϕ
and

then backtracks
α
steps to
ϕ
again. The same is true for Player 1 and her

backtracking.

We call a strategy in a backtracking game

∨

local
if all backtracking

moves from any node
v
are to a previous occurrence of
v
. Given a function

f.
N
→
N, we call a strategy
f
-backtracking if all backtracking moves made

by the strategy have distance at most
f
(
|G|
). The strategy is called
linear

in case
f
(
n
)=
n
and
polynomial
if
f
is a polynomial in
n
.

A backtracking game

G

:= (
V,E,V
0
,V
1
,B,
Ω) is
simple
, if every node in

B
has a self-loop and both players have local linear winning strategies on

their winning regions.

G

Theorem 4.31
For any
IFP
-formula ψ and every finite structure
A
, the

model-checking game

G

(

A

,ϕ
)
, as defined in Section 4.6.3, is simple.

We now want to show that the logic IFP is balanced with the class of

Search Nedrilad ::

Custom Search