The decidability of guarded fixed point logic

Erich Grädel

Abstract

Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of first-order logic that were recently introduced by Andréka, van Benthem and Németi. Guarded fixed point logics can also be viewed as the natural common extensions of the modal μ-calculus and the guarded fragments. In a joint paper with Igor Walukiewicz, we proved recently that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. We present here an elementary proof for the decidability of guarded fixed point logics which is based on guarded bisimulations, a tree model property for guarded logics and an interpretation into the monadic second-order theory of countable trees.

Contents

1 Introduction 2

2 Guarded fixed point logics 4

3 The tree model property 7

4 Reduction to the monadic theory of trees 10

5 Variations 13

1 Introduction

Modal logics are widely used in a number of areas in computer science, in particular for the specification and verification of hardware and software systems, for knowledge representation, in databases, and in artificial intelligence. The most important reason for the successful applications of these logics is that they provide a good balance between expressive power and computational complexity. A great number of logical formalisms have been successfully tailored in such a way that they are powerful enough to express interesting properties for a specific application but still admit reasonably efficient algorithms for their central computational problems, in particular for model checking and for satisfiability or validity tests. Many of these formalisms are essentially modal logics although this is not always apparent from their ‘official’ definitions (as for instance in the case of description logics).

The basic propositional (poly)modal logic ML (for a given set A of ‘actions’ or ‘modalities’) extends propositional logic by the possibility to construct formulae ⟨a⟩ψ and [a]ψ (where a ∈ A) with the meaning that ψ holds at some, respectively each, a-successor of the current state. Although ML is too weak for most of the really interesting applications, it can be extended by features like path quantification, transitive closure operators, counting quantifiers, least and greatest fixed points, and it has turned out that most of these extensions are still decidable and indeed of considerable practical importance.

Up to now, the reasons for these good algorithmic properties of modal logics have not been sufficiently understood. In [15] Vardi explicitly asked the question: “Why is modal logic so robustly decidable?”.

To discuss this question, it is useful to consider propositional modal logic as a fragment of first-order logic. Kripke structures which provide the semantics for modal logics, are relational structures with only unary and binary relations. Every formula ψ ∈ ML can be translated into a first-order formula ψ^{∗}(x) with one free variable, which is equivalent in the sense 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 P x, it commutes with the Boolean connectives, and it translates the modal operators by quantifiers as follows:

⟨a⟩ψ ⇝ (⟨a⟩ψ)^{∗}(x) := ∃y(E_{a}xy ∧ ψ^{∗}(y))
[a]ψ ⇝ ([a]ψ)^{∗}(x) := ∀y(E_{a}xy → ψ^{∗}(y)),

where ψ^{∗}(y) is obtained from ψ^{∗}(x) by replacing all occurrences of x by y and vice versa and where E_{a} is the transition relation associated with the modality a.

The modal fragment of first-order logic is the image of propositional modal logic under this translation. It is properly contained in FO^{2}, relational firstorder logic with only two variables. But although FO^{2} is decidable and has the finite model property (see [12, 6]), it lacks the nice model-theoretic properties [1, 9] and, in particular, the robust decidability properties of modal logics. Indeed while the extensions of modal logic by path quantification, transitive closure operators, least fixed points etc. are still decidable, most of the corresponding extensions of FO^{2} are highly undecidable (see [7, 8]). In particular this is the case for fixed-point logic with two variables, which is the natural common extension of FO^{2} and the μ-calculus. The embedding of ML in FO^{2} therefore does not give a satisfactory answer to Vardi’s question.

An important property that is shared by modal logic and its extensions, but not by FO^{2}, and whose importance for the decidability of modal logics has been pointed out by Vardi [15] is the tree model property: Every satisfiable sentence has a model that is a tree of bounded branching. The tree model property is the basis for the use of automata theoretic techniques to decide the satisfiability problems for modal logics.

An alternative explanation for the good properties of modal logics has been proposed by Andréka, van Benthem and Németi [1]. Starting from the observation that in the translation of modal formulae into first-order formulae, the quantifiers are used only in a very restricted way, they defined the guarded fragment of first-order logic. They dropped the restriction to use only two variables and only monadic and binary predicates, but imposed that all quantifiers must be relativized by atomic formulae. This means that quantifiers appear only in the form

∃y(α(x, y) ∧ ψ(x, y))  or  ∀y(α(x, y) → ψ(x, y)).

Thus quantifiers may range over a tuple y of variables, but are ‘guarded’ by an atom α that contains all the free variables of ψ.

