Finite Model Reasoning in Expressive Fragments of First-Order Logic

TL;DR

This paper reviews recent advances in finite model reasoning within expressive fragments of first-order logic, focusing on decision procedures for finite satisfiability and the techniques used to handle infinity axioms.

Contribution

It provides a comprehensive overview of decision procedures and techniques for finite satisfiability in key first-order logic fragments and their extensions.

Findings

Effective decision procedures for finite satisfiability

Techniques for handling infinity axioms

Open research directions identified

Abstract

Over the past two decades several fragments of first-order logic have been identified and shown to have good computational and algorithmic properties, to a great extent as a result of appropriately describing the image of the standard translation of modal logic to first-order logic. This applies most notably to the guarded fragment, where quantifiers are appropriately relativized by atoms, and the fragment defined by restricting the number of variables to two. The aim of this talk is to review recent work concerning these fragments and their popular extensions. When presenting the material special attention is given to decision procedures for the finite satisfiability problems, as many of the fragments discussed contain infinity axioms. We highlight most effective techniques used in this context, their advantages and limitations. We also mention a few open directions of study.

Tables

Table 1. Table 2: Overview of two variable logics over restricted classes of structures. Unless indicated otherwise, the complexity bounds are tight. Key to symbols: ∗) only general satisfiability and for a restricted variant ∗∗) only finite satisfiability and subject to certain restrictions on signatures.

Logic	Special symbols	Number of special symbols in the signature
		1	2	3 or more
${\text{GF}}^2$	Transitivity	2-ExpTime	undecidable	undecidable
		Sat: [22] FinSat: [29, 28]	[22, 20]	[12]
FMP
ExpTime	Equivalence	FMP, NExpTime	2-ExpTime	undecidable
[13]		[25]	[26]	[25]
${\text{FO}}^2$	Transitivity	in 2-NExpTime [53]∗)	undecidable	undecidable
		FinSat: ?	[22, 20]	[16]
FMP [34]
NExpTime	Linear order	NExpTime	Sat: ?	undecidable
[14]		[35]	ExpSpace∗∗) [50]	[35, 23]
	Equivalence	FMP, NExpTime	2-NExpTime	undecidable
		[25]	[24]	[25]

Equations

$$Px\wedge \exists y(Rxy\wedge (Qy\vee \forall z(Ryz\to \neg Pz)))$$

$$Px\wedge \exists y(Rxy\wedge (Qy\vee \forall x(Ryx\to \neg Px))).$$

