Game Development Reference

In-Depth Information

4.6 Inflationary fixed-point logic and backtracking games

LFP and the modal
μ
-calculus are not the only logics based on fixed-point

operators. In the context of finite model theory, a rich variety of fixed-point

operators has been studied due to the close connection that the resulting

logics have with complexity classes. One of the most prominent fixed-point

logics is IFP, the logic of
inflationary fixed points
. In finite model theory

the logics IFP and LFP have often been used interchangeably as it has long

been known that they have equivalent expressive power on finite structures.

More recently, it has been shown by Kreutzer [2004] that the two logics are

equally expressive even without the restriction to finite structures. However,

it has also been proved by Dawar et al. [2004] that MIC, the extension

of propositional modal logic by inflationary fixed-points, is vastly more

expressive than the modal
μ
-calculus
L
μ
and that LFP and IFP have very

different structural properties even when they have the same expressive

power. This exploration of the different nature of the fixed-point operators

leads naturally to the question of what an appropriate model-checking game

for IFP might look like.

Our analysis of why parity games are the appropriate model-checking games

for LFP logics relied on the
well-foundedness
of the inductive definition of

a
least fixed-point. The Verifier who is trying to prove that a certain tuple

a
belongs to a least fixed-point relation
R
, needs to p
re
sent a well-founded

justification for its inclusion. That is, the inclusion of
a
in
R
may be based

on the inclusion of other elements in
R
whose inclusion in turn needs to be

justified but the entire process must be well-founded. On the other hand, the

justification for including an element in a greatest fixed-point may well be

circular. This interaction between sequences that are required to be finite and

those that are required to be infinite provides the structural correspondence

with parity games.

A key difference that arises when we consider inflationary fixed point
s

(and, dually, deflationary fixed-points) is that the stage at which a tuple
a

enters the construction of the fixed-point
R
may be an important part of the

justification for its inclusion. In the case of least and greatest fixed-points,

the operators involved are monotone. Thus, if the inclusion of
a
can be

justified at some stage, it can be justified at all later stages. In contrast, in

constructing an inflationary fixed-point, if
a
is included in the set, it is on the

basis of the immediately preceding stage of the iteration. It may be possible

to reflect this fact in the game setting by including the iteration stage as an

explicit component of the game position. However, this would blow up the

game enormously, since we would have to take a separate copy of the arena

Search Nedrilad ::

Custom Search