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