Back and forth between guarded and modal logics.
Guarded fixed-point logic GF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal -calculus plays within the modal domain. We provide a semantic characterization of GF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterization of the modal -calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. Guarded second-order logic, the fragment of second-order logic which is introduced in the context of our characterization theorem, captures a natural and robust level of expressiveness with several equivalent characterizations. For a wide range of issues in guarded logics it may take up a role similar to that of monadic second-order in relation to modal logics. At the more general methodological level, the translations between the guarded and modal domains make the intuitive analogy between guarded and modal logics available as a tool in the further analysis of the model theory of guarded logics.
Introduction
Guarded logics generalise certain features and desirable
model theoretic properties of modal logics to a much wider
context. The concept of guarded quantification was introduced
by Andr-eka, van Benthem, and N-emeti [1], who
proposed and analysed the guarded fragment of first-order
logic, GF. This fragment GF provides a very satisfactory basis
for the explanation of quite some of the good behaviour
of modal logics at the level of a rich fragment of classical
first-order logic. Moreover, the robust decidability properties
of modal logics with respect to natural extension mech-
anisms, are also reflected in GF. Most notably, not only is
GF decidable itself [1], but so is its canonical fixed point
extension, -GF, [6]. -GF extends GF so as to render definable
least (and greatest) fixed points of guardedly definable
positive operations in arbitrary arities. In particular it extends
the modal -calculus to the guarded domain. Unlike
its modal companion, however, it no longer shares the finite
model property, though it remains decidable. Another interesting
feature, which again highlights the role of -GF as
a high-level analogue of the -calculus, concerns its potential
for model checking applications. The alternation-free
fragment of -GF admits linear time model checking algorithms
[4]. These and other results of recent research into
guarded logics indicate that GF and its relatives provide a
very interesting domain of logics, combining rich levels of
expressiveness with a very good balance towards algorithmical
issues.
Recall how modal logics, in the broad model theoretic
sense including extensions like CTL and the modal
calculus, are characterised by their invariance under bisim-
ulation: they cannot distinguish between bisimilar struc-
tures. Moreover, invariance under bisimulation is at the root
of many of the successful model theoretic tools available for
modal logics, like e.g. the tree model property which paves
the way towards the use of automata theory. The eminent
role that bisimulation plays in the domain of modal log-
ics, is in the guarded domain taken by a similar but much
more wide-ranging and finer notion of equivalence induced
by guarded bisimulation.
The characteristic feature of modal quantification, which
is also at the heart of bisimulation, is that one can only
directly access nodes along basic edge relations. In the
guarded scenario, this is generalised to simultaneous direct
accessibility of all tuples that are covered (guarded)
by some ground atom. These are what are called guarded
tuples, and guarded quantification is quantification over
guarded tuples. Unlike the modal case, the notion of
guardedness does not impose any arity restrictions, so that
guarded logics are just as meaningful over structures with
higher-arity relations and can address properties of tuples.
One of the underlying technical themes of this paper,
also concerning a methodological point of wider interest,
is the potential of having certain reductions from the richer
scenario of guarded logics to the simpler and well understood
scenario of modal logics, or from guarded bisimulation
to ordinary bisimulation. Corresponding ideas have
been initially explored in [5] in the context of the satisfiability
problem for guarded fixed point logic. This method-
# Mathematische Grundlagen der Informatik, RWTH Aachen, D-52065 Aachen, {graedel,hirsch}@informatik.rwth-aachen.de
Department of Computer Science, University of Wales Swansea, SA2 8PP, United Kingdom, m.otto@swan.ac.uk
ology is carried much further here and applied to a characterisation
issue, concerning the semantic characterisation
of guarded fixed point logic within a suitable second-order
framework. Characterisation theorems of this type have a
strong tradition in the field. They are of particular interest
since they tighten the close connection between logics in a
certain family and characteristic equivalences. At the level
of basic modal logic and the guarded fragment of first-order
logic, the corresponding characterisation theorems are the
see [2] and [1].
Theorem 1.1 (van Benthem). A property of transition systems
is definable in propositional modal logic if and only if
it is first-order definable and invariant under bisimulation.
Theorem 1.2 (Andr- eka, van Benthem, N- emeti). The
guarded fragment GF can define precisely the model
classes that are first-order definable and invariant under
guarded bisimulation.
For the modal scenario, a similar and highly non-trivial
analogous characterisation was given for the associated
fixed point logic in [7].
Theorem 1.3 (Janin, Walukiewicz). A property of transition
systems is definable in the modal -calculus if and only
if it is definable in monadic second-order logic and invariant
under bisimulation.
Johan van Benthem has raised the question whether
-GF admits a similar characterisation, in terms of guarded
bisimulation invariance, within some suitable framework of
second-order logic. It should be noted that MSO is clearly
not the right framework, since monadic second-order quantification
does not suffice to simulate the fixed point definitions
in -GF. Full second-order logic, on the other hand,
is obviously too strong; there are simple examples showing
that even for bisimulation invariant properties, full second-order
logic goes far beyond the expressive power of -GF.
The resulting fragment is, for instance, no longer decid-
able. It turns out, however, that there is a natural analogue
for MSO, which we call guarded second-order logic
GSO. GSO is best characterised in semantic terms, as full
second-order logic with a semantics that restricts second-order
quantifiers to range over sets of guarded tuples, rather
than over arbitrary relations. The precise definition will be
given in section 3, where we also discuss several syntactic
variants which turn out to have exactly the expressive power
of GSO. And indeed we find the following.
Main Theorem. Guarded fixed point logic -GF can define
precisely the model classes that are definable in guarded
second-order logic and are invariant under guarded bisimulation