$$\forall x_{\_}1($$

$$\exists x_{\_}1\exists x_{\_}2(\wedge \exists x_{\_}3(E{x}_{\_}2x_{\_}3\wedge \exists x_{\_}4(E{x}_{\_}3x_{\_}4\wedge \exists x_{\_}5(E{x}_{\_}4x_{\_}5\wedge x_{\_}1=x_{\_}5))))$$

$${\phi }^{\prime }:=\forall x\forall y\alpha \wedge \underset{\_}{\bigwedge }i\in I\forall x\exists y{\beta }_{\_}i,$$

$${\phi }^{\prime }:=\underset{\_}{\bigwedge }j\forall \bar{x}({\alpha }_{\_}j(\bar{x})\to {\vartheta }_{\_}j(\bar{x}))\wedge \underset{\_}{\bigwedge }i\forall \bar{x}({\beta }_{\_}i(\bar{x})\to \exists \bar{y}({\beta }_{\_}i(\bar{y})\wedge {\psi }_{\_}i(\bar{x},\bar{y})))$$

$${\psi }_{\_}k:=\underset{\_}{\bigwedge }j\forall \bar{x}({\alpha }_{\_}j(\bar{x})\to \forall x^{\prime }{\beta }_{\_}j(\bar{x},x^{\prime }))\wedge \underset{\_}{\bigwedge }i\forall \bar{x}({\gamma }_{\_}i(\bar{x})\to \exists x^{\prime }{\delta }_{\_}i(\bar{x},x^{\prime }))$$

$$\forall x\neg Rxx\wedge \forall x\exists yRxy\wedge \forall x\forall y(\text{mbox}TC(Rxy)\leftrightarrow Rxy).$$

$$\forall x\exists yRxy\wedge \forall x\forall y\left(Rxy\to [\text{mbox}{lfp}_{\_}W,x(Ryx\to Wy)]x\right).$$

$$\exists x\forall y\neg Ryx\wedge \forall x\exists yRxy\wedge \forall x{\exists }^{\le 1}yRyx.$$

$$\forall x\forall y\forall z(Rxy\wedge Ryz\to Rxz)$$

$$\phi =\exists x{P}_{\_}0x\wedge \underset{\_}{\bigwedge }0\le i<n\forall x(P_{\_}ix\to \exists y(Rxy\wedge P_{\_}i+1y))\wedge \underset{\_}{\bigwedge }0\le i<j<n\forall x\neg (P_{\_}ix\wedge P_{\_}jx).$$

Full text

1 Introduction

Modal logic has good algorithmic and model theoretic properties. It is well-known that formulas of propositional modal logics under Kripke semantics can be naturally encoded in first-order logic, using the so-called standard translation. But since first-order logic is not so well-behaved, in particular the (finite) satisfiability problems are undecidable, it was natural to ask what the right image of the standard translation is and ’Why is modal logic so robustly decidable?’ (the last question asked literally by Vardi in [58]).

In order to briefly review some of the answers given, let us have a short look at the standard translation. One assigns to every propositional atom $A$, a unary relation $A(x)$, which is understood as ’$A$ is true in world $x$,’ and each reachability relation $R$ corresponds to a binary relation $R(x,y)$. This assignment is extended inductively to arbitrary modal formulas: for every modal formula $\varphi$, one inductively defines a first-order formula $tr(\varphi,x)$ which expresses that ’$\varphi$ is true in world $x$’, where the boxes and diamonds are handled by explicit first-order quantification over $R$-accessible points (cf. [7]). For example, the modal formula $P\wedge\Diamond(Q\vee\Box\neg P)$ translates into the following formula

[TABLE]

One can observe that the formulas obtained under the standard translation follow some patterns: (i) variables appear in some fixed order and no rescoping of variables occurs, (ii) quantifiers are relativized by atomic formulas, (iii) negation is applied only to subformulas with a single free variable. These patterns motivated the studies of corresponding fragments of first-order logic defined by appropriately restricting the syntax.

Moreover, as observed by Gabbay [11], by properly reusing variables one can restrict their number needed for the standard translation to two. E.g. in the previous formula we could replace the variable $z$ by $x$ obtaining:

[TABLE]

This observation is crucial as already the three-variable fragment of first-order is undecidable, even for relational signatures featuring only unary nad binary predicates [19].

In the next section we introduce the fragments of first-order logic defined by the above mentioned restrictions more formally and we shortly characterize their fundamental properties in terms of the finite and tree model properties and in terms of decidability in finite and unrestricted models. Throughout the paper we refer to these languanges as the base languages. In Section 3 we review main results concerning satisfiability and finite satisfiability of some popular extensions of the base fragments. In Section 4 we sketch a few approaches of proving finite satisfiability for those fragments that do not enjoy the finite model property.

2 Base languages

We define the base languages assuming relational signatures not containing any constants or function symbols.

Definition 1

The two variable fragment*: By the $k$-variable fragment of a logic $\cal L$, denoted ${\cal L}^{k}$, we mean the set of formulas of $\cal L$ featuring at most $k$ distinct variables. In particular $\mbox{\rm FO}^{k}$ denotes the set of all first-order formulas with at most $k$ variables. The fragment $\mbox{\rm FO}^{3}$ is already undecidable [19], therefore, we are most interested in the two-variable fragment, $\mbox{\rm FO}^{2}$.*

Definition 2

The fluted fragment* [45]: Let $\bar{x}_{\_}\omega=x_{\_}1,x_{\_}2,\ldots$ be a fixed sequence of variables. We define the sets of formulas \mbox{\mbox{\rm FL}}^{[k]} (for $k\geq 0$) by structural induction as follows: (i) any atom $\alpha(x_{\_}\ell,\ldots,x_{\_}k)$, where $x_{\_}\ell,\dots,x_{\_}k$ is a contiguous subsequence of $\bar{x}_{\_}\omega$, is in \mbox{\mbox{\rm FL}}^{[k]}; (ii) \mbox{\mbox{\rm FL}}^{[k]} is closed under boolean combinations; (iii) if $\varphi$ is in \mbox{\mbox{\rm FL}}^{[k+1]}, then $\exists x_{\_}{k+1}\varphi$ and $\forall x_{\_}{k+1}\varphi$ are in \mbox{\mbox{\rm FL}}^{[k]}. The set of fluted formulas is defined as \mbox{\mbox{\rm FL}}=\bigcup_{\_}{k\geq 0}\mbox{\mbox{\rm FL}}^{[k]}. A fluted sentence is a fluted formula over an empty set of variables, i.e. an element of \mbox{\mbox{\rm FL}}^{[0]}. Thus, when forming Boolean combinations in the fluted fragment, all the combined formulas must have as their free variables some suffix of some prefix $x_{\_}1,\dots,x_{\_}k$ of $\bar{x}_{\_}\omega$; and when quantifying, only the last variable in this sequence may be bound. This is illustrated by the fluted sentence in (1). *

Definition 3

The guarded fragment* [2], GF, is defined as the least set of formulas such that: (i) every atomic formula belongs to GF; (ii) GF is closed under logical connectives $\neg,\vee,\wedge,\rightarrow$; and (iii) quantifiers are appropriately relativised by atoms. More specifically, in GF, condition (iii) is understood as follows: if $\varphi$ is a formula of GF, $\alpha$ is an atomic formula featuring all the free variables of $\varphi$, and $\bar{x}$ is any sequence of variables in $\alpha$, then the formulas ${\forall}{\bar{x}}(\alpha\rightarrow\varphi)$ and ${\exists}{\bar{x}}(\alpha\wedge\varphi)$ belong to GF. In this context, the atom $\alpha$ is called a guard. The equality symbol when present in the signature is also allowed in guards.*

Definition 4

The unary negation fragment* [51], UNF, consists of formulas in which the use of negation is restricted only to subformulas with at most one free variable. More precisely, UNF is defined as the least set of formulas such that: (i) every atomic formula of the form $R(\bar{x})$ or $x=y$ belongs to UNF; (ii) UNF is closed under logical connectives $\vee$, $\wedge$ and under existential quantification; (iii) if $\varphi(x)$ is a formula of UNF featuring no free variables besides (possibly) $x$, then $\neg\varphi(x)$ belongs to UNF.*

The base languages are incomparable in terms of expressive power. In particular, the formula $x\neq y$ is in $\mbox{\rm FO}^{2}$ but not in UNF. Formula (1) lies in the intersection of $\mbox{\rm FO}^{3}$ and FL, while (2) is not fluted. Both formulas are guarded and in UNF (the universal quantifier is used as a shortcut in a standard way). The property:

[TABLE]

belongs to FL3 but is neither two-variable, nor guarded or in UNF. The property:

[TABLE]

is in FO5 and in UNF, but is neither fluted (the variables in the subformula $x_{\_}5=x_{\_}1$ do not match the fixed ordering $x_{\_}1,\ldots,x_{\_}5$) nor guarded (none of the atoms in the subformula $Ex_{\_}4x_{\_}5\wedge x_{\_}1=x_{\_}5$ can be treated as a guard of the quantifier $\exists x_{\_}5$).

In the sequel we are concerned with two version of the classical decision problem. For a given logic $\cal L$, $\textit{Sat}(\cal L)$ is the problem to decide, given a formula $\varphi$ of $\cal L$, if $\varphi$ is satisfiable. Similarly, $\textit{FinSat}(\cal L)$ is the problem to decide, given a formula $\varphi$ of $\cal L$, if $\varphi$ is finitely satisfiable. i.e. if it has a finite model. For first-order logic both problems are undecidable [57, 54, 55] and recursively inseparable [56]. For our base languages the problems are decidable thanks to the finite model property that we explain below.

2.1 Finite Model Property and Tree Model Property

We say that a logic $\cal L$ has the finite model property (FMP), if every satisfiable formula of $\cal L$ has a finite model. If $\cal L$ has the finite property then the problems Sat($\cal L$) and FinSat($\cal L$) coincide. Moreover, if $\cal L$ is a subset of first-order logic having the finite model property, then Sat($\cal L$) (=FinSat($\cal L$)) is decidable.

In many cases, the finite model property of some logic comes with a bound on the size of minimal models from which a direct upper bound for the computational complexity of the corresponding satisfiability problem can be derived. (For a given formula it suffices to generate all possible structures within the given size bound and check if any of them satisfies the formula).

As already mentioned all four of our base languages have the FMP, and hence are decidable. Concerning the bounds on the size of minimal models, $\mbox{\rm FO}^{2}$ has the exponential model property, and this was the property used in [14] to obtain the tight upper bound on the complexity of the satisfiability problem.

An algebraic proof of the finite model property for GF can be found in [3]. In [13] FMP for GF was shown via the extension property for partial automorphisms of Hrushovski, Herwig and Lascar. In case of unbounded arities the size of the minimal models that can be easily obtained from this construction is triply exponential in the size of the formula, and not optimal for deciding finite satisfiability. FMP for UNF was shown by a reduction to the analogous result for modal logic (which has a very simple proof using filtration [10]).

FMP was used to show decidability of the fluted fragment [41]; the complexity bounds for the bounded variable fragments are not yet tight and they correspond to the best known bounds on the size of minimal models. Namely, the following is known [40]:

• •

Sat(FL) is non-elementary;

• •

Sat(FL2k) is $k$-NExpTime-hard and Sat(FLk) is in $k$-NExpTime, for all $k\geq 1$. 111There is some very recent work in progress towards showing that Sat(FL2k) is $k$-NExpTime-complete.

Tight complexity bounds of the satisfiability problem (= finite satisfiability problem) for the remaining base languages are known:

• •

Sat($\mbox{\rm FO}^{2}$) is NExpTime-complete [14].

• •

Sat(GF) is 2-ExpTime-complete; Sat(GFk) is ExpTime-complete for all $k\geq 2$ [13].

• •

Sat(UNF) is 2-ExpTime-complete; the same holds for Sat(UNFk) for all $k\geq 3$ [51].

The optimal complexity bounds for Sat(GF) have been obtained by a generalization of the tree model property, known already as an important tool from modal logic.

We say that $\cal L$ has the (generalised) tree model property, TMP, iff every satisfiable $\varphi\in\cal L$ has a tree (tree-like) model. The fragments $\mbox{\rm FO}^{2}$ and FL do not enjoy the tree model property as they allow to write formulas of the form $\forall x\forall yRxy$, enforcing all elements of a model to be connected. Grädel showed [13] that every formula of GF with $k$ variables is satisfiable only if it has a model of bounded degree such that the Gaifman graph of this model has tree width at most $k+1$. Similar property holds for UNF [51].

Tree-like models allow the use of powerful tools. For example, in the $\mu$-calculus, we can interpret them in the monadic second order theory of the infinite tree and use Rabin’s theorem (this reduction gives decidability but not good complexity) [46]. The proof of Rabin’s theorem uses tree automata, and by constructing tree automata directly, one usually gets good algorithms. However, tree-like models are usually infinite, so TMP is not suitable to decide the finite satisfiability problem. But it might help to improve the complexity bounds, when FMP can be shown independently.

In next sections we will concentrate on logics that do not enjoy FMP and where other techniques to decide finite satisfiability are applied. Before moving on we want to remark on an important pre-processing phase used in the decision procedures for the (finite) satisfiability problems.

2.2 Normal forms

When designing algorithms for (finite) satisfiability in our base languages it is useful to restrict attention to formulas in certain normal forms. The precise notion depends on the logic but in all cases the normal form formulas are obtained by iteratively substituting subformulas of the form $\exists y\psi$, for quantifier-free $\psi$ by atoms $R(\bar{y})$, where $R$ is a fresh predicate letter, $\bar{y}$ denotes the free variables of $\exists y\psi$, and adding appropriate definitions for $R$. Below we recall the corresponding lemmas for $\mbox{\rm FO}^{2}$, GF and FL.

Lemma 5** ([14])**

For every $\mbox{\rm FO}^{2}$-sentence $\varphi$ one can construct in polynomial time an $\mbox{\rm FO}^{2}$-sentence $\varphi^{\prime}$ of the form:

[TABLE]

where $\alpha$ and $\beta_{\_}i$ are quantifier-free such that $\varphi^{\prime}\models\varphi$ and every model of $\varphi$ can be expanded to a model of $\varphi^{\prime}$; moreover, if $n$ is the length of $\varphi$, then $\varphi^{\prime}$ contains at most $n$ predicate symbols and has length $O(n\log n)$.

Lemma 6** ([13])**

For every GF-sentence $\varphi$ one can construct in polynomial time a GF-sentence $\varphi^{\prime}$ of the form:

[TABLE]

*such that $\varphi^{\prime}\models\varphi$ and every model of $\varphi$ can be expanded to a model of $\varphi^{\prime}$. Here the $\alpha_{\_}j$, $\beta_{\_}i$, $\gamma_{\_}i$ are guards and the $\vartheta_{\_}j$, $\psi_{\_}i$ are quantifier-free; the length of $\varphi^{\prime}$ is linear in the length of $\varphi$. *

Lemma 7** ([40])**

Let $\varphi$ be a $\mbox{\rm FL}^{m}$-sentence over a signature $\sigma$. We can compute, in exponential time, a disjunction $\psi=\bigvee_{\_}{k}\psi_{\_}k$ over a signature $\sigma^{\prime}$, where each $\psi_{\_}k$ is an $\mbox{\rm FL}^{m}$-sentence of the form

[TABLE]

such that $\psi\models\varphi$, every model of $\varphi$ can be expanded to a model of $\psi$; moreover, if $n$ is the length of $\varphi$, then each $\psi_{\_}k$ has length $O(n\log n)$, and $\sigma^{\prime}$ consists of $\sigma$ together with some additional predicates of arity at most $m-1$. Here, in each conjunct $\bar{x}$ is a contiguous seguence $x_{\_}1\ldots x_{\_}l$ for some $l$ ($1\leq l<m$), $x^{\prime}=x_{\_}{l+1}$, and all of the formulas \alpha_{\_}j,\gamma_{\_}i\in\mbox{\mbox{\rm FL}^{[l]}} and \beta_{\_}j,\delta_{\_}i\in\mbox{\mbox{\rm FL}^{[l+1]}} are quantifier-free.

Lemma 7 seems weaker than Lemmas 5 and 6 but when aiming at any complexity bound from or above ExpTime, it also allows one to restrict attention to formulas in normal form (one can consider the disjuncts of $\psi$ one by one and check if any of them is satisfiable).

We also remark that every FL-formula over a signature $\sigma$ consisting of predicate symbols of arity at most $k$ when transformed to the fluted normal form gives a formula in $\mbox{\rm FL}^{k}$. Thus, the fluted formulas obtained by the standard translation from modal logic after normalization belong to $\mbox{\rm FL}^{2}$.

2.3 Historical Remarks

The observation that model logic can be seen as a fragment of the two-variable first-order logic was made in 1981 by Gabbay [11]. At that time it was known that $\mbox{\rm FO}^{2}$ has the doubly exponential model property and is decidable in 2-NExpTime as shown in 1975 by Mortimer [34]. The exponential model property and, hence, tight complexity bounds for $\mbox{\rm FO}^{2}$ were shown by Grädel et. al. in 1997 [14]. In the same year Grädel, Otto and Rosen published another article [16], where their performed a test for robust decidability of $\mbox{\rm FO}^{2}$ studying its extensions by adding additional operators corresponding to the operators used in modal logics. This test failed, most of the extensions turned out to lead to undecidable formalism, and therefore $\mbox{\rm FO}^{2}$ was not accepted as the right image of the standard translation of modal logic (more in the next section).

One year later in this context Andréka, van Benthem and Németi put forward the guarded fragment [2]. GF does have the the hoped-for nice properties, and has been widely accepted as a better proposal. This fragment inspired researchers over the past two decades and brought results having applications in other areas like description logics and database theory.

UNF is a young fragment, introduced by Segoufin and ten Cate in 2013 [51] as an orthogonal (to GF) generalisation of modal logic, that enjoys the same nice properties. An important additional property of UNF is that it contains unions of conjunctive queries222A conjunctive query is an existentially quantified conjunction of atoms., a class very important in the field of databases. Hence, it is not surprising that UNF and GF have already been generalised to the guarded negation fragment that retains the good properties of both UNF and GF logics [5].

The origins of the fluted fragment can be traced to a paper given by Quine to the 1968 International Congress of Philosophy [44], in which the author defined what he called the homogeneous $m$-adic formulas. In these formulas, all predicates have the same arity $m$, and all atomic formulas have the same argument sequence $x_{\_}1,\dots,x_{\_}m$. The restriction that all predicates have the same arity is abandoned in [45] published in 1976. The history of discovering the decidability and complexity of FL is complicated, and may be a reason why FL has been curiously neglected in the context of our discussion. In particular, an earlier claim that FL has the exponential model property [43] has been just disproved by showing that FL has the finite model property, and its satisfiability (= finite satisfiability) problem is decidable, but not elementary [40].

3 Extensions

Modal logic is a very weak formalism in terms of expressive power, however, numerous extensions of ML have been designated to overcome these limitations, leading to extensions that still have good algorithmic properties. Such extensions can be defined by extending the language adding new operators or restricting the classes of frames by adding new axioms. In this section we look at the impact of similar extensions on our base languages.

3.1 Additional operators

We first survey the impact of adding transitive closure operators, (monadic) fixed-points or counting quantifiers that appear, respectively, in propositional dynamic logic and in temporal logics, in the $\mu$-calculus and in graded modal logics. Any of the additional operators implies loss of the FMP that can be shown be writing infinity axioms, i.e. satisfiable formulas that have only infinite models.

As an example, consider the $\mbox{\rm FO}^{2}$-formula with the transitive closure operator, TC, applied to a binary predicate symbol:

[TABLE]

This formula is satisfiable and any model of the formula embeds a copy of the natural order relation. We can enforce essentially the same property using fixed-points:

[TABLE]

Here the lfp is the set of points that have only finitely many $R$-predecessors. A modification of the above examples in the extension of $\mbox{\rm FO}^{2}$ with counting quantifiers, C2, can be written as follows:

[TABLE]

Grädel et. al. studied several extensions of $\mbox{\rm FO}^{2}$, in particular the extensions obtained by adding the transitive closure operator and (restricted) monadic fixed points. In [16] they showed that the extensions of $\mbox{\rm FO}^{2}$ by either transitive closure (in fact, even by transitivity, cf. next subsection) or fixed points leads to undecidability for both the satisfiability and the finite satisfiability problems. Decidability of the satisfiability problem for $\mbox{\rm FO}^{2}$ with counting quantifiers came as sort of surprise and was shown independently in 1997 in [15] and [37]. It was also shown that the size of a minimal finite model of a C2-formula $\varphi$ is at least doubly exponential in $|\varphi|$ even when the counting quantifiers are only of the form $\exists^{=1}$. NExpTime-completeness of both Sat(C2) and FinSat(C2) was later proved by Pratt-Hartmann in [38].

The situation with the guarded fragment was different: GF extended with monadic fixed points is decidable and of the same complexity as the base GF: see Grädel and Walukiewicz [17] for the satisfiability problem, and Bárány and Bojańczyk [4] for the finite satisfiability problem (note that [17] is published in 1999 and [4] 13 years later).

Similar properties hold for the unary negation fragment. Despite of the loss of FMP, decidability and complexity are retained when the fragment is extended by (monadic) fixed point operators [51]. To the best of our knowledge, extensions of UNF by adding transitive closure or counting have not yet been studied.

As for the other two extensions of GF, adding either counting or transitive closure leads to undecidability. So special attention has been turned towards the two-variable guarded fragment, where counting quantifiers can be added at no additional cost. Also a decidable extension with restricted transitive closure has been identified in [32] (finite satisfiability remains open), however the complexity jumps by one exponential in comparison with $\mbox{\rm GF}^{2}$. These results are summarized in Table 1.

In Table 1 we do not list FL as this kind of extensions have not yet been properly studied. In [42] the author considers what he calls extended fluted logic, in which, in addition to the usual predicate functors, we have equality, the ability to exchange arguments in binary atomic formulas and functions (the requirement that certain specified predicates be interpreted as the graph of a function—a property easily expressed using counting quantifiers). This extension evidently contains infinity axioms, e.g. formulas equivalent to formula (11), hence the claim of [42] that this extension has FMP is false. And it remains open whether FL with counting, but without the other above mentioned functors, enjoys the finite model property and whether it is decidable.

3.2 Restricted classes of structures

In modal correspondence theory various conditions on the accessibility relations allow one to restrict the class of Kripke structures considered, e.g. to transitive structures for the modal logic K4, transitive and reflexive—for S4, or equivalence structures for the modal logic S5, and still obtain well-behaved fragments. Also in temporal logics, very natural are classes of structures with some kind of orderings, where they model time flow. The central condition here is transitivity. The transitivity axiom is a simple universal first-order formula:

[TABLE]

however, it is expressible in neither of our base languages, because it contains three variables, has no guard, and the atom $Rxz$ is not fluted. Moreover, adding transitivity axioms allows one to write sentences that have only infinite models (e.g. replacing the last conjunct in the formula (9) by the transitivity axiom (12)).

Hence, the question therefore arises as to whether transitivity (or related properties like orderings or equivalence relations) could be added at reasonable computational cost. We have already seen that it cannot be done in general. In the past years various extensions of $\mbox{\rm FO}^{2}$ and $\mbox{\rm GF}^{2}$ were investigated in which certain distinguished binary relation symbols are declared to denote transitive relations, equivalence relations, or linear orderings. It turns out that the decidability of these fragments usually depends on the number of the distinguished relation symbols available.

For three linear orders, both satisfiability and finite satisfiability are undecidable [23, 35]. Similarly for three equivalence relations [22]. Turning to transitive relations, the satisfiability problem becomes undecidable for both satisfiability and finite satisfiability of $\mbox{\rm FO}^{2}$ in the presence of two transitive relations (or even in the presence of one transitive relation and one equivalence relation [27]).

The complexity bounds for such decidable extensions of $\mbox{\rm FO}^{2}$ and $\mbox{\rm GF}^{2}$ are in many cases identical, a notable exception being the case of two equivalences, which, for $\mbox{\rm GF}^{2}$ yields a 2-ExpTime-complete logic [22], and for $\mbox{\rm FO}^{2}$—a 2-NExpTime-complete logic [24]. Table 2 summarizes the above results. We do not list there extensions of $\mbox{\rm GF}^{2}$ with linear orders, as linear orders actually destroy the guardedness of a logic: any pair of elements is guarded by a linear order, and the results from $\mbox{\rm FO}^{2}$ with linear orders can be applied to $\mbox{\rm GF}^{2}$.

For $\mbox{\rm GF}^{2}$, it also makes sense to study variants in which the distinguished predicates may appear only in guards [12]. In this case, $\mbox{\rm GF}^{2}$ with any number of equivalences appearing only as guards remains NExpTime-complete [22], while $\mbox{\rm GF}^{2}$ with any number of transitive relations appearing only as guards is 2-ExpTime-complete [52, 21] (tight complexity bounds for the finite satisfiability problem are established in [28]).

The properties of UNF and FL over restricted classes of structures have not yet been investigated. Obviously, decidability results for extensions of $\mbox{\rm FO}^{2}$ imply decidability of the same extensions of $\mbox{\rm FL}^{2}$ or UNF2. Also it is not difficult to see that the undecidability result for $\mbox{\rm FO}^{2}$ with three equivalence relations can be adapted to the fluted case, hence the satisfiability and the finite satisfiability problems for $\mbox{\rm FL}^{2}$ with at least three equivalence relations is undecidable. Other cases need more detailed inspection, additional research, perhaps also novel techniques.

It is clear that classes of structures defined by stipulating that some binary predicates satisfy some universal first-order formula by no means exhausts the relevant possibilities. One may as well consider e.g. well-founded structures, trees or forests; notions not expressible in first-order logic which arise naturally in a wide range of contexts. Also the world of guarded logics is much richer than shown above. E.g. more liberal guardedness conditions (loosely- or clique-guarded, packed fragment) and guarded fragments of other logics have been studied (guarded second order logic, Datalog LITE).

4 Deciding FinSat

Before we review some techniques used for solving the finite satisfiability problem for logics without FMP we first notice a few potential difficulties.

Let $\varphi$ be the following formula, where $P_{\_}0,\ldots,P_{\_}{n-1}$ are unary predicates and $R$ is a binary predicate:

[TABLE]

The formula $\varphi$ has a simple infinite model that is an $R$-chain of elements on which the unary predicates alternate. In order to get a finite model the $R$-chain must close into cycles. By using combinations of the unary predicates to encode a binary number at a given point of a model, one can easily enforce those cycles to have exponential length w.r.t. the length of the formula. If additionally $R$ is declared transitive, these cycles induce $R$-cliques. Note that $\varphi$ is a formula in all our base languages.

Smallest finite models might also be relatively large w.r.t. the length of the formula used to define them (and also in comparison to the optimal upper complexity of the algorithms deciding finite satisfiability). Recall e.g. the example from [15], where a family of finitely satisfiable C2-formulas $\{\varphi_{\_}n\}_{\_}{n\in{\mathbb{N}}}$ over a signature with one binary and $n$ unary predicate symbols is given, such that every finite model of $\varphi_{\_}n$ contains an isomorphic copy of a full binary tree of height $2^{n}$ and $\varphi_{\_}n$ has length $O(n\log n)$. Hence every model of $\varphi_{\_}n$ has size at least $2^{2^{n}}$. We remark at this point that both Sat(C2) and FinSat(C2) are NExpTime-complete.

This suggest that when designing efficient algorithms for the finite satisfiability problem one can not rely on properties of unrestricted models or on direct constructions of models of minimal size.

In this context let us also mention two titles of papers from the DL community praising unrestricted reasoning versus finite reasoning: ’Nominals, inverses, counting, and conjunctive queries or: Why infinity is your friend!’ [49] and ’The curse of finiteness: Undecidability of database-inspired reasoning problems in very expressive description logics’ [48].

4.1 More or less natural reductions

A perhaps most natural approach to establish (un)decidability or tight complexity bounds of some logic is to reduce formulas of one logic to another one. This classical approach can be illustrated by the extension of UNF by fixed points, UNFP. In fact in [51] an exponential reduction from UNFP to the modal $\mu$-calculus is presented that additionally preserves finiteness of the models. This immediately gives $2\textsc{-ExpTime}$-upper bounds for the complexity of both the satisfiability and the finite satisfiability problems. The same reduction allows one to deduce also FMP of UNF (under this reduction a formula from UNF translates to a modal formula without fixed points) and TMP of UNFP.

Another natural idea of solving the finite satisfiability problem for a logic that has a decidable satisfiability problem, might be to reduce the first problem to the later. This concept has an additional advantage, as for unrestricted reasoning and a family of some simple logics there is a wide range of applicable algorithms (such as e.g. tableau algorithms that rely on TMP or resolution calculi), which often perform well in practical implementations.

This approach has been investigated by Rosati in [47] for a relatively inexpressive logic called DL-Lite${}_{\_}{\cal F}$ that already lacks FMP. The idea has been later extended by Garcia et.al. to the logic Horn-ALCQI [18]. It requires additional research to find out if this concept can be further extended to non-Horn logics.

4.2 Finitary unravellings and locally acyclic structures

When we are concerned with a decidable logic that does not have FMP but has TMP, a natural idea is to study finitary unravellings, obtained by ’bending’ some edges in the tree-like models to keep the structure finite but at the same time similar to a tree, i.e. acyclic. Here, when saying that a structure is acyclic we mean that its hypergraph is. We have already observed that it is not always possible for a given formula $\varphi$ to get a model of $\varphi$ that is at the same time finite and acyclic, cf. the formula in (13).

To address the above idea a notion of $k$-acyclic structures, where $k$ is some parameter, is introduced. Informally, in a $k$-acyclic structure ${\mathfrak{A}}$ there are no cycles of length at most $k$; more precisely, every induced sub-hypergraph of the hypergraph of ${\mathfrak{A}}$ of up to $k$ vertices is acyclic.

The aim then is roughly to show that if a formula $\varphi$ has a finite model then $\varphi$ has a $k$-acyclic model, where $k$ depends only on $\varphi$. Having such a property in hand, one can restrict attention to locally acyclic structures, that are usually easier to handle. This approach has been introduced by Otto [36] for GF over restricted signatures and later extended in [6] to full GF, showing that every finite structure is GF-bisimilar to a finite structure whose hypergrah is locally acyclic. As an application of the general result a new proof of the (small) finite model property for GF with optimal bounds on the size of minimal models is obtained.

We remark that the above results underlie the correctness of the reduction outlined in the previous subsection from UNFP to the $\mu$-calculus in the finite case. They are also one of the main ingredients of the decidability proof for the finite satisfiability problem for the extension of GF with fixed points [4].

4.3 Deciding (Fin)Sat by reduction to linear or integer programming

Here we briefly describe a less direct approach that has successfully been applied to extensions of $\mbox{\rm FO}^{2}$ to get optimal complexity bounds when the logic allows one to formulate sentences that have relatively large finite models w.r.t. optimal complexity bounds for (finite) satisfiability.

The brief idea is to identify (finitely many types of) building blocks of a potential model and connecting conditions for them, and describe them in a succinct way. It turns out that these conditions often can be described by a set of (in)equalities. In such cases the approach has an additional advantage, namely it allows one to solve simultaneously both $\textit{Sat}({\cal L})$ and $\textit{FinSat}({\cal L})$: in case of $\textit{FinSat}({\cal L})$ given $\varphi\in{\cal L}$ we look for solutions of the corresponding equation system over ${\mathbb{N}}$, in case of $\textit{Sat}({\cal L})$ we look for solutions over so-called extended integers, ${\mathbb{N}}\cup\{\aleph_{\_}0\}$.333E.g. the equation $x+1=x$ has no integer solution, but has a solution over extended integers $x=\aleph_{\_}0$. If such equation appears positively in the conditions describing models of a formula $\varphi$ we deduce that $\varphi$ has no finite models. Moreover, this approach does not depend on TMP and gives hope to think about practical implementation using existing linear/integer programming solvers.

This approach has been applied to establish optimal upper complexity bounds for an expressive description logic with (restricted) counting quantifiers in [31] (ExpTime), for C2 in [38] (NExpTime), and for the quarded fragment of C2 in [39] (ExpTime). The (N)ExpTime-upper bounds should be contrasted with the remark that in these logics the size of minimal models is doubly exponential in the size of the formula.

The linear/integer programming approach has been made more transparent in [24] when dealing with the extension of $\mbox{\rm FO}^{2}$ with two equivalence relations, $\mbox{\rm FO}^{2}$+$\{E_{\_}1,E_{\_}2\}$. Suppose $E_{\_}1$ and $E_{\_}2$ are the equivalence symbols in the signature. The strategy employed in [24] starts with the observation that the intersections (i.e. equivalence classes of the coarsest common refinement $E_{\_}1\cap E_{\_}2$ of the equivalence relations) arising in any model of a formula $\varphi$ could, without loss of generality, be assumed to have cardinality exponentially bounded as a function of the size of $\varphi$. In any such model, every $E_{\_}1$-class, and also every $E_{\_}2$-class, is the union of some set of such ’small intersections’; and any given $E_{\_}1$-class and $E_{\_}2$-class are either disjoint, or have exactly one common intersection. This decomposition into equivalence classes allowed one to picture such a model as an edge-coloured, bipartite graph: the $E_{\_}1$-classes are the left-hand vertices; the $E_{\_}2$-classes are the right-hand vertices; and two vertices are joined by an edge just in case they share an intersection, with the colour of that edge being the isomorphism type of the intersection concerned.

Evidently, the formula $\varphi$ imposes constraints on the types of intersections that may arise, and on how intersections may be organized into $E_{\_}1$- and $E_{\_}2$-classes; and it was showed in [24] how these constraints translated to conditions on the induced bipartite graph of equivalence classes.

In this way, the original (finite) satisfiability problem for $\mbox{\rm FO}^{2}$+$\{E_{\_}1,E_{\_}2\}$ was nondeterministically reduced to the problem of determining the existence of a (finite) edge-coloured bipartite graph satisfying certain conditions on the local configurations it realizes. The latter problem was called BGESC (for ’bipartite graph existence with skew constraints and ceilings’). By showing BGESC and its finite version to be NPTime-complete, an optimal 2-NExpTime-upper bound for both the satisfiability and the finite satisfiability problems for $\mbox{\rm FO}^{2}$+$\{E_{\_}1,E_{\_}2\}$ was obtained. Membership in NPTime for both BGESC and the finite BGESC problems was shown by a nondeterministic polynomial reduction to an integer-programming problem.

In [24] and later in [26] two simpler variants of the BGESC problem were introduced called, respectively, BGE and BGE∗. They were shown to remain in PTime via polynomial reductions to the linear programming problems (for the finite versions) and reductions to the satisfiability problem for propositional Horn clauses (for the unrestricted versions). Reductions to the (finite) BGE∗ problem were used in [26] to show the optimal $2\textsc{-ExpTime}$-upper bound for the satisfiability and finite satisfiability problems for the guarded fragment of $\mbox{\rm FO}^{2}$+$\{E_{\_}1,E_{\_}2\}$.

The above approach has already been successfully applied to get optimal upper complexity bounds for extensions of $\mbox{\rm FO}^{2}$ where the operation of equivalence closure can be applied to one or more binary predicates [24, 26]. Such operators can be used to express non-first-order notions such as reachability or connectedness in undirected graphs—notions often encountered in practise.

It remains open whether the linear/integer programming approach might be helpful in designing optimal decision procedures for logics with more than two variables, and in particular when the signatures feature predicates of higher arity.

4.4 Remarks

In this section we discussed several logics for which it required more care to proof decidability of the finite satisfiability problem than to prove decidability of the satisfiability problem. This by no means is a general trade. In particular, there are logics such that Sat($\cal{L}$) is undecidable and FinSat($\cal{L}$) is decidable, or vice versa (see e.g. [33] for a family of examples from the elementary modal logics).

We have also mentioned fragments for which decidability of FinSat($\cal L$) has been solved and the status of Sat($\cal L$) remains open, this include some extensions of $\mbox{\rm FO}^{2}$ with order relations (cf. [50, 8] for a detailed picture).

In this area one can also find fragments for which the complexity of the finite satisfiability problem jumps to classes like vector addition systems which are ExpSpace-hard and are known to be decidable but no elementary upper bound has been found so far (cf. [30]). An example of this phenomenon is the extension of C2 with one linear order and one successor of a linear order augmented with an additional binary relation studied in [9].

5 Conclusion

The picture concerning decidability of the (finite) satisfiability problems for extensions of fragments of first-order logic defined as the natural image of the standard translation of modal logic is multidimensional and colourful. Current research in this area, apart from studying the open question already mentioned, involves investigation of logics used by combining several operators from the already well understood fragments, identifying smaller fragments with better algorithmic properties, and optimization of known algorithms towards practical implementation. Finite model reasoning is crucial to both the theory and practice of computation. It is still not well understood when addressing the problem of query answering—the central reasoning problem of database theory. We believe that this problem will gain a lot of attention in the nearest future and will intensively use results from the areas outlined in this talk.