The guarded fragment GF extends the modal fragment and turns out to have interesting properties [1, 5]: (1) The satisfiability problem for GF is decidable; (2) GF has the finite model property, i.e., every satisfiable formula in the guarded fragment has a finite model; (3) GF has (a generalized variant of) the tree model property; (4) Many important model theoretic properties which hold for first-order logic and modal logic, but not, say, for the boundedvariable fragments FO^{k}, do hold also for the guarded fragment; (5) The notion of equivalence under guarded formulae can be characterized by a straightforward generalization of bisimulation.

In a further paper, van Benthem [2] generalized the guarded fragment to the loosely guarded fragment (LGF) where quantifiers are guarded by conjunctions of atomic formulae of certain forms (details will be given in the next section.) Most of the properties of GF generalize to LGF. In [5] it is shown that the the satisfiability problems for GF and LGF are complete for 2Exptime, the class of problems solvable by a deterministic algorithm in time 2^{2^{p(n)}}, for some polynomial p(n).

Probably the most important extension of ML is the μ-calculus, introduced in [11], which extends propositional modal logic by least and greatest fixed points and subsumes most of the other program logics such as PDL, CTL and CTL^{∗} and also many description logics. It is known that the satisfiability problem for the μ-calculus is decidable and Exptime-complete [3]. Recently, Vardi has shown that also a stronger variant of the μ-calculus that includes backward modalities remains decidable in exponential time [16].

If it is indeed the case that, as suggested by Andréka, van Benthem and Németi, the guarded nature of quantification in modal logics is the main reason also for their good algorithmic properties, then we are naturally lead to the following question:

If we extend the guarded fragments of first-order logic by least and greatest fixed points, do we still get a decidable logic?

In [10] we were able to give a positive answer to this question. We denote by μGF and μLGF the extensions of GF and LGF by least and greatest fixed points (precise definitions will be given in the next section). The model-theoretic and algorithmic methods that are available for the μ-calculus on one side, and the guarded fragments of first-order logic on the other side, can indeed be combined and generalized to provide positive results for the guarded fixed point logics. Using automata theoretic methods and a forgetful determinacy theorem for graph games we could in fact establish precise complexity bounds.

Theorem 1.1 (Grädel, Walukiewicz). The satisfiability problems for μGF and μLGF are decidable and 2Exptime-complete.

Hence, the guarded nature of quantification does indeed seem to provide a convincing explanation for the good algorithmic and model theoretic properties of modal logics.

In this paper, a somewhat simpler decidability proof for guarded fixed point logic is presented which replaces the automata theoretic machinery used in [10] by an interpretation argument into the monadic second-order theory of countable trees which by Rabin’s famous result [13] is known to be decidable. However, note that while this gives a more elementary decidability proof, it does not give good complexity bounds. Indeed, even the first-order theory of countable trees is non-elementary, i.e. its time complexity exceeds every bounded number of iterations of the exponential function.

Here is the plan of this paper. In Sect. 2 we present the definitions and some basic properties of the guarded fragments of first-order logic, GF and LGF, and of the guarded fixed point logics μGF and μLGF. In Sect. 3 we explain the notions of a guarded bisimulation and of the unraveling of a structure and show that guarded fixed point logic satisfies a variant of the tree model property. Finally, in Sect. 4 we reduce the satisfiability problem for μLGF to the monadic second-order theory of countable trees and prove its decidability.

2 Guarded fixed point logics

Definition 2.1. The guarded fragment GF of first-order logic is defined inductively as follows:

(1) Every relational atomic formula belongs to GF.

(2) GF is closed under propositional connectives ¬, ∧, ∨, → and ↔.

