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