Guarded fixed point logics and the monadic theory of countable trees.
Different variants of guarded logics (a powerful generalization of modal logics) are surveyed and an elementary proof for the decidability of guarded fixed point logics is presented. In a joint paper with Igor Walukiewicz, we proved that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time (E. Grdel and I. Walulkiewicz, Proc. 14th IEEE Symp. on Logic in Computer Science, 1999, pp. 45-54). That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. The exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width. Based on the tree model property, we show that the satisfiability problem for guarded fixed point formulae can be reduced to the monadic theory of countable trees (SS), or to the -calculus with backwards modalities.
Introduction
Guarded logics are dened by restricting quantication in rst-order logic,
second-order logic, xed point logics or innitary logics in such a way that,
semantically speaking, each subformula can 'speak' only about elements that
are 'very close together' or `guarded'.
Email address: graedel@informatik.rwth-aachen.de (Erich Gradel).
URL: www-mgi.informatik.rwth-aachen.de (Erich Gradel).
Preprint submitted to Elsevier Preprint 5 October 2000
Syntactically this means that all rst-order quantiers must be relativised by
certain 'guard formulae' that tie together all the free variables in the scope of
the quantier. Quantication is of the form
where quantiers may range over a tuple y of variables, but are 'guarded' by
a formula  that must contain all the free variables of the formula that is
quantied over. The guard formulae are of a simple syntactic form (in the basic
version, they are just atoms). Depending on the conditions imposed on guard
formulae, one has logics with dierent levels of 'closeness' or `guardedness'.
Again, there is a syntactic and a semantic view of such guard conditions.
Let us start with the logic GF, the guarded fragment of rst-order logic, as it
was introduced by Andreka, van Benthem, and Nemeti [1].
Denition 1.1. GF is dened inductively as follows:
(1) Every relational atomic formula Rx i 1
or x belongs to GF.
(2) GF is closed under boolean operations.
(3) If x; y are tuples of variables, (x; y) is a positive atomic formula, and
(x; y) is a formula in GF such that free( )  y, then
also the formulae
belong to GF.
Here free( ) means the set of free variables of . An atom (x; y) that rel-
ativizes a quantier as in rule (3) is the guard of the quantier. Hence in
GF, guards must be atoms. But the really crucial property of guards (also for
the more powerful guarded logics that we will consider below) is that it must
contain all free variables of the formula that is quantied over.
The main motivation for introducing the guarded fragment was to explain
and generalize the good algorithmic and model-theoretic properties of propositional
modal logics (see [1,26]). Recall that the basic (poly)modal logic ML
(also called propositional logic by the possibility to construct formulae
hai and [a] (for any a from a given set A of 'actions' or `modalities')
with the meaning that holds at some, respectively each, a-successor of the
current state. (We refer to [4] or [22] for background on modal logic).
Although ML is formally a propositional logic we really view it as a fragment
of rst-order logic. Kripke structures, which provide the semantics for modal
logics, are just relational structures with only unary and binary relations.
There is a standard translation taking every formula 2 ML to a rst-order
formula  (x) with one free variable, such that for every Kripke structure
K with a distinguished node w we have that K; w if and only if K
(w). This translation takes an atomic proposition P to the atom Px, it
commutes with the Boolean connectives, and it translates the modal operators
by quantiers as follows:
where E a is the transition relation associated with the modality a. The modal
fragment of rst-order logic is the image of propositional modal logic under
this translation. Clearly the translation of modal logic into rst-order logic uses
only guarded quantication, so we see immediately that the modal fragment
is contained in GF. The guarded fragment generalizes the modal fragment
by dropping the restrictions to use only two variables and only monadic and
binary predicates, and retains only the restriction that quantiers must be
guarded.
The following properties of GF have been demonstrated [1,10]:
(1) The satisability problem for GF is decidable.
(2) GF has the nite model property, i.e., every satisable formula in the
guarded fragment has a nite model.
(3) GF has (a generalized variant of) the tree model property.
Many important model theoretic properties which hold for rst-order
logic and modal logic, but not, say, for the bounded-variable fragments
do hold also for the guarded fragment.
(5) The notion of equivalence under guarded formulae can be characterized
by a straightforward generalization of bisimulation.
Further work on the guarded fragment can be found in [7{9,17]. Based on this
kind of results Andreka, van Benthem, and Nemeti put forward the 'thesis'
that it is the guarded nature of quantication that is the main reason for the
good model-theoretic and algorithmic properties of modal logics.
Let us discuss to what extent this explanation is adequate. One way to address
this question is to look at the complexity of GF. We have shown in
[10] that the satisability problem for GF is complete for 2Exptime, the
class of problems solvable by a deterministic algorithm in time 2 2 p(n)
, for some
polynomial p(n). This seems very bad, in particular if we compare it to the
well-known fact that the satisability problem for propositional modal logic
is in Pspace [19]. But dismissing the explanation of Andreka, van Benthem,
and Nemeti on these grounds would be too supercial. Indeed, the reason for
the double exponential time complexity of GF is just the fact that predicates
may have unbounded arity (wheras ML only expresses properties of graphs).
Given that even a single predicate of arity n over a domain of just two element
leads to 2 2 n
possible types already on the atomic level, the double exponential
lower complexity bound is hardly a surprise. Further, in most of the potential
applications of guarded logics the arity of the relation symbols is bounded.
But for GF-sentences of bounded arity, the satisability problem can be decided
in Exptime [10], which is a complexity level that is reached already for
rather weak extensions of ML (e.g. by a universal modality) [25]. Thus, the
complexity analysis does not really provide a decisive answer to our question.
To approach the question from a dierent angle, let us look at extensions of
ML. Indeed ML is a very weak logic and the really interesting modal logics
extend ML by features like path quantication, temporal operators, least and
greatest xed points etc. which are of crucial importance for most computer
science applications. It has turned out that many of these extended modal logics
are algorithmically still manageable and actually of considerable practical
importance. The most important of these extensions is the modal -calculus
, which extends ML by least and greatest xed points and subsumes most of
the modal logics used for automatic verication including CTL, LTL, CTL  ,
PDL, and also many description logics. The satisability problem for L  is
known to be decidable and complete for Exptime [5]. Therefore, a good test
for the explanation put forward by Andreka, van Benthem, and Nemeti is the
following problem:
If we extend GF by least and greatest xed points, do we still get a decidable
logic? If yes, what is its complexity? To put it dierently, what is the penalty,
in terms of complexity, that we pay for adding xed points to the guarded
In [13] we were able to give a positive answer to this question. The model-theoretic
and algorithmic methods that are available for the -calculus on
one side, and the guarded fragments of rst-order logic on the other side, can
indeed be combined and generalized to provide positive results for guarded
xed point logics. (Precise denitions for these logics will be given in the next
section.) In fact we could establish precise complexity bounds.
Theorem 1.2 (Gradel, Walukiewicz). The satisability problems for
guarded xed point logics are decidable and 2Exptime-complete. For guarded
xed point sentences of bounded width the satisability problem is Exptime-
complete.
By the width of a formula , we mean the maximal number of free variables
in the subformulae of . For sentences that are guarded in the sense of GF,
the width is bounded by the maximal arity of the relation symbols, but there
are other variants of guarded logics where the width may be larger. Note that
for guarded xed point sentences of bounded width the complexity level is the
same as for -calculus and for GF without xed points.
The proof that we give in [13] relies on alternating two-way tree automata
(on trees of unbounded branching), on a forgetful determinacy theorem for
parity games, and on a notion of tableaux for guarded xed point sentences,
which can be viewed as tree representations of structures. We associate with
every guarded xed point sentence an alternating tree automaton A that
accepts precisely the tableaux that represent models for . This reduces the
satisability problem for guarded xed point logic to the emptiness problem
for alternating two-way tree automata.
In this paper we discuss other variants of guarded logics, with more liberal notions
of guarded quantication and explain alternative possibilities to design
decision procedures for guarded xed point logics. Already in [3], van Benthem
had proposed loosely guarded quantication (also called guarded
quantication) as a more general way of restricting quantiers, and proved
that also LGF, the loosely guarded fragment of rst-order logic, remains de-
cidable. Here we motivate and introduce clique guarded quantication, which
is even more liberal than loosely guarded quantication, but retains the same
decidability properties.
The techniques for establishing decidability results for guarded xed point
logics that we explain in this paper exploit a crucial property of such logics,
namely the (generalized variant of the) tree model property, saying that every
satisable sentence of width k has a model of tree width at most k 1. The tree
width of a structure is a notion coming from graph theory which measures how
closely the structure resembles a tree. Informally a structure has tree width
k, if it can be covered by (possibly overlapping) substructures of size at
most are arranged in a tree-like manner. The tree model property
for guarded logics is a consequence of their invariance under a suitable notion
of bisimulation, called guarded bisimulation.
Guarded bisimulations play a fundamental role for characterizing the expressive
power of guarded logics, in the same way as usual bisimulations are crucial
for understanding modal logics. For instance, the characterization theorem by
van Benthem [2], saying that a property is denable in propositional modal
logic if and only if it is rst-order denable and invariant under bisimulation.
has a natural analogue for the guarded fragment: GF can dene precisely the
model classes that are rst-order denable and invariant under guarded bisimulation
[1]. We will explain and prove a similar result for the clique-guarded
fragment in Section 3. There is a similar and highly non-trivial characterisation
theorem for the modal -calculus, due to Janin and Walukiewicz [18],
saying that the properties denable in the modal -calculus are precisely the
properties that are denable in monadic second-order logic and invariant under
bisimulation. And, as shown recently by Gradel, Hirsch, and Otto [12],
this result also carries over to the guarded world. Indeed, there is a natural
fragment of second-order logic, called GSO, which is between monadic second-order
logic and full second-order logic, such that guarded xed point logic is
precisely the bisimulation-invariant portion of GSO.
Outline of the paper. In Sect. 2 we discuss dierent variants of guarded
logics. In particular we introduce the notion of clique-guarded quantication
and present the precise denitions and elementary properties of guarded xed
point logics. In Sect. 3 we explain the notions of guarded bisimulations, of
tree width and of the unraveling of a structure. We prove a characterization
theorem for the clique-guarded fragment and discuss the tree model property
of guarded logics. Based on the tree model property we will present in Sect. 4.2
a simpler decidability proof for guarded xed point logic that replaces the
automata theoretic machinery used in [13] by an interpretation argument into
the monadic second-order theory of countable trees (S!S) which by Rabin's
famous result [23] is known to be decidable. We then show in Sect. 4.3 that
instead of using S!S, one can also reduce guarded xed point logic to the
-calculus with backwards modalities which has recently been proved to be
decidable (in Exptime, actually) by Vardi [27].
We remark that this paper is to a considerable extent expository. The new
results, mostly concerning clique-guarded logics, can also be derived using
the automata theoretic techniques of [13]. However, it is worthwhile to make
the role of guarded bisimulations explicit and to show how one can establish
decidability results for guarded xed point logics via reductions to well-known
formalisms such as S!S or the -calculus. Even if the automata theoretic
method gives more ecient algorithms, the reduction technique provides a
simple and high-level method for proving decidability, avoiding any explicit
use of automata-theoretic machinery (the use of automata is hidden in the
decision algorithms for S!S or the -calculus). For the convenience of the
reader, we have included explicit proofs of some facts that are known | or
straightforward variations of known results | but where the proofs are hard
to nd.
Guarded logics
There are several ways to dene more general guarded logics than GF. On one
side, we can consider other notions of guardedness, and on the other side we
can look at guarded fragments of more powerful logics than rst-order logic.
We rst consider other guardedness conditions.
Loosely guarded quantication. The direct translation of temporal formulae
say over the temporal frame (N ; <), into rst-order logic
is
which is not guarded in the sense of Denition 1.1. However, the quantier 8z
in this formula is guarded in a weaker sense, which lead van Benthem [3] to
the following generalization of GF.
Denition 2.1. The loosely guarded fragment LGF is dened in the same
way as GF, but the quantier-rule is relaxed as follows:
is in LGF, and (x; is a conjunction of
atoms, then
belong to LGF, provided that free( )  any two
variables z 2 y, z 0 2 x[ y there is at least one atom  j that contains both
z and z 0 .
In the translation of ( until ') described above, the quantier 8z is loosely
guarded by (x  z^z < y) since z coexists with both x and y in some conjunct
of the guard. On the other side, the transitivity axiom
Exz) is not in LGF. The conjunction Exy ^ Eyz is not a proper guard of
8xyz since x and z do not coexist in any conjunct. Indeed, it has been shown
in [10] that there is no way to express transitivity in LGF.
Clique-guarded quantication. In this paper we introduce a new, even
more liberal, variant of guarded quantication, which leads to what we may
call clique-guarded logics. To motivate this notion, let us look at the semantic
meaning of guardedness.
Denition 2.2. Let B be a structure with universe B and vocabulary  . A
set guarded in B if there exists an atomic formula
Note that every singleton set
guarded (by the atom is guarded
some guarded set X.
Clearly, sentences of GF can refer only to guarded tuples. Consider now the
LGF-sentence
While the rst quantier is guarded even in the sense of GF, the second one
is only loosely guarded: the quantied variables u; v coexist in an atom of the
guard (in fact in both of them) and they also coexist with each of the other
z in one of the atoms. The subformula ' can hence talk about
quadruples (y; z; u; v) in a structure, that are not guarded in the sense of the
denition just given, but in weaker sense.
The corresponding semantic denition of a loosely guarded set in a structure
B is inductive.
Denition 2.3. A set X is loosely guarded in the structure B if it either is
a guarded set, or if there exists a loosely guarded set X 0 such that for every
there is a guarded set Y with fa; bg  Y  X.
For instance in the structure
and a ternary relation consisting of the triples (a; b; c); (b; d; e); (c; d; e), the set
fb; c; d; eg is loosely guarded. Note that the elements of a loosely guarded set
need not coexist in a single atom of the structure, but they are all 'adjacent'
in the sense of the locality graph or Gaifman graph of a structure.
Denition 2.4. The Gaifman graph of a relational structure B (with universe
B) is the undirected graph
there exists a guarded set X  B with a; a 0 2 Xg:
set X of elements of a structure B is clique-guarded in B if it induces a
clique in G(B). A tuple (b clique-guarded if its components
form a clique-guarded set.
Lemma 2.5. Every loosely guarded set is also clique-guarded.
Proof. We proceed by induction on the denition of a loosely guarded set. If
X is guarded, then it is obviously also clique-guarded. Otherwise there exists
a loosely guarded set X 0 and, for every a 2 X X 0 , b 2 X a guarded set
containing both a and b. Hence all such a and b are connected in G(B). It
remains to consider elements b that are both contained in X [ X 0 . In that
case, a and b are connected in G(B) because, by induction hypothesis, X 0
induces a clique in G(B).
The converse is not true, as the following example shows. Consider a structure
and one ternary relation
R containing the triangles (a 1 ; a
is neither guarded nor loosely guarded, but induces a clique in G(A).
Note that for each nite vocabulary  and each k 2 N , there is a positive, existential
rst-order formula clique(x
B and all b
induce a clique in G(B):
Denition 2.6. The clique-guarded fragment CGF of rst-order logic is dened
in the same way as GF and LGF, but with the clique-formulae as guards.
Hence, the quantication rule for CGF is
(3) 00 If (x; y) is a formula CGF, then
belong to CGF, provided that free( )  y.
Note that quantiers over tuples are in principle no longer needed in CGF
(contrary to GF and LGF), since they can be written as sequences of clique-
guarded quantiers over single variables.
Alternative denitions of CGF. In practice, one will of course not write
down the clique-formulae explicitly. One possibility is not to write them down
at all, i.e., to take the usual (unguarded) rst-order syntax and to change
the semantics of quantiers so that only clique-guarded tuples are considered.
More precisely: let '(x; y) be a rst-order formula, B a structure and a be
a clique-guarded tuple of elements of B. Then B there exists
an element b such that (a; b) is clique-guarded and B
for universal quantiers. It is easy to see that, for nite vocabularies, this
semantic denition of CGF is equivalent to the one given above.
An alternative possibility is to permit as guards any existential positive formul

(x) that implies clique(x). This is what Maarten Marx [20,16] uses in
his denition of the packed fragment PF. The dierences between the clique-
guarded fragment and the packed fragment are purely syntactical. PF and
CGF have the same expressive power. The work of Maarten Marx and ours
have been done independently.
Every LGF-sentence is equivalent to a CGF-sentence. (The analogous statement
for formulae is only true if we impose that the free variables must be
interpreted by loosely guarded tuples. However, in this paper, we restrict attention
to sentences.) We observe that CGF has strictly more expressive power
than LGF.
Proposition 2.7. The CGF-sentence 8xyz(clique(x; Rxyz) is not
equivalent to any sentence in LGF.
The good algorithmic and model-theoretic properties of GF go through also
for LGF and CGF. In most cases, in particular for decidability, for the characterization
via an appropriate notion of guarded bisimulation and for the
tree model property, the proofs for GF extend without major diculties. An
exception is the nite model property which, for GF, has been established in
[10], and where the extension to LGF and CGF, recently established by Ian
Hodkinson [15], requires considerable eort.
Notation. We use the notation
i.e., we write guarded formulae in the form
When this notation is used, then it is always understood that  is indeed a
proper guard as specied by condition (3), (3) 0 , or (3) 00 .
Guarded xed point logics. We now dene guarded xed point logics,
which can be seen as the natural common extensions of GF, LGF and CGF
on one side, and the -calculus on the other side.
Denition 2.8. The guarded xed point logics GF; LGF, and CGF are
obtained by adding to GF; LGF, and CGF, respectively, the following rules
for constructing xed point formulae:
Let W be a k-ary relation a k-tuple of distinct vari-
ables, and (W; x) be a guarded formula that contains only positive occurrences
of W , no free rst-order variables other than x
is not used in guards. Then we can build the formulae
The semantics of the xed point formulae is the usual one: Given a structure
A providing interpretations for all free second-order variables in , except W ,
the formula (W; x) denes an operator on k-ary relations W  A k , namely
Since W occurs only positively in , this operator is monotone (i.e., W  W 0
implies A (W )  A (W 0 )) and therefore has a least xed point LFP( A )
and a greatest xed point GFP( A ). Now, the semantics of least xed point
formulae is dened by
A
and similarly for the greatest xed points.
Least and greatest xed point can be dened inductively. For a formula (W; x)
with k-ary relation variable W a structure A, and ordinals  set
~
W  for limit ordinals
The relations W  (resp. ~
are called the stages of the LFP-induction (resp.
GFP-induction) of (W; x) on A. Since the operator A is monotone, we have
~
W +1     , and there exist ordinals ;  0 such that W
~
These are called the closure ordinals of the LFP-induction
resp. GFP-induction of (W; x) on A.
Finite and countable models. Contrary to GF, LGF, CGF, and also to
the modal -calculus, guarded xed point logics do not have the nite model
property [13].
Proposition 2.9. Guarded xed point logic GF (even with only two vari-
ables, without nested xed points and without equality) contains innity axioms

Proof. Consider the conjunction of the formulae
9xyFxy
The rst two formulae say that a model should contain an innite F -path
and the third formula says that F is well-founded, thus, in particular, acyclic.
Therefore every model of the three formulae is innite. On the other side, the
are clearly satisable, for instance by (!; <).
While the nite model property fails for guarded xed point logics we recall,
for future use, that the Lowenheim-Skolem property is true even for the (un-
guarded) least xed point logic every satisable xed point
sentence has a countable model. This result is part of the folklore on xed
point logic, but it is hard to nd a published proof. Our exposition follows the
one in [6].
Theorem 2.10. Every satisable sentence in hence every
satisable sentence in GF, LGF, or CGF, has a model of countable
cardinality.
Proof. Consider a xed point formula of form (x) := [LFP Rx : '(R; x)](x),
with rst-order ' such that A j= (a) for some innite model A.
For any ordinal , let R  be stage  of the least xed point induction of ' on
A.
Expand A by a monadic relation U , a binary relation <, and a m
relation (where m is the arity of R) such that
(1) (U; <) is a well-ordering of length
1, and < is empty outside U .
describes the stages of ' A in the following way
; u is the -th element of (U; <),
and b 2 R  g:
In the expanded structure A  := (A; U; <; S) the stages of the operator ' A are
dened by the sentence
:= 8u8x
Here '[Ry=9z(z < is the formula obtained form '(R; x) by
replacing all occurrences of subformula Ry by 9z(z <
be a countable elementary substructure of A  ,
containing the tuple a. Since A
the stages of ' B . Since also B  j= 9uSua, it follows that a is contained in the
least xed point of ' B , i.e., B (a).
A straightforward iteration of this argument gives the desired result for arbitrary
nestings of xed point operators, and hence for the entire xed point
Guarded innitary logics. It is well known that xed point logics have a
close relationship to innitary logics (with bounded number of variables).
Denition 2.11. GF are the innitary variants of the
guarded fragments GF, LGF, and CGF, respectively. For instance GF 1 extends
GF by the following rule for building new formulae: If   GF 1 is any
set of formulae, then also W  and V  are formulae of GF 1 . The denitions
for LGF 1 and CGF 1 are anologous.
In the sequel we explicitly talk about the clique-guarded case only, i.e., about
CGF and CGF 1 , but all results apply to the guarded and loosely guarded
case as well. The following simple observation relates CGF with CGF 1 .
Proposition 2.12. For each 2 CGF of width k and each cardinal
, there
is a 0 2 CGF 1 , also of width k, which is equivalent to on all structures up
to cardinality
Proof. Consider a xed point formula [LFP Rx : '(R; x)](x). For every ordinal
, there is a formula '  (x) 2 CGF 1 that denes the stage  of the
induction of '. Indeed, let ' 0 (x) := false, let ' +1 (x) := '[Ry='  (y)](x),
that is, the formula that one obtains from '(R; x) if one replaces each atom
Ry (for any y) by the formula '  (y), and for limit ordinals , let '  (x) :=
On structures of bounded cardinality, also the closure ordinal of
any xed-point formula is bounded. Hence for every cardinal
there exists an
ordinal  such that [LFP Rx : '(R; x)](x) is equivalent to '  (x) on structures
of cardinality at most
Remark. Without the restriction on the cardinality of the structures, this
result fails. Indeed there are very simple xed point formulae, even in the
modal -calculus (such as well-foundedness axioms), that are not equivalent
to any formulae of the full innitary logic L1! .
Guarded bisimulation and the tree model property
Tree width is an important notion in graph theory. Many dicult or undecidable
computational problems on graphs become easy on graphs of bounded
tree width. The tree width of a structure measures how closely it resembles a
tree. Informally, a structure has tree width  k, if it can be covered by (pos-
sibly overlapping) substructures of size at most k + 1 which are arranged in a
tree-like manner. For instance, trees and forests have tree width 1, cycles have
tree width 2, and the n  n-grid has tree width n. Here we need the notion
of tree width for arbitrary relational structures. For readers who are familiar
with the notion of tree width in graph theory we can simply say that the tree
width of a structure is the tree width of its Gaifman graph. Here is a more
detailed denition.
Denition 3.1. A structure B (with universe B) has tree width k if k is
the minimal natural number satisfying the following condition. There exists a
directed tree E) and a function
assigning to every node v of T a set F (v) of at most k +1 elements of B, such
that the following two conditions hold.
(i) For every guarded set X in B there exists a node v of T with X  F (v).
(ii) For every element b of B, the set of nodes fv
connected (and hence induces a subtree of T ).
For each node v of T , F (v) induces a substructure F(v)  B of cardinality at
most k + 1. (Since F (v) may be empty, we also permit empty substructures.)
is called a tree decomposition of width k of B.
Remark. A more concise, but equivalent, formulation of clause (i) would be
that
v2T F(v).
By denition, every guarded set X  B is contained in some F (v). A simple
graph theoretic argument shows that the same is true for loosely guarded and
clique-guarded sets.
Lemma 3.2. Let hT; (F(v) v2T )i be a tree decomposition of B and X  B be a
clique-guarded set in B. Then there exists a node v of T such that X  F (v).
Proof. For each b 2 X, let V b be the set of nodes v such that b 2 F (v). By
the denition of a tree decomposition, each V b induces a subtree of T . For all
is non-empty, since b and b 0 are adjacent
in G(B) and must therefore coexist in some atomic fact that is true in B. It
is known that any collection of pairwise overlapping subtrees of a tree has a
common node (see e.g. [24, p. 94]). Hence there is a node v of the T such that
F (v) contains all elements of X.
Guarded bisimulations. The notion of bisimulation from modal logic generalises
in a straightforward way to various notions of guarded bisimulation
that describe indistinguishability in guarded logics. We focus here on clique-
bisimulations, the appropriate notion for clique-guarded formulae. The notions
of guarded or loosely guarded bisimulations can be dened analogously.
Denition 3.3. A clique-k-bisimulation, between two -structures A and B
is a non-empty set I of nite partial isomorphisms Y from A to B,
where X  A and Y  B are clique-guarded sets of size at most k, such that
the following back and forth conditions are satised. For every
I,
for every clique-guarded set X 0  A of size at most k there exists a
partial isomorphism in I such that f and g agree on X \ X 0 .
back: for every clique-guarded set Y 0  B of size at most k there exists a
partial isomorphism in I such that f 1 and g 1 agree on Y \Y 0 .
Clique-bisimulations are dened in the same way, without restriction on the
size of X; Y; X 0 and Y 0 . Two -structures A and B are clique-(k-)bisimilar if
there exists a cliqe-(k-)bisimulation between them. Obviously, two structures
are clique-bisimilar if and only if they are clique-k-bisimilar for all k.
Remark. One can describe clique-k-bisimilarity also via a guarded variant
of the innitary Ehrenfeucht-Frasse game with k pebbles. One just has to
impose that after every move, the set of all pebbled elements induces a clique
in the Gaifman graph of each of the two structures. Then A and B are clique-
k-bisimilar if and only if Player II has a winning strategy for this guarded
game.
Adapting basic and well-known model-theoretic techniques to the present sit-
uation, one obtains the following result.
Theorem 3.4. Let A and B be two -structures. The following are equivalent:
(i) A and B are clique-k-bisimilar.
(ii) For all sentences 2 CGF 1 of width at most k, A
Proof. (i) =) (ii): Let I be a clique-k-bisimulation between A and B, let
formula in CGF 1
with width at most k such that A
We show, by induction on , that there is no partial isomorphism f 2 I with
. By setting the claim follows.
If is atomic this is obvious, and the induction steps for
are immediate. Hence the only interesting case concerns formulae
of the form
Since A j= (a), there exists a tuple a 0 in A such that A j= clique(a; a
'(a; a 0 ). Suppose, towards a contradiction, that some f 2 I takes a to b. Since
the set a[a 0 is clique-guarded there exists a partial isomorphism g 2 I, taking
a to b and a 0 to some tuple b 0 in B. But then the tuple b[b 0 is clique-guarded
and B
contradicts the induction hypothesis.
(ii) =) (i): Let I be the set of all partial isomorphisms f : a 7! b, taking a
clique-guarded tuple a in A to a clique-guarded tuple b in B such that for all
of width at most k, A
and B cannot be distinguished by sentences of width k in CGF 1 , I contains
the empty map and is therefore non-empty. It remains to show that I satises
the back and forth properties.
For the forth property, take any partial isomorphism I and any
clique-guarded set X 0 in A of size at most k. Let X
g. We have to show that there exists a g 2 I,
dened on X 0 that coincides with f on X \ X 0 .
Suppose that no such exists. Let a = a
and let T be the set of all tuples b
s such that b[b
0 is clique-guarded
in B. Since there is no appropriate g 2 I there exists for every tuple b
(a; a 0
But then we can construct the formula
Clearly, A j= (a) but B which is impossible, given that f 2 I maps
a to b. The proof for the back property is analogous.
In particular, this shows that clique-(k-)bisimilar structures cannot be separated
by CGF-sentences (of width k).
Characterizing CGF via clique-guarded bisimulations. We show next
that the characterisations of propositional modal logic and GF as bisimulation-
invariant fragments of rst-order logic [1,2] have their counterpart for CGF
and clique-guarded bisimulation. The proof is a straightforward adaptation of
van Benthems proof for modal logic, but for the convenience of the reader,
we present it in full. However, we assume that the reader is familiar with the
notions of elementary extensions and !-saturated structures (see any textbook
on model theory, such as [14,21]). We recall that every structure has an !-
saturated elementary extension.
Theorem 3.5. A rst-order sentence is invariant under clique-guarded bisimulation
if and only if it is equivalent to a CGF-sentence.
Proof. We have already established that CGF-sentences (in fact even sentences
from CGF 1 ) are invariant under clique-guarded bisimulations. For the
converse, suppose that is a satisable rst-order sentence that is invariant
under clique-guarded bisimulations. Let  be the set of sentences ' 2 CGF
such that It suces to show that  j= . Indeed, by the compactness
theorem, already a nite conjunction of sentences from  will then imply, and
hence be equivalent to, .
Since was assumed to be satisable, so is . Take any model A j= . We
have to prove that A j= . Let TCGF (A) be the CGF-theory of A, i.e., the set
of all CGF-sentences that hold in A.
is satisable.
Otherwise there were sentences such that
CGF-sentence implied by and is
therefore contained in . But then A which is impossible
since This proves the claim.
Take any model B be !-saturated
elementary extensions of A and B, respectively.
are clique-bisimilar.
Let I be the set of partial isomorphisms Y from clique-guarded
subsets of A + to clique-guarded subsets of B + such that, for all formulae
'(x) in CGF and all tuples a from X, we have that A +
'(fa). The fact that A are !-saturated implies that the back and
forth conditions for clique-guarded bisimulations are satised by I. Indeed,
let f 2 X, and let X 0 be any clique-guarded set in A + , with X 0 \
g. Let  be the set of all formulae of form
For every formula '(fa; y) 2 , we have A
therefore Hence  is a consistent type
of which is, by !-saturation, realized in B + by some xed tuple b
such that (fa; b) is clique-guarded. Hence the function g taking a to fa and
a 0 to b is a partial isomorphism with domain X 0 that coincides with f on
. The back property is proved in the same way, exploiting that A + is
!-saturated.
We can now complete the proof of the theorem. Since B
an elementary extension of B, we have that By assumption, is
invariant under clique-guarded bisimulations, so A + j= and therefore also
A
An analogous result applies to clique-k-bisimulations and CGF-sentences of
width k, for any k 2 N .
Unravelings of structures. The k-unraveling B (k) of a structure B is dened
inductively. We build a tree T , together with functions F and G such that
for each node v of T , F (v) induces a clique-guarded substructure F(v)  B,
and G(v) induces a substructure G(v)  B (k) that is isomorphic to F(v).
Further, hT; (G(v)) v2T i will be a tree decomposition of B (k) .
The root of T is , with F Given a node v of T with F
r g we create for every clique-guarded set
in B with s  k a successor node w of v such that F
and G(w) is a set fb
s g which is dened as follows. For
those i, such that b
j so that G(w) has the same
overlap with G(v) as F (w) has with F (v). The other b
in G(w) are fresh
elements.
G(w) be the bijection taking b i to b
F(w) being the substructure of B induced by F (w), dene G(w) so that f w
is an isomorphism from F(w) to G(w). Finally B (k) is the structure with tree
decomposition hT; (G(v) v2T )i.
Note that the k-unraveling of a structure has tree width at most k 1.
Proposition 3.6. B and B (k) are k-bisimilar.
Proof. Let I be the set of functions f nodes v of T .
It follows that no sentence of width k in CGF 1 , and hence no sentence of width
k in CGF distinguishes between a structure and its k-unraveling. Since every
satisable sentence in CGF has a model of at most countable cardinality,
and since the k-unraveling of a countable model is again countable we obtain
the following tree model property for guarded xed point logic.
Theorem 3.7 (Tree model property). Every satisable sentence in CGF
with width k has a countable model of tree width at most k 1.
Remark. In fact the decision algorithms for guarded xed point logics imply
a stronger version of the tree model property, where the underlying tree has
branching bounded by O(j
4 Decision procedures
Once the tree model property is established, there are several ways to design
decision algorithms for guarded logics. We focus here on guarded xed point
logics (in fact on CGF which contains GF and LGF).
4.1 Tree representations of structures
Let hT; be a tree decomposition of width k 1 of a -structure D
with universe D. We want to describe D by a tree with a nite set of labels.
To this end, we x a set K of 2k constants and choose a function f : D ! K
assigning to each element d of D a constant a d 2 K such that the following
condition is satised. If v; w are adjacent nodes of T , then distinct elements
of F(v) [ F(w) are always mapped to distinct constants of K.
For each constant a 2 K, let O a be the set of those nodes v 2 T at which
the constant a occurs, i.e., for which there exists an element d 2 F(v) such
that a. Further, we introduce for each m-ary relation R of D a tuple
R := (R a of monadic relations on T with
R a := fv 2 T : there exist d
The tree E) together with the monadic relations O a and R a (for
called the tree structure T (D) associated with D (and, strictly
speaking, with its tree decomposition and with K and f ).
Lemma 4.1. Two occurrences of a constant a 2 K at nodes u; v of T represent
the same element of D if and only if a occurs in the label of all nodes on
the link between u and v. (The link between two nodes u; v in a tree T is the
smallest connected subgraph of T containing both u and v.)
An arbitrary tree E) with monadic relations O a and R does dene
a tree decomposition of width k 1 of some structure D, provided that the
following axioms are satised.
(1) At each node v, at most k of the predicates O a are true.
(2) Neighbouring nodes agree on their common elements. For all m-ary relation
we have the axiom
8x8y
a2a
(O a x ^ O a y)
(R a x $ R a y)
These are rst-order axioms over the vocabulary   := fEg [ fO a : a 2
Kg. Given a tree structure T with underlying tree
E) and monadic predicates O a and R a satisfying (1) and (2), we obtain
a structure D such that T as follows. For every constant a 2 K, we
call two nodes u; w of T a-equivalent if T j= O a v for all nodes v on the link
between u and w. Clearly this is an equivalence relation on O T
a . We write [v] a
for the a-equivalence class of the node v. The universe of D is the set of all
a-equivalence classes of T for a 2 K, i.e.,
O a vg:
For every m-ary relation symbol R in  , we dene
(and hence all) v 2
4.2 Reduction to S!S
We now describe a translation from CGF into monadic second-order logic
on countable trees. Given a formula '(x
we construct a monadic second-order formula ' a
(z) with
describe in the associated tree structure
T (D) the same properties of clique-guarded tuples as '(x) does in D. (We
will make this statement more precise below).
On a directed tree E) we can express that U contains all nodes on
the link between x and y by the formula
For any set a  K we can then construct a monadic second-order formula
link a
a2a
O a z)
saying that the tuple a occurs at all nodes on the link between x and y. The
translation is now dened by induction as follows:
(1) If '(x) is an atom Sx i 1
(3) If '(x) := clique(x), let
clique a
a;a2a
9y(link a;a 0
_
_
(z).
' a (z) := 9y
link a
_
O
' a (z) := 8S
Here S is a tuple (S b ) b2K m of monadic predicates where m is the arity
of S.
Theorem 4.2. Let '(x) be a formula in CGF and D be a structure with
tree decomposition hT; For an appropriate set of constants K and
a (D) be the associated tree structure. Then, for
every node v of T and every clique-guarded tuple d  F(v) with
Proof. We proceed by induction on '. The non-trivial cases are the clique-
guards, existential quantication and least xed points.
For the clique-guards, note that the translated formula clique a (v) says that
for any pair a; a 0 of components of a, there is a node w, such that
a; a 0 occur at all nodes on the link from v to w and hence represent the same
elements at w as they do at v.
some predicate R and some tuple b that contains both
a and a 0 . By induction hypothesis, this means that d; d 0 are components of
some tuple d 0 such that D
Hence T (D) clique a (v) if and only if the tuple d induces a clique in the
Gaifman graph G(D).
Suppose now that and that D
there exists a tuple d
0 such that D j= clique(d; d
By Lemma 3.2 there exists a node w of T such that all components of d [ d 0
are contained in F(w).
induction hypothesis it follows that
O
Let U be the set of nodes on the link between v and w. Then the tuple d
occurs in F(u) for all nodes u 2 U . It follows that T (D) link a
(v; w). Hence
Conversely, if T (D)
(v) then there exists a node w such that the constants
a occur at all nodes on the link between v and w (and hence correspond to
the same tuple d) and such that T (D) clique ab
(w) for some tuple
b. By induction hypothesis this implies that D j= clique(d; d
some tuple d 0 , hence D
Finally, let
and only if d is contained in every xed point of the operator  D , i.e., is in
every relation S such that c)g.
We rst observe that, for guarded tuples d, this is equivalent to the seemingly
weaker condition that d is contained in every S such that c 2 S i D
for all guarded tuples c. Indeed, this is obvious since (S; x) is a Boolean
combination of quantier-free formulae not involving x, of positive atoms of
the form Su where u is a recombination of the variables appearing in x and
of formulae starting with a guarded existential quantier. Therefore the truth
values of Sc for unguarded tuples c never matters for the question whether a
given guarded tuple is in ' D (S).
Recall that the formula associated with '(x) and a is
' a (z) := (8S)
Consider any tuple of monadic relations on T (D) that satisies
the consistency axiom such that
This tuple S denes a relation S on D such that for all nodes w of T and all
tuples c in F(w) with Conversely, each
relation S on D denes such a tuple S of monadic relations on T (D) which
describes the truth values of S on all guarded tuples of D. Since T (D)
induction hypothesis that D
Further d 2 S if and only if v 2 S a .
Hence the formula ' a (v) is true in T (D) if and only if d is contained in all
relations S over D such that for all guarded tuples c, c 2 S i c 2  D (S).
By the remarks above, this is equivalent to saying that d is in the least xed
point of  D .
Theorem 4.3. The satisability problem for CGF is decidable.
Proof. Let be a sentence in CGF of vocabulary  and width k. We translate
into a monadic second-order sentence  such that is satisable if and
only if there exists a countable tree E) with T
Fix a set K of 2k constants and let O be the tuple of monadic relations O a
for a 2 K. Further, for each m-relation symbol R 2  , let R be the tuple
of monadic relation R a where a 2 K m . The desired monadic second-order
sentence has the form
Here  is the rst-order axiom expressing that the tree T expanded by the
relations O and R does describe a tree structure T (D) associated to some
-structure D. We have shown above that this can be done in rst-order logic.
The formula ; (x) is the translation of (and the empty tuple of constants)
into monadic second-order logic, as described by Theorem 4.2.
If is satisable, then by Theorem 3.7, has a countable model D of tree
width k 1. By Theorem 4.2, the associated tree structure T (D) satises
there exists a tree T such that T j=  . Conversely, if
there exists an expansion which satises  and
hence describes the tree decomposition of a -structure D. Since T
it follows by Theorem 4.2 that D j= .
The decidability of CGF now follows by the decidability of S!S, the monadic
second-order theory of countable trees, a famous result that has been established
by Rabin [23].
Note that while this reduction argument to S!S gives a somewhat more elementary
decidability proof (modulo Rabin's result, of course), it does not give
good complexity bounds. Indeed, even the rst-order theory of countable trees
is non-elementary, i.e. its time complexity exceeds every bounded number of
iterations of the exponential function.
4.3 Reduction to the -calculus with backwards modalities
Instead of reducing the satisability problem for CGF to the monadic second-order
theory of trees, we can dene a similar reduction to the -calculus with
backward modalities and then invoke Vardi's decidability result for this logic
[27].
For a set of actions A, the -calculus with backwards modalities L
, permits,
for each action a 2 A, besides the common modal operators hai and [a] also the
backwards operators ha i and [a ] corresponding to the backwards transitions
a := f(w; g. Hence ha i' is true at state w in a Kripke
structure K if and only if there exists a state v, such that K; v
reachable from v via action a.
Here we will need L
on trees (V; E) with only one transition relation. We can
write h+i, [+] for the forward modal operators, and hi, [ ] for the backwards
operators, and then use the abbreviations
Hence 3 and 2 are the usual modal operators on symmetric Kripke structures.
Finally, it is convenient for our reduction argument to permit the use of simultaneous
least and greatest xed points in L
. Let
a sequence of propositional variables, and
a sequence of L
-formulae in which all occurrences of X are posi-
tive. Then, for each i  r, the expressions [X : '(X)] i and [X : '(X)] i are
formulae in L
On every Kripke structure K with universe V , the sequence '(X) denes an
operator ' K that maps any tuple to a new
tuple
r (S)) where ' K
Since the variables in X occur only positive in ', the operator ' K has a least
xed point
r ). Now, the semantics of simulteneous least
xed point formulae is given by
The meaning of a simultaneous greatest xed point
similarly. It is well-known that simultaneous xed points can be rewritten as
nestings of simple xed points, so the use of simultaneous xed points does
not change the expressive power of L
.
Theorem 4.4 (Vardi). Every satisable formula in L
has a tree model.
Further, the satisability problem for L
is decidable and Exptime-complete.
On connected Kripke structures (in particular on trees), the universal modality
is denable in L
. For every formula ', we write 8' to abbreviate the formula
It is easy to see that 8' is satised at some state of a connected
Kripke structure K if and only if ' is satised at all states of K.
Let D be a  structure of bounded tree width, and let T (D) be its tree representation
as described in Sect. 4.1. We view T (D) as a Kripke structure,
with atomic propositions O a and R a . Having available an universal modality,
the axioms for tree representations T (D) given in the previos subsection, can
easily be expressed by modal formulae. For instance, the consistency axioms
can be written
a2a
O a
_
a2a
:O a _ R a
Theorem 4.5. Let D be a structure with tree decomposition hT;
For an appropriate set of constants K and a function f : D ! K, let T (D) be
the associated tree structure. For every formula '(x
every tuple a 2 K m we can construct a formula ' a 2 L
such that, for every
node v of T and every clique-guarded tuple d  F(v) with
Proof. The translation is very similar to the translation into monadic second-order
logic that was given in the previous section.
(1) If '(x) is an atom Sx i 1
then ' a
true if a
(3) For the guard formulae clique(x), let
clique a
_
_ 3(O a ^ O a 0
' a
_
a2a
O a
' a
Here S is a tuple of xed point variables S b and (S) is the tuple of the
(S) for all b 2 K m (where m is the arity of S).
The proof that the translation is correct is analogous to the proof of Theorem
4.2.
We now get another proof for the decidability of guarded xed point logic.
Given a sentence 2 CGF, we translate it into the L
according
to Theorem 4.5 and take the conjunction with the consistency axioms in L
for tree representations T (D). Then use Vardi's decidability result for L
.
By the tree model property of L
, the tree model property of CGF and
Theorem 4.5 this gives a decision procedure for CGF.
However, it is not clear whether this argument can be modied to provide the
optimal complexity bounds for guarded xed point logic.



--R


Modal Correspondence Theory
Dynamic bits and pieces
Modal Logic
The complexity of tree automata and logics of programs
On the (in
A superposition decision procedure for the guarded fragment with equality
The two-variable guarded fragment with transitive relations





Model Theory
Loosely guarded fragment of
Interpolation in guarded fragments.
Beth De
On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
The computational complexity of provability in systems of propositional modal logic
Tolerance logic
Cours de th
First Steps in Modal Logic
Decidability of second-order theories and automata on in nite trees
Tree width and tangles: A new connectivity measure and some applications
Complexity of modal logics
Why is modal logic so robustly decidable?

--TR
First steps in modal logic
Beth Definability for the Guarded Fragment
Reasoning about The Past with Two-Way Automata
On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic
Guarded Fixed Point Logic
The Two-Variable Guarded Fragment with Transitive Relations
A Superposition Decision Procedure for the Guarded Fragment with Equality
Back and Forth between Guarded and Modal Logics

--CTR
Antje Nowack, A Guarded Fragment for Abstract State Machines, Journal of Logic, Language and Information, v.14 n.3, p.345-368, June      2005
Dirk Leinders , Maarten Marx , Jerzy Tyszkiewicz , Jan Bussche, The Semijoin Algebra and the Guarded Fragment, Journal of Logic, Language and Information, v.14 n.3, p.331-343, June      2005
Maarten Marx, Queries determined by views: pack your views, Proceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 11-13, 2007, Beijing, China
Erich Grdel , Wolfgang Thomas , Thomas Wilke, Literature, Automata logics, and infinite games: a guide to current research, Springer-Verlag New York, Inc., New York, NY, 2002
decidability;guarded logics;fixed point logics