(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(ψ) ⊆ free(α) = x ∪ y, then the formulae

∃y(α(x, y) ∧ ψ(x, y))
∀y(α(x, y) → ψ(x, y))

belong to GF.

Here free(ψ) means the set of free variables of ψ. An atom α(x, y) that relativizes a quantifier as in rule (3) is the guard of the quantifier. Notice that the guard must contain all the free variables of the formula in the scope of the quantifier.

While the guarded fragment clearly contains the modal fragment of firstorder logic, it seems not to be able to express all of temporal logic over (ℕ, <). Indeed, the straightforward translation of (ψ until φ) into first-order logic

∃y(x ≤ y ∧ φ(y) ∧ ∀z((x ≤ z ∧ z < y) → ψ(z))

is not guarded in the sense of Definition 2.1. However, the quantifier ∀z in this formula is guarded in a weaker sense, which lead van Benthem [2] to the following generalization of GF.

Definition 2.2. The loosely guarded fragment LGF is defined in the same way as GF, but the quantifier-rule is relaxed as follows:

(3)′ If ψ(x, y) is in LGF, and α(x, y) = α_{1} ∧⋯∧α_{m} is a conjunction of atoms, then

∃y((α_{1} ∧ ⋯ ∧ α_{m}) ∧ ψ(x, y))
∀y((α_{1} ∧ ⋯ ∧ α_{m}) → ψ(x, y))

belong to LGF, provided that free(ψ) ⊆ free(α) = x ∪ y and for every quantified variable y ∈ y and every variable z ∈ {x, y} there is at least one atom α_{j} that contains both y and z.

In the translation of (ψ until φ) described above, the quantifier ∀z 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 ∀xyz(Exy∧Eyz → Exz) is not in LGF. The conjunction Exy ∧ Eyz is not a proper guard of ∀xyz since x and z do not coexist in any conjunct. Indeed, it has been shown in [5] that there is no way to express transitivity in LGF.

Notation. We will use the notation (∃y . α) and (∀y . α) for relativized quantifiers, i.e., we write guarded formulae in the form

(∃y . α)ψ(x, y) and (∀y . α)ψ(x, y).

When this notation is used, then it is always understood that α is indeed a proper guard as specified by condition (3) or (3)′.

Definition 2.3. The guarded fixed point logics μGF and μLGF are obtained by adding to GF and LGF, respectively, the following rules for constructing fixed-point formulae:

Let W be a k-ary relation symbol, x = x_{1}, …, x_{k} a k-tuple of distinct variables and ψ(W, x) be a guarded formula that contains only positive occurrences of W, no free variables other than x_{1}, …, x_{k} and where W is not used in guards. Then we can build the formulae

[LFP W x . ψ](x)  and  [GFP W x . ψ](x).

The semantics of the fixed point formulae is the usual one: Given a structure 𝔄 providing interpretations for all free second-order variables in ψ, except W, the formula ψ(W, x) defines an operator on k-ary relations W ⊆ A^{k}, namely

ψ^{𝔄} : W ↦ ψ^{𝔄}(W) := {a ∈ A^{k} : 𝔄 ⊧ ψ(W, a)}.

Since W occurs only positively in ψ, this operator is monotone (i.e., W ⊆ W′ implies ψ^{𝔄}(W) ⊆ ψ^{𝔄}(W′)) and therefore has a least fixed point LFP(ψ^{𝔄}) and a greatest fixed point GFP(ψ^{𝔄}). Now, the semantics of least fixed point formulae is defined by

𝔄 ⊧ [LFP W x . ψ(W, x)](a) iff a ∈ LFP(ψ^{𝔄})

and similarly for the greatest fixed points.

The Löwenheim-Skolem property. For future use, we recall that even the (unguarded) least fixed point logic (FO + LFP), and hence also its fragments μGF and μLGF, have the Löwenheim-Skolem property. This result is part of the folklore on fixed point logic, but it is hard to find a published proof. Our exposition follows the one in [4].

Theorem 2.4. Every satisfiable sentence in (FO + LFP) has a model of countable cardinality.

Proof. Consider a fixed-point formula of form ψ(x) := [LFP Rx . φ(R, x)](x), with first-order φ such that 𝔄 ⊧ ψ(a) for some infinite model 𝔄.

For any ordinal α, let R^{α} be stage α of the least fixed point defined by φ on 𝔄, i.e R^{0} := ∅, R^{α} := φ^{𝔄}(⋃_{β<α} R^{β}) for α > 0. Then the least fixed point ψ^{𝔄} coincides with R^{γ} for some ordinal γ (whose cardinality is bounded by |𝔄|); γ is called the closure ordinal of ψ on 𝔄.

Expand 𝔄 by a monadic relation U a binary relation < and a m + 1-ary relation S (where m is the arity of R) such that

(1) (U, <) is a well-ordering of length γ + 1, and < is empty outside U.

(2) S describes the stages of φ^{𝔄} in the following way

S := {(u, b) : for some ordinal α ≤ γ, u is the α-th element of (U, <),
and b ∈ R^{α}}.

In the expanded structure 𝔄^{∗} := (𝔄, U, <, S) the stages of the operator φ^{𝔄} are defined by the sentence

η := ∀u∀x(Sux ↔ ∃z(z < u ∧ φ[Ry/∃z(z < u ∧ Szy)](x))).

Here φ[Ry/∃z(z < u ∧ Szy)](x)) is the formula obtained form φ(R, x) by replacing all occurrences of subformula Ry by ∃z(z < u ∧ Szy).

Let 𝔅^{∗} = (𝔅, U^{𝔅}, <^{𝔅}, S^{𝔅}) be a countable elementary substructure of 𝔄^{∗}, containing the tuple a. Since 𝔄^{∗} ⊧ η, also 𝔅^{∗} ⊧ η and therefore S^{𝔅} encodes the stages of φ^{𝔅}. Since also 𝔅^{∗} ⊧ ∃uSua, it follows that a is contained in the least fixed point of φ^{𝔅}, i.e., 𝔅 ⊧ ψ(a).

A straightforward iteration of this argument gives the desired result for arbitrary nestings of fixed point operators, and hence for the entire fixed point logic FO + LFP.

3 The tree model property

Tree width is an important notion in graph theory. Here we need a generalisation of this concept to arbitrary relational structures. For readers who are familiar with the notion of tree width in graph theory and the notion of the Gaifman graph of a structure we can simply say that the tree width of a structure is the tree width of its Gaifman graph. Here is a more detailed definition.

Definition 3.1. A structure 𝔅 (with universe B and arbitrary vocabulary τ) has tree width k if k is the minimal natural number satisfying the following condition. There exists a directed tree T = (V, E) and a function

F : V → {X ⊆ B : |X| ≤ k + 1},

assigning to every node v of T a set F (v) of at most k + 1 elements of 𝔅, such that the following two conditions hold.

(i) For every τ-atom α(x_{1}, …, x_{r}) and every tuple b_{1}, …, b_{r} such that 𝔅 ⊧ α(b_{1}, …, b_{r}) there exists a node v of T such that {b_{1}, …, b_{r}} ⊆ F (v).

(ii) For every element b of 𝔅, the set of nodes {v ∈ V : b ∈ F (v)} is connected (and hence induces a subtree of T).

For each node v of T, the set F (v) induces a substructure 𝔉(v) ⊆ 𝔅 of cardinality at most k + 1. (Since F (v) may be empty, we also permit empty substructures.) ⟨T, (𝔉(v)_{v∈T})⟩ is called a tree decomposition of width k of 𝔅.

Definition 3.2. A set X of elements is loosely k-guarded in a structure 𝔅 if, for some s ≤ k, there exists a tuple b_{1}, …, b_{s} in 𝔅 such that X ⊆ {b_{1}, …, b_{s}} and 𝔅 ⊧ α(b_{1}, …, b_{s}) where α(b_{1}, …, b_{s}) = α_{1} ∧ ⋯ ∧ α_{m} is a conjunction of atoms that guards b_{1}, …, b_{s} in the sense of LGF (i.e. every pair b_{i}, b_{j} coexists in some conjunct of α).

A set is loosely guarded if it is loosely k-guarded for some k. A tuple b = (b_{1}, …, b_{r}) is loosely guarded in 𝔅 if the set {b_{1}, …, b_{r}} is loosely guarded in 𝔅.

Lemma 3.3. Let ⟨T, (𝔉(v)_{v∈T})⟩ be a tree decomposition of 𝔅 and X ⊆ B be a loosely guarded set in 𝔅. Then there exists a node v of T such that X ⊆ F (v).

Proof. Let α(b_{1}, …, b_{s}) be a guard of X in 𝔅. In the case that α is atomic the claim follows immediately from the definition of a tree decomposition. Otherwise α(b) may be a conjunction α_{1} ∧ ⋯ ∧ α_{m} of atoms. For each component b ∈ b, let V_{b} be the set of nodes v such that b ∈ F (v). By the definition of a tree decomposition, each V_{b} induces a subtree of T. The fact that 𝔅 ⊧ α_{1} ∧⋯∧α_{m} and the occurrence conditions of variables in guards imply that for all b, b′ ∈ b the intersection V_{b} ∩ V_{b′} is non-empty. It is a well-known result in graph theory that any collection of pairwise overlapping subtrees of a tree has a common node (see e.g. [14, p. 94]). Hence there is a node v of the T such that F (v) contains all elements of b and therefore 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 loosely guarded k-bisimulations, the appropriate notion for loosely guarded formulae of width at most k. The width of a formula is the maximal number of free variables in subformulae of ψ.

Definition 3.4. A loosely guarded k-bisimulation, or briefly, a k-bisimulation between two τ-structures 𝔄 and 𝔅 is a non-empty set I of finite partial isomorphisms f : X → Y from 𝔄 to 𝔅, where X ⊆ A and Y ⊆ B are loosely k-guarded sets, such that the following back and forth conditions are satisfied. For every f : X → Y in I,

forth: for every loosely k-guarded set X′ ⊆ A there exists a partial isomor-

phism g : X′ → Y′ in I such that f and g agree on X ∩ X′. back: for every loosely k-guarded set Y′ ⊆ B there exists a partial isomorphism

g : X′ ↦ Y′ in I such that f^{−1} and g^{−1} agree on Y ∩ Y′.

Two τ-structures 𝔄 and 𝔅 are k-bisimilar if there exists a k-bisimulation between them.

Definition 3.5. Let LGF^{∞} be the infinitary variant of the loosely guarded fragment, extending LGF by the following rule for building new formulae: If Φ ⊆ LGF^{∞} is a set of formulae, then also ⋁ Φ and ⋀ Φ are formulae of LGF^{∞}.

Adapting basic and well-known model-theoretic techniques to the present situation, one obtains the following result.

Theorem 3.6. Let 𝔄 and 𝔅 be two τ-structures. The following are equivalent:

(i) 𝔄 and 𝔅 are k-bisimilar.

(ii) For all sentences ψ ∈ LGF^{∞} of width at most k, 𝔄 ⊧ ψ ⟺ 𝔅 ⊧ ψ.

The following simple observation relates μLGF to LGF^{∞} and shows that k-bisimilar structures cannot be separated by guarded fixed point sentences of width k.

Proposition 3.7. For each ψ ∈ μLGF of width k and each cardinal γ, there is a ψ′ ∈ LGF^{∞}, also of width k, which is equivalent to ψ on all structures up to cardinality γ.

Proof. Consider a fixed point formula [LFP Rx . φ(R, x)](x). For every ordinal α, there is a formula φ_{α}(x) ∈ LGF^{∞} that defines the stage α of the induction of φ. Indeed, let φ_{0}(x) = false and, for α > 0, let φ_{α}(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) which defines the stages prior to α. On structures of bounded cardinality, also the closure ordinal of any fixed-point formula is bounded. Hence for every cardinal γ there exists an ordinal α such that [LFP Rx . φ(R, x) is equivalent to φ_{α}(x) on structures of cardinality at most γ.

Unravelings of structures. The k-unraveling 𝔅^{(k)} of a structure 𝔅 is defined inductively. We build a tree T, with functions F and G such that each F (v) induces a loosely guarded substructure 𝔉(v) ⊆ 𝔅, each G(v) induces a substructure 𝔊(v) ⊆ 𝔅^{(k)} that is isomorphic to 𝔉(v), and ⟨T, (𝔊(v))_{v∈T} ⟩ is a tree decomposition of 𝔅^{(k)}.

The root of T is λ, with F (λ) = G(λ) = ∅. Given a node v of T with F (v) = {a_{1}, …, a_{r}} and G(v) = {a_{1}^{∗}, …, a_{r}^{∗}} we create for every loosely k-guarded set {b_{1}, …, b_{s}} in 𝔅 a successor node w of v such that F (w) = {b_{1}, …, b_{s}} and G(w) is a set {b_{1}^{∗}, …, b_{s}^{∗}} which is defined as follows. For those i, such that b_{i} = a_{j} ∈ F (v), put b_{i}^{∗} = a_{j}^{∗} so that G(w) has the same overlap with G(v) as F (w) has with F (v). The other b_{i}^{∗} in G(w) are fresh elements.

Let f_{w} : F (w) → G(w) be the bijection taking b_{i} to b_{i}^{∗} for i = 1, …, s. For 𝔉(w) being the substructure of 𝔅 induced by F (w), define 𝔊(w) so that f_{w} is an isomorphism from 𝔉(w) to 𝔊(w). Finally 𝔅^{(k)} is the structure with tree decomposition ⟨T, (𝔊(v)_{v∈T})⟩.

Note that the k-unraveling of a structure has tree width at most k − 1.

Proposition 3.8. 𝔅 and 𝔅^{(k)} are k-bisimilar.

Proof. Let I be the set of functions f_{v} : F (v) → G(v) for all nodes v of T.

It follows that no sentence of width k in LGF^{∞}, and hence no sentence of width k in μLGF distinguishes between a structure and its k-unraveling. Since every satisfiable sentence in μLGF 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 fixed point logic.

Theorem 3.9 (Weak tree model property). Every satisfiable sentence ψ in μLGF of width k has a countable model of tree width at most k − 1.

Remark. Using more sophisticated arguments, one can establish a stronger variant of the tree model property with the additional condition that the branching of the underlying tree is bounded by O(|ψ|^{k}) (see [10]).

4 Reduction to the monadic theory of trees

Let ⟨T, (𝔉(v))_{v∈T} ⟩ be a tree decomposition of width k − 1 of a τ-structure 𝔇 with universe D. We want to describe 𝔇 by a tree with a finite set of labels. To this end, we fix a set K of 2k constants and choose a function f : D → K assigning to each element d of 𝔇 a constant a_{d} ∈ K such that the following condition is satisfied. If v, w are adjacent nodes of T, then distinct elements of 𝔉(v) ∪ 𝔉(w) are always mapped to distinct constants of K.

For each constant a ∈ K, let O_{a} be the set of those nodes v ∈ T at which the constant a occurs, i.e., for which there exists an element d ∈ 𝔉(v) such that f(d) = a. Further, we introduce for each m-ary relation R of 𝔇 a tuple R̄ := (R_{a})_{a∈K^{m}} of monadic relations on T with

R_{a} := {v ∈ T : 𝔉(v) ⊧ Rd_{1} ⋯ d_{m} and f(d_{1}) = a_{1}, …, f(d_{m}) = a_{m}}.

The tree T = (V, E) together with the monadic relations O_{a} and R̄ (for R ∈ τ) is called the tree structure T (𝔇) associated with 𝔇 (and, strictly speaking, with its tree decomposition and with K and f). Note that two occurrences of a constant a ∈ K at nodes u, v of T represent the same element of 𝔇 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 T = (V, E) with monadic relations O_{a} and R̄ does define a tree decomposition of a structure 𝔇, provided that the following axioms are satisfied.

(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 symbols R ∈ τ we have the axiom

consistent(R̄) := ⋀_{a∈K^{m}} ∀x∀y((Exy ∧ ⋀_{a∈a}(O_{a}x ∧ O_{a}y)) → (R_{a}x ↔ R_{a}y)).

Note that these are first-order axioms over the vocabulary τ^{∗} := {E}∪{O_{a} : a ∈ K}∪{R̄ : R ∈ τ}. Given a tree structure T with underlying tree T = (V, E) and monadic predicates O_{a} and R_{a} satisfying (1) and (2), we obtain a structure 𝔇 such that T (𝔇) = T as follows. For every constant a ∈ K, we call two nodes u, w of T a-equivalent if T ⊧ O_{a}v for all nodes v on the link between u and w. Clearly this is an equivalence relation on O_{a}^{T}. We write [v]_{a} for the aequivalence class of the node v. The universe of 𝔇 is the set of all a-equivalence classes of T for a ∈ K, i.e.,

D := {[v]_{a} : v ∈ T, a ∈ K, T ⊧ O_{a}v}.

For every m-ary relation symbol R in τ, we define

R^{𝔇} := {([v_{1}]_{a_{1}}, …, [v_{m}]_{a_{m}}) :T ⊧ R_{a_{1}...a_{m}}v for some
(and hence all) v ∈ [v_{1}]_{a_{1}} ∩ ⋯ ∩ [v_{m}]_{a_{m}}}.

Recall that on any directed tree T = (V, E) we can express that U is the set of nodes on the link between x and y by a monadic second-order formula link(U, x, y) constructed as follows. Let first

connect(U, x, y) := Ux ∧ Uy ∧ ∃r(Ur ∧ ∀z(Ezr → ¬Uz)
∧ ∀w∀z(Ewz ∧ Uz ∧ z ≠ r → Uw)).

This formula expresses that U contains the link from x to y. Then set

link(U, x, y) := connect(U, x, y) ∧ ∀Z(connect(Z, x, y) → U ⊆ Z).

We now describe a translation from μLGF into monadic second-order logic. Given a formula φ(x_{1}, …, x_{m}) ∈ μLGF we construct, for all tuples a = a_{1}, …, a_{m} over K, monadic second-order formulae φ_{a}(z) with one free variable, which describe in the associated tree structure T (𝔇) the same properties of loosely guarded tuples as φ(x) does in 𝔇. (We will make this statement more precise below). The translation is defined by induction as follows:

(1) If φ(x) is an atom Sx_{i_{1}} ⋯ x_{i_{m}} then φ_{a}(z) := S_{b}z where b = (a_{i_{1}}, …, a_{i_{m}}).

(2) If φ = (x_{i} = x_{j}), let φ_{a}(z) = true if a_{i} = a_{j} and φ_{a}(z) = false otherwise.

(3) If φ = η ∧ ϑ, let φ_{a}(z) = η_{a}(z) ∧ ϑ_{a}(z).

(4) If φ = ¬ϑ, let φ_{a}(z) = ¬ϑ_{a}(z).

(5) If φ = (∃y . α(x, y))η(x, y), let φ_{a}(z) :=

∃U∃y(link(U, y, z) ∧ ∀x(Ux → ⋀_{a∈a}O_{a}x) ∧ ⋁_{b}(⋀_{b∈b}O_{b}y ∧ α_{ab}(y) ∧ η_{ab}(y))).

(6) If φ = [LFP Sx . η(S, x)](x), let

φ_{a}(z) := ∀S̄((consistent(S̄) ∧ ⋀_{b}∀x(S_{b}x ↔ η_{b}(S̄, x))) → S_{a}z).

Here S̄ is a tuple (S_{b})_{b∈K^{m}} of monadic predicates where m is the arity of S.

Theorem 4.1. Let φ(x) be a formula in μLGF and 𝔇 be a structure with tree decomposition ⟨T, (𝔉(v))_{v∈T} ⟩. For an appropriate set of constants K and a function f : D → K, let T (𝔇) be the associated tree structure. Then, for every node v of T and every loosely guarded tuple d ⊆ 𝔉(v) with f(d) = a,

𝔇 ⊧ φ(d) ⟺ T (𝔇) ⊧ φ_{a}(v).

Proof. We proceed by induction on φ. The only non-trivial cases are existential quantification and least fixed points.

Suppose that φ(x) = (∃y . α(x, y))η(x, y) and that 𝔇 ⊧ φ(d). Then there exists a tuple d′ such that 𝔇 ⊧ α(d, d′) ∧ η(d, d′).

Claim. There exists a node w of T such that all components of d ∪ d′ are contained in 𝔉(w).

By assumption d is loosely guarded, and α guards d′ with respect to d (i.e. α(d, d′) is a conjunction α_{1} ∧ ⋯ ∧ α_{m} of atoms such that every d′ ∈ d′ coexists with every element from d ∪ d′ in at least one conjunct of α(d, d′). Hence the conjunction of α with any guard for d is a guard for d, d′. Thus d, d′ is loosely guarded and by Lemma 3.3, the claim follows.

Let f(d′) = b. By induction hypothesis it follows that

T (𝔇) ⊧ ⋀_{b∈b}O_{b}w ∧ α_{ab}(w) ∧ η_{ab}(w).

Let U be the set of nodes on the link between v and w. Then the tuple d occurs in 𝔉(u) for all nodes u ∈ U. It follows that

T (𝔇) ⊧ link(U, v, w) ∧ ∀x(Ux → ⋀_{a∈a}O_{a}x).

Hence T (𝔇) ⊧ φ_{a}(v).

Conversely, if T (𝔇) ⊧ φ_{a}(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 (𝔇) ⊧ α_{ab}(w) ∧ η_{ab}(w) for some tuple b. By induction hypothesis this implies that 𝔇 ⊧ α(d, d′) ∧ η(d, d′) for some tuple d′, hence 𝔇 ⊧ φ(d).

Finally, let φ(x) = [LFP Sx . η(S, x)](x). By definition, 𝔇 ⊧ φ(d) is true if and only if d is contained in every fixed point of the operator η^{𝔇}, i.e. is in every relation S such that S = {c : (𝔇, S) ⊧ η(S, c)}.

We first observe that, for loosely guarded tuples d, this is equivalent to the seemingly weaker condition that d is contained in every S such that c ∈ S iff 𝔇 ⊧ η(S, c) for all loosely guarded tuples c. Indeed this is obvious, since η(S, x) is a Boolean combination of quantifier-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 quantifier. Therefore the truth values of Sc for unguarded tuples c never matters for the question whether a given guarded tuple is in φ^{𝔇}(S).

Recall that the formula associated with φ(x) and a is

φ_{a}(z) := (∀S̄)((consistent(S̄) ∧ ⋀_{b}∀x(S_{b}x ↔ η_{b}(S̄, x))) → S_{a}z).

Consider any tuple S̄ = (S_{b})_{b∈K^{m}} of monadic relations on T (𝔇) that satisifies the consistency axiom such that

(T (𝔇), S̄) ⊧ ⋀_{b}∀x(S_{b}x ↔ η_{b}(S̄, x)).

This tuple S̄ defines a relation S on 𝔇 such that for all nodes w of T and all tuples c in 𝔉(w) with f(c) = b, we have c ∈ S iff w ∈ S_{b}. Conversely each relation S on 𝔇 defines such a tuple S̄ of monadic relations on T (𝔇) which describes the truth values of S on all loosely guarded tuples of 𝔇. Since T (𝔇) ⊧ S_{b}w ↔ η_{b}(S̄, w) it follows by induction hypothesis that 𝔇 ⊧ Sc ↔ η(S, c). Further d ∈ S if and only if v ∈ S_{a}.

Hence the formula φ_{a}(v) is true in T (𝔇) if and only if d is contained in all relations S over 𝔇 such that for all loosely guarded tuples c, c ∈ S iff c ∈ η^{𝔇}(S). By the remarks above this is equivalent to saying that d is in the least fixed point of η^{𝔇}.

Theorem 4.2. The satisfiability problem for μLGF is decidable.

Proof. Let ψ be a sentence in μLGF of vocabulary τ and width k. We translate ψ into a monadic second-order sentence ψ^{∗} such that ψ is satisfiable if and only if there exists a countable tree T = (V, E) with T ⊧ ψ^{∗}.

Fix a set K of 2k constants and let Ō be the tuple of monadic relations O_{a} for a ∈ K. Further, for each m-relation symbol R ∈ τ, let R̄ be the tuple of monadic relation R_{a} where a ∈ K^{m}. The desired monadic second-order sentence has the form

ψ^{∗} := (∃Ō)(∃R̄)(χ ∧ ∀xψ_{∅}(x)).

Here χ is the first-order axiom expressing that the tree T expanded by the relations Ō and R̄ does describe a tree structure T (𝔇) associated to some τstructure 𝔇. We have shown above that this can be done in first-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.1.

If ψ is satisfiable, then by Theorem 3.9, ψ has a countable model 𝔇 of tree width k − 1. By Theorem 4.1, the associated tree structure T (𝔇) satisfies χ ∧ ∀xψ_{∅}(x), hence there exists a tree T such that T ⊧ ψ^{∗}. Conversely, if T ⊧ ψ^{∗}, then there exists an expansion T = (T, Ō, R̄) which satisfies χ and hence describes the tree decomposition of a τ-structure 𝔇. Since T ⊧ ∀xψ_{∅}(x) it follows by Theorem 4.1 that 𝔇 ⊧ ψ.

The decidability of μLGF now follows by the decidability of the monadic second-order theory of countable trees, which has been established by Rabin [13].

5 Variations

Instead of reducing the satisfiability problem for μLGF to the monadic secondorder theory of trees, we could also define a similar reduction to the μ-calculus with backward modalities and then invoke Vardi’s decidability result for this logic [16].

Further, the reduction argument can be generalized to provide in fact a reduction from a (loosely) guarded variant of second-order logic over structures of bounded tree width to monadic second-order logic over trees. As a consequence we obtain the following decidability result.

Theorem 5.1. For every constant k, the satisfiability problem for loosely guarded second-order formulae on structures of tree width at most k is decidable.

References

[1] H. Andréka, J. van Benthem, and I. Németi, Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic, 27 (1998), pp. 217– 274.

[2] J. van Benthem, Dynamic bits and pieces, ILLC research report, University of Amsterdam, 1997.

[3] A. Emerson and C. Jutla, The complexity of tree automata and logics of programs, in Proc. 29th IEEE Symp. on Foundations of Computer Science, 1988, pp. 368–377.

[4] J. Flum, On the (infinite) model theory of fixed-point logics, in Models, algebras, and proofs, X. Caicedo and C. Montenegro, eds., no. 2003 in Lecture Notes in Pure and Applied Mathematics Series, Marcel Dekker, 1999, pp. 67–75.

[5] E. Grädel, On the restraining power of guards, Journal of Symbolic Logic. To appear.

[6] E. Grädel, P. Kolaitis, and M. Vardi, On the decision problem for twovariable first-order logic, The Bulletin of Symbolic Logic, 3 (1997), pp. 53–69.

[7] E. Grädel and M. Otto, On logics with two variables, Theoretical Computer Science, (1999). To appear.

[8] E. Grädel, M. Otto, and E. Rosen, Undecidability results on two-variable logics, in Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS‘97, Lecture Notes in Computer Science Nr. 1200, Springer, 1997, pp. 249–260.

[9] E. Grädel and E. Rosen, On preservation theorems for two-variable logic, Mathematical Logic Quarterly, (1999). To appear.

[10] E. Grädel and I. Walukiewicz, Guarded fixed point logic, in Proc. 14th IEEE Symp. on Logic in Computer Science, 1999.

[11] D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science, 27 (1983), pp. 333–354.

[12] M. Mortimer, On languages with two variables, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21 (1975), pp. 135–140.

[13] M. Rabin, Decidability of second-order theories and automata on infinite trees, Transactions of the AMS, 141 (1969), pp. 1–35.

[14] B. Reed, Tree width and tangles: A new connectivity measure and some applications, in Surveys in Combinatorics, R. Bailey, ed., Cambridge University Press, 1997, pp. 87–162.

[15] M. Vardi, Why is modal logic so robustly decidable?, in Descriptive Complexity and Finite Models, N. Immerman and P. Kolaitis, eds., vol. 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1997, pp. 149– 184.

[16] , Reasoning about the past with two-way automata, in Automata, Languages and Programming ICALP 98, vol. 1443 of Springer Lecture Notes in Computer Science, 1998, pp. 628–641.