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