Game Development Reference

In-Depth Information

for each ordinal. Our aim is to leave the notion of the game arena unchanged

as the product of the structure and the formula. We wish only to change

the rules of the game to capture the nature of the inflationary fixed-point

operator.

The change we introduce to parity games is that either player is allowed to

backtrack
to an earlier position in the game, effectively to force a
countback

of the number of stages. That is, when a backtracking move is played, the

number of positions of a given priority that are backtracked are counted

and this count plays an important role in the succeeding play. The precise

definition is given in Section 4.6.2 below. The backtracking games we define

are more complex than parity games. Winning strategies are necessarily more

complicated, requiring unbounded memory, in contrast to the positional

strategies that work for parity games. Furthermore, deciding the winner is

Pspace-hard and remains hard for both NP and Co-NP even when games

have only two priorities. In contrast, parity games are known to be decidable

in NP
∩
Co-NP and in Ptime when the number of priorities is fixed. We will

explain how the model-checking problem for IFP can be represented in the

form of backtracking games. The construction allows us to observe that a

simpler form of backtracking game su
ces which we call
simple
backtracking

games, and we will see that the winning regions of simple backtracking games

are definable in IFP. Thus, we obtain a tight correspondence between the

game and the logic, as exists between LFP and parity games.

4.6.1 Inflationary fixed-point logic

The
inflationary fixed-point
of any operator
F.P
(
A
k
)
→P
(
A
k
)is

defined as the limit of the increasing sequence of sets (
R
α
)
α∈
Ord
defined as

R
0

∪ F
(
R
α
), and
R
λ
:=
α<λ
R
α
for limit ordinals
λ
.

The
deflationary fixed-point
of
F
is constructed in the dual way starting

with
A
k
as the initial stage and taking intersections at successor and limit

ordinals.

Inflationary fixed-point logic
(IFP) is obtained from FO by allowing

formulae of the form [
ifp
Rx.ϕ
(
R, x
)](
x
) and [
dfp
Rx.ϕ
(
R, x
)](
x
), for arbi-

trary
ϕ
, defining the inflationary and deflationary fixed-point of the operator

induced by
ϕ
.

To illustrate the power of IFP, we present here a few examples of situations

where inflationary and deflationary fixed-points arise.

:=
∅
,
R
α
+1

:=
R
α

Bisimulation.

=(
V,E,P
1
,...,P
m
) be a transition system with a

binary transition relation
E
and unary predicates
P
i
. Bisimilarity on

Let

K

K

is

Search Nedrilad ::

Custom Search