2. Preliminaries
Transition systems and bisimulation. Transition systems
(or Kripke structures) are structures whose universe is
a set of states (worlds), labelled by unary predicates (atomic
propositions), and carrying binary transition relations labelled
by actions (accessibility relations). We typically
with state set V , based on a set B of atomic propositions
and a set A of actions.
Definition 2.1. A bisimulation between two transition
systems
respecting the P b in the sense that
for all b # B and (v, v # Z, and satisfying the following
back and forth conditions.
for all (v, v # Z, a # A and every w such that
(v, w) # E a , there exists a w # such that (v # , w # E # a and
(w, w # Z.
Back: for all (v, v # Z, a # A and every w # such that
a , there exists a w such that (v, w) # E a and
(w, w # Z.
Two transition systems with distinguished nodes are
bisimilar, K, u # K # , u # , if there is a bisimulation Z between
them with (u, u # Z. We say that two trees are
bisimilar if they are bisimilar at their roots # and # , and
just
Definition 2.2. The unravelling T (K, u) of a transition
system K from node u is the tree of all paths through
K that start at u. More formally, given
(V, the unravelling is
is the
set of all sequences
A such that v
b contains the sequences v 0 a
a contains the pairs (v, vav) in V T - V T .
It is easy to see that each pair (K, u) is bisimilar to its
unravelling: K, u # T (K, u), u. Hence, as far as bisimulation
invariant properties are concerned, we can restrict our
attention to trees.
Bisimilar trees admit special minimal bisimulations,
which may be constructed inductively, level by level starting
from (# ) in such a way that at each new level we add
a tuple (w, w # ) to Z only where this is required by a back
or forth requirement from the previous level. It is clear that
the resulting bisimulation is minimal in the sense that no
proper subset would still be a bisimulation. Note that minimal
bisimulations are in general not unique. They have,
however, the following useful properties.
Lemma 2.3. Let Z be a minimal bisimulation between T
and T # . If (v, v # Z and if u and u # are the parent
nodes of v and v # , respectively, then also (u, u # Z
and (u, v) # E a iff (u # , v # E a . Therefore, a minimal
bisimulation satisfies the back and forth requirements also
with respect to the converses of the E a . The converse forth
property w.r.t. E a , for instance, is the following. For every
(v, v # Z and every u such that (u, v) # E a , there exists
a u # such that (u # , v # E # a and (u, u # Z.
Proof. It is straightforward to show that otherwise Z -
would still be a bisimulation.
It follows that w.r.t. a minimal bisimulation Z between
trees T and T # and for (v, v # Z, any path from v in T
can be lifted to a bisimilar path from v # in T # . In particular
consider for any w in T the unique minimal connecting path
(from v up to the
first common ancestor of v and w, and from there down to
w). Then there is a path (z #
r labelled exactly
the same as the original path, and such that (z i , z
all i.
2.1. Modal logics
We recall the definitions of propositional modal logic
and the -calculus. The formulae of these logics are evaluated
on Kripke structures at a particular state. Given a formula
and a transition system K with state v, we write
to denote that the formula holds in K at state v.
Propositional modal logic. We describe propositional
(multi-)modal logic ML for several transition rela-
tions, i.e., for reasoning about transition systems
(V, may have more
than one element. In the literature on modal logic, this system
is sometimes called Kn (where is the number
of actions or 'modalities').
Syntax of ML. The formulae of ML are defined by the following
rules.
. Each atomic proposition P b is a formula.
. If and # are formulae of ML, then so are ( #),
( #) and - .
. If is a formula of ML and a # A is an action, then
#a# and [a] are formulae of ML.
If there is only one transition relation,
simply writes # and # for [a] and #a#, respectively.
Semantics of ML. Let # be a formula of ML,
(V,
state. In the case of atomic propositions,
Boolean connectives are treated in the
natural way. Finally for the semantics of the modal operators
we put
The -calculus L- . The propositional -calculus L - is
propositional modal logic augmented with least and greatest
fixed points. It subsumes almost all of the commonly
used modal logics, in particular LTL, CTL, CTL # , PDL and
also many logics used in other areas of computer science,
for instance description logics.
Syntax of L- . The -calculus extends propositional modal
logic ML (including propositional variables X,Y, . , also
viewed as monadic second-order variables) by the following
rule for building fixed point formulae.
. If # is a formula in L- , and X is a propositional variable
that does not occur negatively in #, then -X.#
and #X.# are L- formulae.
Semantics of L- . The semantics of the -calculus is given
as follows. A formula #(X) with propositional variable X
defines on every transition system K (with state set V , and
with interpretations for other free second-order variables
that # may have besides X) an operator
P(V ) on the powerset P(V ) of V assigning to every set
the set
As X occurs only positively in # K is monotone for
every K, and therefore has a least and a greatest fixed point.
Now we put
is an element of the least fixed point
of the operator # K . Similarly K, v |= #X.# iff v is an
element of the greatest fixed point of # K .
Remark. By the well known duality between least
and greatest fixed points, #X.# is equivalent to
Hence we could eliminate greatest fixed
points. However, it will be more convenient to keep least
and greatest fixed points and to work with formulae in
negation normal form, where negations are applied only to
atomic propositions.
There is a variant of L - which admits systems of simultaneous
fixed points. These do not increase the expressive
power but sometimes allow for more straightforward
formalisations. Here one associates with any tuple
all positive in the X i , a new formula -X. The semantics
of # is induced by the least fixed point of the monotone
operator # K mapping X to X # where X #
precisely, K, v |= # iff v is an element
of the first component of the least fixed point of the
above operator. Similar conventions apply w.r.t. simultaneous
greatest fixed point. It is well known that simultaneous
fixed points can be uniformly eliminated in favour of indi-
vidual, nested fixed points.
It is easy to see that all formulae of ML and L - are invariant
under bisimulation.
3. Guarded first and second-order logics
Definition 3.1. Let B be a structure with universe B and
vocabulary # .
(i) A set X # B is guarded in B if there exists a ground
atom
is guarded in B if
(b 1 , . , b n
is a guarded list in B if its
components are pairwise distinct and {b 1 , . , b k } is
a guarded set. We admit the empty list # as a guarded
list.
is guarded if it only consists of
guarded tuples.
Note that a singleton set guarded
by the atom b. The cardinality of guarded sets in B
is bounded by the maximal arity of the relations in # , the
width of # . Guarded tuples, however, can have any length.
Guarded lists will be of technical interest later as succinct
tuple representations of guarded subsets.
The guarded fragment GF. The guarded fragment extends
modal logic to a richer fragment of first-order logic. Its
characteristic feature is a relativised pattern of quantifica-
tion, which generalises modal quantification.
Syntax of GF. The formulae of GF (in vocabulary # ) are
defined by the following rules.
are formulae of
GF.
(ii) If # and # are formulae of GF, then so are (#),
(#) and -#.
(iii) If #(x, y), with free variables among those listed, is
a formula of GF and #(x, y) is a #-atom in which all
displayed variables actually occur, then #y #(x, y) #
are formulae of
GF.
The atoms # relativising GF quantifications are called
guards. We shall often also use the more intuitive notation
(#y . # and (#y . # as shorthand for correspondingly
relativised first-order quantification.
Semantics of GF. The semantics of GF is the usual one for
first-order formulae.
As one simple example of a formula in GF, which will
be useful later, consider the formula guarded(x) in variables
#-structures the set of
all guarded k-tuples, cf. Definition 3.1. For any complete
equality type on {1, . , k} specified by a quantifier-free
formula #(x) in the language of just = , let x # be the sub-
tuple of x comprising precisely one variable from each =-
class specified by #. Let #(y, x # ) be a #-atom in which all
variables in x # actually occur, the y new, i.e. disjoint form
x. Put # (x) := #(x) #y#(y, x # ). For the degenerate
case of # 0 , specifying the equality type of a singleton tuple
It is easily
checked that the disjunction over all these formulae # (x)
is as desired.
Note that first-order quantification over an individual single
free variable is always admissible in GF, since singletons
are guarded (by an =-atom):
Guarded fixed point logic -GF. Guarded fixed point logic
-GF as introduced in [6] is the natural extension of GF by
means of least and greatest fixed points (or corresponding
systems of simultaneous fixed points).
Syntax of -GF. Starting from GF, with second-order variables
X,Y, Z, . that are treated like predicates in # but
may not be used in guards, we augment the syntax of GF by
the following rule for least and greatest fixed points.
. If #(X, x) is a formula of -GF, which is positive
in X , X k-ary and
(first-order) variables of # are among these x i , then
-X.# and #X.# are also formulae of -GF.
Semantics of -GF. The semantics of -X.# is the natural
one associated with the least fixed point of the monotone
. More precisely,
is an element of the least fixed
point of the operator # B .
Similarly for #X.# and the greatest fixed point of # B .
One may also admit simultaneous least (and great-
est) fixed points w.r.t. tuples of formulae
the X i have only positive occurrences, and the x i contain
match the arities of the X i .
Then we obtain new
whose semantics is the natural one associated with the first
component X 1 of the least or greatest fixed point of the
corresponding monotone operator. As with the -calculus,
one finds that simultaneous fixed points can be eliminated
in -GF, too.
Guarded second-order logic. We introduce the natural
second-order extension of the guarded fragment, or the
guarded fragment of second-order logic, which relative to
GF and -GF occupies a role analogous to that of MSO relative
to ML and L - . The naturalness of this logic is further
demonstrated below, where we show that the corresponding
level of expressiveness is surprisingly robust under a
number of changes in the actual formalisation and syntax.
Indeed, we shall show that three natural candidates for a
second-order guarded logic all have the same expressive
power. It should be stressed that for all considerations,
guardedness (of sets, tuples, or relations) always refers to
guardedness w.r.t. the underlying vocabulary # ; at no point
will second-order variables be admitted as guards.
In our preferred definition of guarded second-order logic
we simply use the syntax of ordinary second-order logic,
but restrict it semantically by the stipulation that all second-order
quantifiers range just over guarded relations, rather
than over arbitrary relations. We refer to this semantic restriction
as guarded semantics for the second-order quanti-
fiers. It is clear, however, that this stipulation may alternatively
be captured purely syntactically, by only allowing occurrences
of atoms Xx in conjunction with the GF-formula
guarded(x), which says that x is a guarded tuple, thus effectively
restricting X to its guarded part.
Definition 3.2. Guarded second-order logic GSO is
second-order logic with guarded semantics for the second-order
quantifiers.
Note that GSO includes full first-order logic. Hence
GSO is undecidable and, unlike GF and -GF, not invariant
under guarded bisimulation (cf. Definition 4.2). Also
note that, as singletons are always guarded, the monadic
version of guarded second-order logic coincides with full
MSO. Consequently, since MSO is strictly more expressive
than FO, the same is true for GSO. Furthermore, we shall
see in Lemma 3.5 below that GSO collapses to MSO over
words. The robustness of GSO, and its place properly in between
MSO and full second-order SO, is underlined by the
following.
Lemma 3.3. The following fragments of second-order
logic are equally expressive (with respect to sentences):
(1) The extension of GF by full second-order quantification

(2) The extension of GF by second-order quantification
with guarded semantics.
(3) Guarded second-order logic GSO.
Proof. It suffices to argue for translations from (1) and (3)
into (2).
For (1) # (2) consider a second-order variable X in a
formula according to (1), which is meant to range over arbitrary
rather than guarded relations. Any atom Xx occurring
in a GF sentence necessarily is in the scope of a guarded
quantification (Qy . #(y, z))# where the occurrence of x in
Xx is free in #, whence the x all occur in #. It follows that
the truth value of Xx for non-guarded tuples has no impact
on the truth value of #.
For (3) # (2) it suffices to show that unrestricted first-order
quantification can be simulated by guarded (in fact:
monadic) second-order quantification over GF. To this end,
each element variable x is replaced by a set variable X , and
we use the following rules for translating formulae.
Rx #x . Rx) # i
where singleton(X) is a formula stating that X contains exactly
one element:
Note that these translations and in particular
singleton(X) are in GF, since first-order quantification over
a single free first-order variable is always guarded.
The following two lemmas show that GSO lies strictly
between MSO and SO.
Lemma 3.4. GSO is strictly more expressive than MSO.
Proof. We show that the existence of a Hamiltonian cycle in
an undirected graph can be expressed in GSO. It is known,
however, that Hamiltonicity is not expressible in MSO, see
e.g. [3]. Here is a GSO-sentence expressing Hamiltonicity:
(#x#y(Hxy #zHxz #
Lemma 3.5. SO is strictly more expressive than GSO. In
particular GSO collapses to MSO over words.
Proof. We can show that every guarded set over words can
be encoded into a series of monadic predicates. The edge or
successor relation is the predicate of maximal arity occuring
in structures encoding words. Hence any guarded set
contains at most two subsequent nodes.
Due to the directedness of the edges we can simply
choose the element a to represent the guarded set {a, b},
where b is the successor of a.
The encoding uses one monadic predicate for each
second-order predicate and each possibility of forming a tuple
of appropriate arity out of two variables. Hence GSO
is not more expressive than MSO over words, i.e. able to
define exactly the regular languages. On the other hand full
second-order logic is known to capture the polynomial-time
hierarchy.
To summarise, we have the following hierarchy of logics
3.1. A normal form for guarded logics.
We present a normal form for GF and GSO that will
be useful in the following. Let
. } be two disjoint sets of variables. Let
Z stand for either X or Y . GFX and GF Y are defined inductively
as follows.
(1) Every relational atomic formula # with
belongs to GFZ .
(2) A boolean combination of formulae in GFZ also belongs
to GFZ .
be any partial bijection between {1, . , n} and
{1, . , m}. Then, for every guard 1 #(y 1 , . , yn )
and #(y 1 , . , yn
#y. #(i)=j y
is in GFX . By interchanging x- and y-variables we
obtain an analogous rule for GF Y .
It should be noted that the formulae in GFX and GF Y
are syntactically not in GF. It is clear, however, that these
are logically equivalent to guarded ones. Let
These syntactic stipulations extend
from GF to GSO in the obvious way. We let GSO 0 be
the extension of GF 0 by second-order quantification over
guarded relations.
In the sequel, relativised quantifications of the type
(#y. #(i)=j y as used in
GF 0 will be abbreviated as (#= y . #(x, y) #(y)).
Proposition 3.6. Every sentence in GF is equivalent to a
sentence in GF 0 .
Corollary 3.7. Every sentence in GSO is equivalent to a
sentence in GSO 0 .
The proof is not difficult but a bit technical. We
just explain the idea. First, it is well known, that
first-order sentences can be reformulated so that in all
subformulae distinct variables are always to be interpreted
by distinct elements. One way to make this precise
is to use the quantifier #= rather than # where
means that there exists an x that is
distinct from z 1 , . , z n such that #(x, z 1 , . , z n ) holds.
Obviously, this does not change the expressive power of
first-order sentences, since #x #(x, z 1 , . , z n ) is equivalent
to # n
combine this with the idea that any quantification over a
part of the free variables in a formula should come with
a complete renaming of all variables, so that we move,
say, from x-variables to y-variables. Consider a formula
of the form We then replace this
by the equivalent formula (#= y 1 - y 4 . y
(Here the notation #= y means that the
quantified y-variables must assume distinct values, but the
values of a y-variable can be the same as for an x-variable.)
To see why this might be useful (beyond the applications
in this paper actually) let us consider another simple exam-
ple. In the evaluation game for the sentence
the verifier first has to pick distinct elements a 1 , . , a 4 and
is then challenged by the falsifier to justify one of the three
conjuncts. Suppose that she has to justify the subformula
This means that she has to keep a 2
and extend it by some new a 1 and a 5 so that she can win the
evaluation game for #(a 1 , a 5 , a 2 ) holds. Similarly, if she is
challenged to verify the third conjunct she has to produce
a new a 3 so that she wins the game for #(a 3 , a 4 , a 3 ). This
becomes more transparent if we reformulate in GF 0 as
Indeed this formulation makes it apparent that the verifier
moves from a tuple to a new tuple (y 1 , y 2 , y 3
or (y 1 , y 2 ) subject to explicitly given equality constraints.
4. Guarded bisimulation and tree representation

Guarded bisimulation is for GF what bisimulation is for
ML.
Definition 4.1. A guarded bisimulation between two # -
structures A and B is a non-empty set I of finite partial
from A to B, where X # A and
are guarded sets, such that the following back and
forth conditions are satisfied. For every
We require that all y i occur in #, however order and multiplicity is arbitrary!
for every guarded set X # A there exists a partial
in I such that f and g agree on
Back: for every guarded set Y # B there exists a partial
in I such that f -1 and g -1
agree on Y # Y # .
Two #-structures A and B are guarded bisimilar (in sym-
bols: A # g B) if there exists a guarded bisimulation between
them. We refer to the relation # g , which obviously
is an equivalence relation between structures, as guarded
bisimulation equivalence.
Definition 4.2. We say that a sentence # is invariant under
guarded bisimulation if it does not distinguish between
guarded bisimilar structures, i.e. if A # g B and A |= #
then also B |= #. A logic L is invariant under guarded
bisimulation if all its sentences are.
Proposition 4.3. GF and -GF are invariant under
guarded bisimulation.
The guarded Ehrenfeucht-Fra-ss- e game. It is well understood
how guarded bisimulation equivalence may be
described by means of an associated Ehrenfeucht-Fra-ss-e
game. We indicate the characteristic features of the guarded
game, in a version directly relating to our GF 0 normal form.
Two players, player I and player II, take turns to place and
relocate two groups of corresponding, labelled pebbles on
elements of the underlying structures A and B, respectively.
The rules of the game are such that after each round the
groups of pebbles positioned in A and B, respectively, label
guarded lists a and b in such a way that the correspondence
a # b is a partial isomorphism. In each round, player I
has the choice in which of the two structures to play. In
the chosen structure, player I then may leave some pebbles
fixed, remove some from the board, and re-locate some oth-
ers. The only restriction is that the new pebble positions
again have to label a guarded list. Player II then has to re-position
the corresponding pebbles in the other structure so
as to produce a locally isomorphic configuration. Player II
loses if no such response is available. Now A and B are
guarded bisimilar iff player II can always respond indefi-
nitely, i.e. iff there is a winning strategy for player II in the
infinite guarded game. It is apparent that a guarded bisimulation
in the sense of Definition 4.1 is a formalisation of a
(non-deterministic) strategy for player II.
We now use the intuition behind the game to introduce
the following structural transformations. One which abstracts
from a given #-structure B a tree representation
T (B), which fully describes as a transition system the behaviour
of B in the guarded game, and thus characterises
B up to guarded bisimulation equivalence. Another one
which, conversely, associates with a tree T a #-structure
D(T ), such that the game behaviour specified by T is realised
in the guarded game on D(T ).
The guiding idea behind these transformations is that
guarded bisimulations at the level of the #-structures lift to
ordinary bisimulations at the level of the abstracted transition
systems. In particular, B # := D(T (B)) # g B will
be a tree-like variant of B, intuitively corresponding to a
guarded unravelling of B, as considered e.g. in [1] and [5].
From structures to trees. Recall from Definition 3.1 that a
guarded list in B is a tuple (b 1 , . , b k ) of distinct elements
such that {b 1 , . , b k } is a guarded set. We regard such
guarded lists as descriptions of positions over B in the restricted
guarded game. The nodes of the induced tree are associated
with guarded lists over B, and we symmetrise the
description of the game so as to allow re-labellings (permu-
tations) of the guarded list in conjunction with every move
in the game. The information to be recorded in each node
precisely the isomorphism type of the
induced substructure on {b 1 , . , b k } in B. The information
to be recorded concerning possible moves describes the
constraints imposed on a move from l ) to
some choice of elements that remain
fixed (according to player I's choice).
For a #-structure B we work with the following vocabulary
- # for the associated tree. If m is the width (maximal
arity of predicates) of # , let S be the set of all #-structures A
with universe {1, . , k}, admitted
F be the set of all pairs (k, #), where
is a partial bijection from {1, . , k}
to {1, . , m}. Then -
# has monadic predicates PA for
all A # S, and binary predicates E k
# for all (k, # F .
Let G be the set of all guarded lists over B. Define V as
the set of all sequences
all
have | and for all j # dom(#) the j-th element
at g i+1 is the same as the #(j)-th element at g i . A
node . gn of T (B) is naturally associated with
the guarded list in B, in which the sequence
terminates. In particular we set |v| := |g n
and let A v be the unique A # S that is isomorphic with
. Then the tree associated with
B is
# .
The following is a direct consequence of the fact that the
transition system T (B) is precisely set up to capture the
behaviour of B w.r.t. the guarded game.
Lemma 4.4. For all #-structures B and
From trees to structures. Conversely, we would like to
associate with a tree T of type - # a #-structure D for which
. This is clearly not possible for arbitrary T .
Definition 4.5. Let T be any -tree. We call T consistent
if the following are satisfied.
(a) For each node v there is a unique A # S such that
T |= PA (v), denoted A v . A #.
(b) If (u, v)
# then the partial bijection # is an isomorphism
between A v # dom(#) and A u # im(#), and for
each A v from some structure
A # S to A v there exists a node w such that
and (u, w)
# .
Lemma 4.6. Within the class of -trees, the class of consistent
trees is bisimulation invariant and first-order definable.
Every tree T (B) is consistent. Conversely, if
consistent -tree, then we
may define an associated #-structure D(T ) as follows. Let
# be the reflexive and
symmetric transitive closure of the following relation on U :
(v,
The universe of D(T ) is D := U/# , the set of #-
equivalence classes [v, i] in U . We say that an equivalence
class lives at node u if [v,
We observe that if an equivalence class d lives at nodes u
and v in T then it must also live at every node of the unique
shortest path connecting u to v in T . It follows from consistency
condition (b), that we may consistently interpret every
k-ary predicate in # over D(T ) by putting
Note that guarded list in D(T ) if
and only if
of size |w| = k. We say that v represents the guarded list d.
Lemma 4.7. For all #-structures B: D(T (B)) # g B.
Proof. Let
that T is the unravelling of K, whence any node v of T may
be associated with a unique node v 0 in K (the last node in
the unravelled path that gives rise to v). Further recall that
being a node in K, is a guarded list in B.
For any guarded list d in D and any node v of T representing
this guarded list, let f d,v
be the bijection which
maps d to the guarded list v 0 in B. Note that as a map f d,v
only depends on the guarded set {d 1 , . , d k } and not on
the order of components or on the chosen representative v.
If v and v # represent the same guarded set, they are linked
in T by a path along which all components always live to-
gether. The corresponding path in K similarly links v 0 to
matching permutations along that path.
We claim that the set of all these f d,v
is a guarded bisimulation
between D and B. It is obvious from the construction
that the f d,v
are partial isomorphisms whose domains
are guarded sets. The forth property is immediate from the
construction. We indicate the argument for the back prop-
erty. Let d and d # be guarded lists in D, f d,v : d # v 0 . Let
c be the tuple of common components in d and d # . Let v # be
any representative of the guarded list d # . The tuple c lives
along the unique shortest path from v to v # in T . Projecting
this path down to K we see that f d # ,v # and f d,v agree on
their common domain.
may be regarded as a guarded
unravelling of B, analogous to the standard unravelling of
transition systems. Indeed, the resulting guarded bisimilar
structure B # is also tree-like in that it has a tree decomposition
of width m- 1, where m is the width of # . The naked
tree T (B), stripped of its labels and regarded as a directed
graph, together with the natural association of a node v of
with the guarded set it represents in B # , induces a
tree decomposition of B # in the usual sense. Tree unrav-
ellings, and the corresponding generalised tree model property
for GF and some of its relatives have been put to use
e.g. in [1] and [5].
The following proposition extends the intuition that the
bisimulation type of T (B) captures the guarded bisimulation
type of B to the setting of all consistent trees. The
proof is via a canonical lift of tree bisimulations.
Proposition 4.8. For any consistent -
-trees T and
Proof. Let Z # V -V # be a minimal bisimulation between
T and T # , cf. Lemma 2.3.
For each pair (v, v # Z let f vv # be the function that
maps the guarded list represented by v to that represented by
v # . Clearly, f vv # is a partial isomorphism, since A
For
# and
# , the
maps f uu # and f vv # agree on their common domain. This
follows from the construction of D(T ) and D(T # ), because
elements represented at u and v are identified in D(T ) via
# in exactly the same way as the corresponding elements at
are identified in D(T # ).
We claim that the set of all f vv # , for (v, v # Z, is a
guarded bisimulation between D(T ) and D(T # ).
To verify, for instance, the forth condition, let c and d be
guarded lists in D(T ), represented by u and v in T , respec-
tively. Let (u, u # Z, f We need to find
such that (v, v # Z and such that f vv # agrees with
f uu # on their common domain. Let X be the set of common
elements in c and d. Consider the unique shortest path from
u to v in T . As Z is minimal, this path gives rise to a bisimilar
path from u # to some v # in T . Now f vv # is as desired:
the elements of X live at all nodes on the path from u to v,
whence all the intermediate mappings fww # along the path,
and in particular f vv # respect f uu #X .
5. Back and forth
Recall the characterisation of the modal -calculus from
Theorem 1.3. We want to apply this characterisation in restriction
to trees, and therefore refer to the following vari-
ant, which is proved en route to Theorem 1.3 in [7].
Theorem 5.1 (Janin, Walukiewicz). A class of trees is definable
in the modal -calculus if and only if it is definable
in monadic second-order logic and closed under bisimulation
within the class of all trees.
Towards a reduction of our main theorem to Theorem
5.1, we define a "forth" translation that maps every
sentence # GSO[# ] to a formula # (x) # MSO[-# ] with
translation that maps every
to a sentence # -GF[# ]. These
translation will be such that
(1) If T is a consistent tree with root #, then T |=
#) iff D(T ) |= #.
(2) If B is a #-structure and # is the root of T (B), then
It follows from (1) and Proposition 4.8 that GSO sentences
that are invariant under guarded bisimulation are
mapped to MSO formulae that are bisimulation invariant on
consistent trees.
Before giving the formal definitions, we informally discuss
the main problems arising from the differences between
the guarded and the modal viewpoint.
We wish to translate GSO sentences to MSO formulae
and L- formulae back to -GF sentences. We want a modal
formula to hold at some node v if and only if the corresponding
guarded formula holds of the guarded list represented
by v. For second-order variables we need to map
sets of guarded tuples to sets of nodes and vice versa. For
each node v of a consistent tree T , the associated structure
A v has in general many different guarded tuples that
can occur in any single guarded set. Therefore a second-order
variable Z in a GSO sentence will be translated into
a sequence Z # of set variables Z i 1 ,.,i r , one for each (lo-
cal) choice of elements. In the other direction we have to
deal with monadic second-order variables, which in general
range over sets of nodes of arbitrary size. Consequently
a monadic second-order variable X is translated into a sequence
that each X i ranges over guarded tuples of length i.
5.1. From guarded to monadic second-order logic.
Without loss of generality we restrict attention to GSO
sentences in GSO 0 , cf. Proposition 3.7. Let m be the width
of # , i.e. the maximal arity of relations in # .
Definition 5.2. Let T be a consistent -tree, and let D(T )
be the associated #-structure. If Z is an r-ary second-order
variable, then Z # := (Z
is the
corresponding sequence of monadic predicates. A tuple
J # of monadic predicates J
on T encodes an r-ary
guarded relation J on D(T ) iff J
Not all sequences J of monadic predicates over T do indeed
encode a guarded relation over D(T ). To do so, they
have to satisfy the following correctness conditions.
(a)
only contains nodes v where all i j are in A v .
(b) J is consistent on tuples living at different nodes,
i.e. if in D(T ) a tuple (d 1 , . , d r ) is represented by
(i 1 , . , i r ) at node u and by (j 1 , . , j r ) at node v,
then
Lemma 5.3. For each r # m there exists a first-order
that expresses the correctness conditions

These conditions are necessary and sufficient in the
sense that a tuple J encodes a guarded relation on D(T ),
if and only if T |= correct(J).
Proof. Note that it suffices to express condition (b) for adjacent
nodes to enforce it globally. Thus the consistency requirement
for Z # can be expressed by a first order formula
states condition (a) in an obvious way and con-
tains, for each pair (k, # F and each tuple (i 1 , . , i r ) a
clause
The proof of the adequacy claim is straightforward.
First-order quantifiers also require a special treatment.
Let us first consider the case where T is a tree representation
(B). By construction such trees satisfy a strong
homogeneity condition, namely for all nodes u, u # and all
successors v of u there is a successor v # of u # such that
the subtrees with roots v and v # are isomorphic. To put
it differently, an indistinguishable copy of any guarded list
anywhere in D(T ) is available locally, at some child of the
current node. Therefore guarded first-order quantifications
over D(T ) can be simulated over T by moving to an immediate
successor of the current node (i.e. by a modal quantifier
# or #). However, if T is an arbitrary consistent -
# -tree,
this is no longer the case. To verify a formula of the form
(#= y . #(x, y) #(y))#(y) we want to move from the current
tuple x to a new tuple y, guarded by #, such that #(y)
is true and the overlap conditions for x and y as stated by
#(x, y) are satisfied. In arbitrary consistent trees, such a witness
need not exist locally, but may only occur as a remote
node, which is linked to the current node by a path along
which the common components according to # are kept.
To capture this situation in MSO we use a sequence W
of monadic predicates W k
# , one for each (k, # F , that
partition the set of nodes according to their size and their
overlap with the current node. The proof of the following is
then straightforward.
Lemma 5.4. There is a first-order formula F-part(z, W )
expressing the following correctness conditions on partitions
with respect to node z. For every consistent tree T ,
every sequence
predicates on T , we have T |= F-part(u, W ) iff W k
|Aw
Proof. As in the previous lemma, it suffices to express the
required condition at the current node and for every edge.
The formula F-part(z, W ) states that
(a) The sets W form a partition of the universe.
(b) The node z itself belongs to W k
id , where
(c) If y # W k
(d) For all (k, #) and
then x # W #
# .
By induction on the distance from z one easily shows
that F-part(z, W ) expresses the right property.
The translation. Recall that formulae in GSO 0 either
belong to GSOX and have all their free first-order variables
in X , or they belong to GSO Y and have all their
are two disjoint
sets of variables. Further, formulae in GSOX that start
with a quantifier are of the form #(x) := (#= y . #(x, y) #
#(y))#(y) with #(y), #(y) # GSO Y .
We inductively translate every GSOX [#
into an MSO[-#
r ), with a single free first-order variable
x and sequences of monadic second-order variables
i that correspond to the second-order variables Z i . Sim-
ilarly, formulae in GSO Y are translated into formulae #
y. We just present the translation
for formulae in GSOX :
r-ary relation variable
(x).
(#W . F-part(x, W ))(#y . W |y|
(5) For #Z# with r-ary relation variable Z, let
Theorem 5.5. Let T be a consistent -tree with root #, let
D(T ) be the associated #-structure, and let # be a sentence
in GSO[# ]. Then D(T
Proof. This theorem is a consequence of the following
more general statement. Consider any formula
second-order variables as displayed. Its translation into
MSO[-#
guarded list in D(T ), and let v be a node of T such that
be sets of guarded
tuples in D(T ), and let J #
s be their representations
according to Definition 5.2.
Note that for sentences (i.e.
the claim implies the theorem. The claim itself is established
inductively. The cases corresponding to (1) - (3)
are immediate.
(#W . F-part(x, W ))(#y . W |y|
As second-order variables play no role for this case, we
suppress them. Suppose that D(T ) |= #(d). Then there
exists a guarded list
that D(T ) |= #(e) #(e) and e
e is guarded, there exists a node w such that all e i live together
at w. Actually, due to the last of the conditions for
consistent trees, we can assume that
and |Aw | = #. We know that there exists a W satisfying
that for all (i,
[v, j]. It follows that T |= W #
# (w) and, by induction hy-
pothesis, T |= (# (w). Therefore T |= # (v).
Conversely, suppose that T |= # (v). Hence for the
(unique) tuple W satisfying F-part(v, W ), there exists a
node w # W #
# such that T |= (# (w). For e i := [w, i]
we find that e and, by induction hy-
pothesis, D(T ) |= (#)(e). Therefore D(T ) |= #(d).
For (5), the claim is immediate from the induction hypothesis
and from Lemma 5.3.
Corollary 5.6. If # GSO[# ] is a sentence that is invariant
under guarded bisimulation, then # (x) is bisimulation
invariant on consistent -trees.
Proof. Let T , T # be two bisimilar, consistent -trees. Then
Proposition 4.8. It follows that T |=
5.2. From the -calculus to guarded fixed point
logic.
The translation back from the modal into the guarded
world again requires some preliminary discussion. Every
formula # of the -calculus, evaluated on a tree
defines the set # T of all nodes v such that T , v |= #. Recall
how each node v of T represents a guarded list g v in
B. So the idea is to translate # into a guarded formula #(x)
defining in B the set #
should be equal to {g v #}. The main problem
is that guarded lists do not have a fixed length, so that
must actually be translated into a tuple
Definition 5.7. Let X be a monadic second-order variable.
is an i-
ary second-order variable. Let N be a set of nodes in
a tree T (B). The representation of N in B is N :=
Note that, since the root # is the only node of size 0, either
we say that
or N
In the sequel we assume w.l.o.g. that L - formulae are
written without #-operators, that in any formula -X.# the
fixed point variable X occurs in # only inside the scope of
modal operators, and even that in each # L - , the fixed
point formulae -X.#(X) themselves only occur inside the
scope of modal operators, cf. [8].
The translation. For every formula # L -# ] we now
define
one for each
m, in which each monadic second-order variable X of
# is represented by a tuple of second-order variables X #
(of arities 0, 1, . , m).
:= false if |A| #= k, and
be the conjuction over
all atomic and negated atomic #-formulae # such that
that for
is the following simultaneous
least fixed point, which can be simulated
by nested individual fixed points in the standard way:
Theorem 5.8. Let B be a #-structure, let # be the root of
# be a formula in L -#
T (B), #.
Proof. Again we prove a more general statement involving
variables. W.l.o.g., consider the case of just one
monadic second-order variable Y . Let #(Y ) be a formula
in L-# ], N a set of nodes in
Claim. is the representation
of #(N) T in B.
The claim is proved inductively. The cases corresponding
to (1) - (3) are trivial.
Consider (4) and let #. Suppose that T , v |=
#. Then there is a node w such that (v, w) # E #
# and
for all (i, and, by induction hypothesis, B |=
Conversely, suppose that B |= # k (b 1 , . , b k ). This
means that there exists a guarded list
By the construction of T (B), there exists a node w such
that (v, w) # E #
# and The induction hypothesis
implies that T , w |= #. It follows that T , v |= #.
For (5) finally let Consider the stages
of the fixed point induction on # 0 := false , #+1 :=
# for limit ordinals #. Let
similarly, for the simultaneous fixed point induction on
wise) in limits.
By induction hypothesis, if M # is the representation of
M in B, then the
representation of #(M) T . By induction on # (together
with the representation of the
set defined by # in T . Hence the same is true for the least
fixed points.
We are now in a position to prove our main theorem.
Theorem 5.9. Every sentence in GSO that is invariant under
guarded bisimulation is equivalent to a sentence in
-GF.
Proof. Let # GSO[# ] be invariant under guarded bisimulation
and let # (z) be its translation into MSO[-# ]. By
Lemma 5.6 # (z) is bisimulation-invariant on consistent
trees. Recall that the consistency condition for trees can be
formulated by a monadic second-order sentence #, which is
bisimulation invariant with respect to all trees. As a conse-
quence, the formula (# )(x) is bisimulation invariant
on arbitrary trees. By the Janin-Walukiewicz Theorem,
Theorem 5.1 above, there exists an equivalent formula #
in the -calculus. Let # 0 be its translation into -GF[# ].
Putting everything together, we have
The first equivalence uses guarded bisimulation invariance
of # and Lemma 4.7; the second one is an application
of Theorem 5.5; the third equivalence reflects the input from
the Janin Walukiewicz Theorem; the fourth is an application
of Theorem 5.8.



--R

Modal languages and bounded fragments of predicate logic.
Modal Logic and Classical Logic.
Finite Model Theory.
lite.
The decidability of guarded fixed point logic.
Guarded fixed point logic.
On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
Games for the mu-calculus
--TR
Automata on infinite objects
Games for the MYAMPERSANDmgr;-calculus
Reasoning in description logics
Why are modal logics so robustly decidable?
Dynamic Logic
Modal Logic over Finite Structures
Games and Model Checking for Guarded Logics
Modal and Guarded Characterisation Theorems over Finite Transition Systems
On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic
The monadic second-order logic of graphs XIV
Guarded Fixed Point Logic
Back and Forth between Guarded and Modal Logics

--CTR
Dirk Leinders , Jan Van den Bussche, On the complexity of division and set joins in the relational algebra, Journal of Computer and System Sciences, v.73 n.4, p.538-549, June, 2007
Dirk Leinders , Jan Van den Bussche, On the complexity of division and set joins in the relational algebra, Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 13-15, 2005, Baltimore, Maryland
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
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
modal logic;bisimulation;model theory;guarded logic