Model-Checking on Ordered Structures

TL;DR

This paper investigates the complexity of model-checking for first- and monadic second-order logic on ordered structures, revealing intractability in general but tractability under certain order-invariant conditions on specific graph classes.

Contribution

It extends understanding of model-checking complexity by analyzing order-invariant logic on classes of structures, showing tractability results where ordering does not affect truth.

Findings

Order-invariant MSO model-checking is tractable on certain graph classes.

First-order successor-invariant formulas are tractable on graphs with bounded expansion.

Model-checking is tractable on coloured posets of bounded width.

Abstract

We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but it does become tractable on interesting classes of structures, such as on classes whose Gaifman graphs have bounded treewidth. In this paper we continue this line of research and study model-checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order invariant case, where the formulas may resort to an ordering, but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of structures. In contrast, in the order invariant case we obtain tractability results for order-invariant monadic second-order formulas on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant formulas on classes whose Gaifman graphs have bounded expansion. Furthermore, we show that model-checking for order-invariant first-order formulas is tractable on coloured posets of bounded width.

Equations

$$A(m,n)\coloneqq\begin{cases}n+1,&\text{if $m=0$};\\ A(m-1,1),&\text{if $m>0$ and $n=0$};\\ A\big{(}m-1,A(m,n-1)\big{)},&\text{if $m,n>0$}.\end{cases}$$

$$D_k:=2k-1+\sum _{i=1}^{k-1}{\hat{d}}_i,$$

$$\lambda :V(T)\to$$

$$\cup \{{\text{edge}}_{R,i\to j}:R\in \sigma ,i,j=1,\dots ,k\}\cup \{{\text{rename}}_{i\to j}:i,j=1,\dots ,k\},$$

$$\mathrm{col}_{r}(G,L)=\max_{v\in V(G)}\bigl{|}\mathrm{SReach}_{r}[G,L,v]\bigr{|},$$

$${\mathrm{col}}_r(G)=\underset{L\in \Pi (G)}{\min }{\mathrm{col}}_r(G,L).$$

$${\mathrm{adm}}_r(G,L)=\underset{v\in V(G)}{\max }{\mathrm{adm}}_r[G,L,v],$$

$${\mathrm{adm}}_r(G)=\underset{L\in \Pi (G)}{\min }{\mathrm{adm}}_r(G,L).$$

$$\mathrm{adm}_{r}(G,L)\leqslant\mathrm{col}_{r}(G,L)\leqslant\bigl{(}\mathrm{adm}_{r}(G,L)\bigr{)}^{r}.$$

$$E\coloneqq\bigl{\{}\{(v,v^{\prime}),(u,u^{\prime})\}\,:\,\text{$\{v,u\}\in E(G)$, or $v=u$ and $\{v^{\prime},u^{\prime}\}\in E(H)$}\bigr{\}}.$$

$${\mathrm{adm}}_r(G+F,L)⩽2+2\cdot {\mathrm{col}}_{2r}(G,L),$$

$${\mathrm{adm}}_r(G+F,L)⩽2\cdot {\mathrm{col}}_{2r}(G,L).$$

$${\mathrm{adm}}_r(G_i+F_i,L_i)⩽2\cdot {\mathrm{col}}_{2r}(G_i,L_i)⩽2\cdot {\mathrm{col}}_{2r}(G,L).$$

$$F=\{v_1{v}_2,v_2{v}_3,\dots ,v_{p-1}{v}_p\}\cup \bigcup _{i=1}^p{F}_i.$$

$$B=\bigcup _{u\in V(G)}{B}_u.$$

$$|B|⩽\sum _{u\in V(G)}|B_u|=|V(G)|-1.$$

$$F=\bigcup _{u\in V(G)}{F}_u\text{and}T=(V(G),F).$$

$$|F|⩽\sum _{u\in V(G)}|F_u|=|V(G)|-1.$$

$$\mathrm{adm}_{r}(G+\bar{S},L)\leqslant h\bigl{(}r,\mathrm{adm}_{40r+1}(G+F)\bigr{)},$$

$${\nabla }_r(G+S)$$

$$\displaystyle\leqslant\nabla_{10r}\bigl{(}(G+F)\bullet K_{9}\bigr{)}$$

$$⩽5\cdot 9^2\cdot (10r+1{)}^2\cdot {\nabla }_{10r}(G+F)$$

$$⩽5\cdot 9^2\cdot (10r+1{)}^2\cdot {\mathrm{col}}_{40r+1}(G+F)$$

$$f(i):=|\{j⩽i:w(i)=w(j)\}|.$$

$$F(v):=|\{i\in [n]:w(i)=v\}|.$$

$${\phi }_{\mathrm{succ}}^{(1)}(x,y):=E_{11}xy.$$

$${\phi }_{\text{k-times}}(x):=\underset{a=1}{\overset{k}{\bigvee }}\exists y{E}_{ka}xy.$$

$${\phi }_{\text{jump},1}(x),\dots ,{\phi }_{\text{jump},k-2}(x)$$

$${\phi }_{\text{jump},k-1}(x)$$

$${\phi }_{\text{jump},k}(x)$$

$${\phi }_{\text{next},a,b}^{(0)}(x,y):=$$

$${\phi }_{\text{next},a,b}^{(r+1)}(x,y):=$$

$$\displaystyle\wedge\Bigl{(}\varphi_{\text{jump},a}(x)\to\exists z\,\bigvee_{c=1}^{k}\bigl{(}E_{ac}xz\wedge\varphi_{\text{next},c,b}^{(r)}(z,y)\bigr{)}\Bigr{)}.$$

$${\delta }_{ab}:=\{\begin{array}{ll}\top ,& \text{if a=b};\\ \perp ,& \text{otherwise}.\end{array}$$

Full text

{textblock}

5(12.75,14.15)

1 Introduction

Pinpointing the exact complexity of the model-checking problem for first-order and monadic second-order logic has been the object of a large body of research. The model-checking problem for a logic $\mathcal{L}$, denoted $\mathrm{MC}(\mathcal{L})$, is the problem of deciding for a given finite structure $\mathbb{A}$ and a formula $\varphi\in\mathcal{L}$ whether $\mathbb{A}$ is a model of $\varphi$; in symbols $\mathbb{A}\models\varphi$. We will denote $\mathrm{MC}(\mathcal{L})$ restricted to a class $\mathscr{C}$ of input structures as $\mathrm{MC}(\mathcal{L},\mathscr{C})$.

Vardi [59] proposed to distinguish the complexity of the model-checking problem into data, formula, and combined complexity, depending on whether we treat the structure $\mathbb{A}$ (the data) as input while considering $\varphi$ as fixed, the formula as input while considering $\mathbb{A}$ as fixed, or considering both $\mathbb{A}$ and $\varphi$ as part of the input. As shown by Vardi, for any fixed formula $\varphi\in\mathrm{FO}$ of size $|\varphi|$ the model-checking problem is solvable in polynomial time $n^{\mathcal{O}(|\varphi|)}$, i.e. the data complexity of $\mathrm{MC}(\mathrm{FO})$ is in Ptime. On the other hand, the formula complexity and combined complexity of first-order logic is Pspace-complete already on a fixed 2-element structure [5]. Evaluating a fixed formula of monadic second-order logic belongs to the polynomial time hierarchy. (And for each level $\Sigma_{i}^{p}$ and $\Pi_{i}^{p}$ there exists an $\mathrm{MSO}$-formula whose model-checking problem is complete for that level [57].) Again, the formula complexity and combined complexity of monadic second-order logic is PSpace-complete.

A more fine-grained analysis of model-checking complexity can be achieved through the lens of parameterised complexity. In this framework, the model-checking problem $\mathrm{MC}(\mathcal{L})$ for a logic $\mathcal{L}$ is said to be fixed-parameter tractable if it can be solved in time $f(|\varphi|)\cdot|\mathbb{A}|^{c}$, for some function $f$ (usually required to be computable) and a constant $c$ independent of $\varphi$ and $\mathbb{A}$. The complexity class FPT of all fixed-parameter tractable problems is the parameterised analogue to Ptime as a model of efficient solvability. Hence, parameterised complexity lies somewhere between data and combined complexity, in that the formula is not taken to be fixed and yet has a different influence on the complexity than the structure. Already the model-checking problem for first-order logic is complete for the parameterised complexity class $\textsc{AW}[\ast]$, which is conjectured and widely believed to strictly contain the class FPT. Thus it is widely believed that model-checking for first-order logic (and thus also for monadic second-order logic) is not fixed-parameter tractable.

Perhaps the most famous result on the parameterised complexity of model-checking is Courcelle’s theorem [7], which states that every algorithmic property on graphs definable in monadic second-order logic (with quantification over edge sets) can be evaluated in linear time on any class of graphs of bounded treewidth. An equivalent statement is that $\mathrm{MC}(\mathrm{MSO},\mathscr{C})$ is fixed-parameter tractable via a linear-time algorithm for any class $\mathscr{C}$ of bounded treewidth. This result was followed by a similar result for monadic second-order logic with only quantification over vertex sets on graph classes of bounded clique-width [9]. It was shown in [39, 40] that Courcelle’s theorem cannot be extended in full generality much beyond bounded treewidth.

For first-order logic, Seese [55] proved that first-order model-checking is fixed-parameter tractable on any class of graphs of bounded degree. This result was the starting point of a long series of papers establishing tractability results for first-order model-checking on sparse classes of graphs; see e.g. [24, 22, 11, 15, 31], and see [29] for a survey. This line of research culminated in the theorem of Grohe et al. [31] stating that for any nowhere dense class $\mathscr{C}$ of graphs we have $\mathrm{MC}(\mathrm{FO},\mathscr{C})\in\textsc{FPT}$. Moreover, for classes of graphs that are closed under taking subgraphs, this yields a precise characterisation of tractability for first-order model-checking [15].

So far, most of the work on algorithmic meta-theorems has focused on unordered structures. Many of the results mentioned above rely on locality theorems for first-order logic, such as Gaifman’s locality theorem [25], and the applied techniques do not readily extend to ordered structures. In this paper we study the complexity of first-order model-checking on structures where an ordering is available to be used in formulas. We do so in two different settings. The first is that the input structures are equipped with a fixed order or with a fixed successor relation. (A successor relation is a directed Hamiltonian path on the universe of the structure.) We show that first-order logic on ordered structures as well as on structures with a successor relation is essentially intractable on nearly all interesting classes.

The other case we consider is an order-invariant or a successor-invariant logic. In order-invariant logics, we are allowed to use an order relation in the formulas, but whether the formula is true in a given structure must not depend on the particular choice of order.

It is easily seen that the expressive power of order-invariant $\mathrm{MSO}$ is greater than that of plain $\mathrm{MSO}$, as, e.g. with an order we can formalise in $\mathrm{MSO}$ that a structure has an even number of elements, a property not definable without an order. In fact, the expressive power of order-invariant $\mathrm{MSO}$ is even greater than the expressive power of the extension of $\mathrm{MSO}$ with counting quantifiers $\mathrm{CMSO}$ [28]. Over restricted classes of structures, order-invariant $\mathrm{MSO}$ and $\mathrm{CMSO}$ have the same expressive power (see e.g. [8]). This holds true for successor-invariant $\mathrm{MSO}$ as well, as an order is definable from a successor relation via $\mathrm{MSO}$.

For monadic second-order logic we are able to show that order-invariant $\mathrm{MSO}$ is tractable on essentially the same classes of graphs as plain $\mathrm{MSO}$, i.e. we can increase the expressive power without restricting the tractable cases. To be precise, we show that the model-checking problem for order-invariant $\mathrm{MSO}$ on classes of graphs of bounded clique-width is fixed-parameter tractable. Furthermore, combining the result of Courcelle [7] and results that one can add the edges of a successor relation to a graph of bounded treewidth without increasing its treewidth too much, we get that model-checking for order-invariant $\mathrm{MSO}$ (with quantification over edge sets) on classes of graphs of bounded treewidth is fixed-parameter tractable.

Also successor- and order-invariant first-order logic have both been studied intensively in the literature, see e.g. [50, 47, 1, 53, 52, 19]. However, the difference between the expressive powers of order-invariant, successor-invariant, and plain $\mathrm{FO}$ on various classes of structures remains largely unexplored. An unpublished result of Gurevich states that the expressive power of order-invariant $\mathrm{FO}$ is stronger than that of plain $\mathrm{FO}$ (see e.g. Theorem 5.3 of [41] for a presentation of the result). Rossman [53] proved the stronger result that that successor-invariant $\mathrm{FO}$ is more expressive than plain $\mathrm{FO}$. The construction of [53] creates dense instances though, and no separation between successor-invariant $\mathrm{FO}$ and plain $\mathrm{FO}$ is known on sparse classes, say on classes of bounded expansion. On the other hand, collapse results in this context are known only for very restricted settings. It is known that order-invariant $\mathrm{FO}$ collapses to plain $\mathrm{FO}$ on trees [1, 46] and on graphs of bounded treedepth [16]. Moreover, order-invariant $\mathrm{FO}$ is a subset of $\mathrm{MSO}$ on graphs of bounded degree and on graphs of bounded treewidth [1], and, more generally, on decomposable graphs in the sense of [19].

We show that, up to a narrow gap, the model-checking results for plain $\mathrm{FO}$ carry over to successor-invariant $\mathrm{FO}$. In particular, we show that model-checking successor-invariant $\mathrm{FO}$ is fixed-parameter tractable on any class of graphs of bounded expansion. Classes of bounded expansion generalise classes with excluded topological minors, and form a natural meta-class one step below nowhere dense classes of graphs. More precisely, we show that if $\mathscr{C}$ is a class of structures of bounded expansion, then model-checking for successor-invariant first-order formulas on $\mathscr{C}$ can be solved in time $f(|\varphi|)\cdot n\cdot\alpha(n)$, where $n$ is the size of the universe of the given structure, $f$ is some function, and $\alpha(\cdot)$ is the inverse Ackermann function. Note that model-checking for plain $\mathrm{FO}$ can be done in linear time on classes of bounded expansion [15], thus the running time of our algorithm is very close to the best known results for plain $\mathrm{FO}$.

The natural way of proving tractability for successor-invariant $\mathrm{FO}$ on a specific class $\mathscr{C}$ of graphs is to show that any given graph $G\in\mathscr{C}$ can be augmented by a new set $S$ of coloured edges which form a successor relation on $V(G)$ such that $G+S$ falls within a class $\mathscr{D}$ of graphs on which plain $\mathrm{FO}$ is tractable. In this way, model-checking for successor-invariant $\mathrm{FO}$ on the class $\mathscr{C}$ is reduced to the model-checking problem for $\mathrm{FO}$ on $\mathscr{D}$. The main problem is how to construct the set of augmentation edges $S$. For classes of bounded expansion, to construct such an edge set, we rely on a characterisation of bounded expansion classes by generalised colouring numbers. The definition of these graph parameters is roughly based on measuring reachability properties in a linear vertex ordering of the input graph. Any such ordering yields a very weak form of decomposition of a graph in terms of an elimination tree. The main technical contribution of this paper is that we find a way to control these elimination trees so that we can use them to define, in a first step, a set $F$ of new edges with the following properties: a) $F$ forms a spanning tree of the input graph $G$, b) $F$ has maximum degree at most $3$, and c) after adding all the edges of $F$ to the graph, the increase in the colouring numbers is bounded. In a second step, from the bounded degree spanning tree we will construct a successor relation $S$ as desired.

This construction, besides its use in this paper, yields a new insight into the elimination trees generated by colouring numbers. We believe it may prove useful in future research as well.

As mentioned before, the tractability of model-checking for $\mathrm{FO}$ on sparse graphs is well understood, while only few results are available for classes of dense graphs. We review some known results for $\mathrm{FO}$ model-checking on dense graph classes in Section 6 and show that a result by Gajarský et al. [26] carries over to order-invariant $\mathrm{FO}$.

Organisation of the paper.

In Section 2 we fix the terminology and notation used throughout the paper. In Section 3 we study the case of ordered structures, i.e. structures equipped with a fixed order or successor relation. Order-invariant $\mathrm{MSO}$ is considered in Section 4. We recall the notions from the theory of sparse graphs, in particular the generalised colouring numbers, and prove tractability of successor-invariant $\mathrm{FO}$ on bounded expansion classes in Section 5. Finally, in Section 6 we consider order-invariant $\mathrm{FO}$ on posets of bounded width and other dense classes of structures.

Acknowledgements.

We thank Christoph Dittmann and Viktor Engelmann for many hours of fruitful discussions.

2 Preliminaries

General notation.

By $\mathbb{N}$ we denote the set of nonnegative integers. For a set $X$, by $\binom{X}{2}$ we denote the set of unordered pairs of elements of $X$, that is, $2$-element subsets of $X$. By $\alpha(\cdot)$ we denote the inverse Ackermann function, i.e. the inverse of the function $n\mapsto A(n,n)$ with

[TABLE]

Relational structures.

We consider finite structures over finite signatures that contain only relation symbols and constant symbols. Hence a signature $\tau=\{R_{1},\ldots,R_{k},c_{1},\ldots,c_{s}\}$ is a finite set of relation symbols $R_{i}$ and constant symbols $c_{i}$, where each relation symbol $R\in\tau$ is assigned an arity $\mathrm{ar}(R)$ (arities are part of the signature). A $\tau$-structure \mathbb{A}=\bigl{(}V(\mathbb{A}),R_{1}(\mathbb{A}),\ldots,R_{k}(\mathbb{A}),c_{1}(\mathbb{A}),\ldots,c_{s}(\mathbb{A})\bigr{)} consists of a set $V(\mathbb{A})$, the universe of $\mathbb{A}$, for each $R_{i}\in\tau$ a relation $R_{i}(\mathbb{A})\subseteq V(\mathbb{A})^{\mathrm{ar}(R_{i})}$, and for each $c_{i}\in\tau$ a constant $c_{i}(\mathbb{A})\in V(\mathbb{A})$. If $\mathbb{A}$ is a $\tau$-structure and $R$ is a relation symbol not in $\tau$ with associated arity $r$ and $R(\mathbb{A})\subseteq V(\mathbb{A})^{r}$ is an $r$-ary relation over $V(\mathbb{A})$, we write $(\mathbb{A},R(\mathbb{A}))$ for the $\tau\cup\{R\}$-structure obtained by extending $\mathbb{A}$ with the relation $R(\mathbb{A})$. The order $|\mathbb{A}|$ of a $\tau$-structure $\mathbb{A}$ is $|V(\mathbb{A})|$, and its size $\lVert\mathbb{A}\rVert$ is $|\tau|+|V(\mathbb{A})|+\sum_{R\in\tau}|R(\mathbb{A})|$, which corresponds to the size of a representation of $\mathbb{A}$ in an appropriate model of computation. We call a structure $G$ of signature $\{E\}$, where $E$ is a binary relation symbol, a digraph, and if $E(G)$ is symmetric and irreflexive, we call $G$ a graph. Let $V$ be a set. A successor relation on $V$ is a binary relation $S\subseteq V\times V$ such that $(V,S)$ is a directed path of length $|V|-1$. We write $\bar{a}$ for a finite sequence $(a_{1},\ldots,a_{k})$ and usually leave it to the context to determine the length of a sequence. The Gaifman-graph $G(\mathbb{A})$ of a $\tau$-structure $\mathbb{A}$ is the graph with vertex set $V(\mathbb{A})$ and edge set \{(u,v)\,:\,\text{u\neq v$and there is an$R\in\tau$and a tuple$\bar{a}\in R(\mathbb{A})$such that$u,v\in\bar{a}}\}.

First-order logic.

We assume familiarity with first-order logic $\mathrm{FO}$ and monadic second-order logic $\mathrm{MSO}$. We write $\mathrm{FO}(\tau)$ and $\mathrm{MSO}(\tau)$ for the set of all $\mathrm{FO}$ and $\mathrm{MSO}$ formulas over signature $\tau$, respectively. If $\varphi$ is a formula of $\mathrm{FO}$ or $\mathrm{MSO}$, we write $|\varphi|$ for the length (of an encoding) of $\varphi$. If $\varphi$ is a sentence of $\mathrm{FO}(\tau)$ or $\mathrm{MSO}(\tau)$ and $\mathbb{A}$ a $\tau$-structure, we write $\mathbb{A}\models\varphi$ if $\varphi$ is true in $\mathbb{A}$. If $\varphi(\bar{x})$ has free variables $\bar{x}$ and $\bar{a}\in V(\mathbb{A})^{k}$ is a tuple of the same length as $\bar{x}$, we write $\mathbb{A}\models\varphi(\bar{a})$ if $\varphi$ is true in $\mathbb{A}$, where the free variables $\bar{x}$ are interpreted by the elements of $\bar{a}$ in the obvious way. We write $\varphi(\mathbb{A})$ for the relation $R\coloneqq\{\bar{a}\,:\,\mathbb{A}\models\varphi(\bar{a})\}$. We call a formula $\varphi(\bar{x})$ over signature $\tau=\sigma\cup\{<\}$ order-invariant if for every $\sigma$-structure $\mathbb{A}$ and all linear orders $<_{1},<_{2}$ over $V(\mathbb{A})$ we have $\varphi(\mathbb{A},<_{1})=\varphi(\mathbb{A},<_{2})$. Analogously, we call a formula $\varphi(\bar{x})$ over signature $\tau=\sigma\cup\{S\}$ (where $S$ is a binary relation symbol) successor-invariant if for every $\sigma$-structure $\mathbb{A}$ and all successor relations $S_{1},S_{2}$ over $V(\mathbb{A})$ we have $\varphi(\mathbb{A},S_{1})=\varphi(\mathbb{A},S_{2})$. We write $\mathrm{FO}[{<}\mathit{-inv}]$ and $\mathrm{MSO}[{<}\mathit{-inv}]$ for the set of all order-invariant $\mathrm{FO}$ and $\mathrm{MSO}$ formulas, respectively, and $\mathrm{FO}[+1\mathit{-inv}]$ and $\mathrm{MSO}[+1\mathit{-inv}]$ for the set of all successor invariant $\mathrm{FO}$ and $\mathrm{MSO}$ formulas, respectively. We write $\mathrm{FO}[{<}]$ and $\mathrm{MSO}[{<}]$ for the set of all $\mathrm{FO}$ and $\mathrm{MSO}$ formulas, respectively, over a signature which contains at least the binary relation symbol $<$, and similarly for $\mathrm{FO}[{+1}]$ and $\mathrm{MSO}[{+1}]$. For any order-invariant formula $\varphi$ and any $\tau$-structure $\mathbb{A}$, we denote $\mathbb{A}\models_{\mathrm{ord-inv}}\varphi$ if for some (equivalently, every) order relation $<$ on the universe of $\mathbb{A}$ it holds that $(\mathbb{A},<)\models\varphi$. Similarly, For a successor-invariant formula $\varphi$ and any $\tau$-structure $\mathbb{A}$, we denote $\mathbb{A}\models_{\mathrm{succ-inv}}\varphi$ if for some (equivalently, every) successor relation $S$ on the universe of $\mathbb{A}$ it holds that $(\mathbb{A},S)\models\varphi$.

Throughout the paper we study the complexity of order- and successor-invariant logics on restricted classes of structures. As usual in this type of research we focus on classes of graphs. More general structures can be reduced to this case using their Gaifman-graphs. In our analysis we will use the framework of parameterised complexity, see, e.g. [10, 13, 23]. A parameterised problem is a subset of $\Sigma^{*}\times\mathbb{N}$ where $\Sigma$ is a fixed finite alphabet. For an instance $(w,k)\in\Sigma^{*}\times\mathbb{N}$, $k$ is called the parameter.

Let $\mathscr{C}$ be a class of graphs and $\mathcal{L}$ be one of first-order or monadic second-order logic. The order-invariant model-checking problem $\mathrm{MC}(\mathcal{L}[{<}\textit{-inv}],\mathscr{C})$ of the logic $\mathcal{L}$ on the class $\mathscr{C}$ of graphs is defined as the problem

$\mathrm{MC}(\mathcal{L}[{<}\textit{-inv}],\mathscr{C})$

Input:

$G\in\mathscr{C}$, order-invariant $\varphi\in\mathcal{L}(\{E,<\})$

Parameter:

$|\varphi|$

Problem:

$G\models_{\mathrm{ord-inv}}\varphi$ ?

Analogously, we define the successor-invariant model-checking problem $\mathrm{MC}(\mathcal{L}[+1\textit{-inv}],\mathscr{C})$ for $\mathcal{L}$ on $\mathscr{C}$, where instead the formula $\varphi\in\mathcal{L}(\{E,S\})$ is required to be successor-invariant.

Finally, we define the ordered model-checking problem $\mathrm{MC}(\mathcal{L}[{<}],\mathscr{C})$ for $\mathcal{L}$ on $\mathscr{C}$ as

$\mathrm{MC}(\mathcal{L}[{<}],\mathscr{C})$

Input:

$G\in\mathscr{C}$, $<$ a linear order of $V(G)$ and $\varphi\in\mathcal{L}(\{E,<\})$

Parameter:

$|\varphi|$

Problem:

$(G,<)\models\varphi$?

Likewise, we define the model-checking problem $\mathrm{MC}(\mathcal{L}[{+1}],\mathscr{C})$ with successor for $\mathcal{L}$ on $\mathscr{C}$, which gets as input a graph $G\in\mathscr{C}$, a successor relation $S$ on $V(G)$, and a formula $\varphi\in\mathcal{L}(\{E,S\})$.

The order- and successor-invariant model-checking problems are fixed-parameter tractable, or in the complexity class FPT, if there are algorithms that correctly decide on input $(G,\varphi)$ whether ${(G,<)}\models\varphi$ for some linear order $<$ or $(G,S)\models\varphi$ for some successor relation $S$, respectively, in time $f(|\varphi|)\cdot\lVert G^{\mathcal{O}(1)}\rVert$, for some function $f:\mathbb{N}\to\mathbb{N}$ in the case where $\varphi$ is order invariant or successor invariant, respectively. We have a similar definition of FTP for $\mathrm{MC}(\mathcal{L}[{<}])$ and $\mathrm{MC}(\mathcal{L}[{+1}])$. The model-checking problem for first-order logic is complete for the parameterised complexity class $\textsc{AW}[\ast]$, which is conjectured and widely believed to strictly contain the class FPT. Thus it is widely believed that model-checking for first-order logic (and thus also for monadic second-order logic) is not fixed-parameter tractable.

3 Model-Checking on Ordered Structures

In this section we investigate the tractability of model-checking on classes of ordered structures and on classes of structures with a successor relation. Of course, it is easy to come up with classes of ordered structures on which model-checking is fixed-parameter tractable, e.g. by taking the class of all cliques with a linear order on the vertex set. Thus we seek restrictions as weak as possible while still allowing us to show that model-checking is AW$[\ast]$-hard.

3.1 Coloured Sets

We start by observing that on the class of ordered coloured sets (and, a forteriori, on the class of coloured sets with a successor relation), model-checking is tractable even for monadic second-order logic. This is Büchi-Elgot-Trakhtenbrot’s Theorem (cf. [23]), since coloured ordered sets are just strings. Thus model-checking for $\mathrm{MSO}$ is fixed-parameter tractable on structures whose signature contains only unary relation symbols, apart from the order relation.

3.2 Vertex-Ordered Graphs

The simplest case not covered by the preceding paragraph is that of ordered graphs, i.e. $\{E,{<}\}$-structures where both $E$ and ${<}$ are binary relation symbols. We show that model-checking for first-order logic is AW$[\ast]$-hard even for very simple graphs.

Theorem 1**.**

*Let $\mathscr{C}$ be a class of graphs. If $\mathscr{C}$ contains all partial matchings, then $\mathrm{MC}(\mathrm{FO}[{<}],\mathscr{C})$ is AW$[\ast]$-hard. If $\mathscr{C}$ contains all star forests, then $\mathrm{MC}(\mathrm{FO}[+1],\mathscr{C})$ is AW$[\ast]$-hard. *

Here, a partial matching is a disjoint union of edges and isolated vertices (i.e. a graph of maximum degree 1), while a star forest is a disjoint union of stars (complete bipartite graphs $K_{1,n}$ with $n\geqslant 0$). Note that on both these graph classes, the model-checking problem for plain $\mathrm{FO}$ is fixed-parameter tractable.

Proof.

For the first part we show how to construct in polynomial time for every graph $G$ a $\{E,{<}\}$-structure $\mathbb{A}$ such that $G$ can be $\mathrm{FO}$-interpreted in $\mathbb{A}$. For this, let $\{v_{1},\ldots,v_{n}\}$ be the vertex set of $G$ ordered in an arbitrary way, and assume that $v_{i}$ has degree $d_{i}$ in $G$. To each vertex in $G$ we associate an interval of length ${\hat{d}}_{i}\coloneqq\max\{d_{i},1\}$ in $\mathbb{A}$, and separate the intervals by gaps of length $2$. Thus with

[TABLE]

we associate with $v_{i}$ the interval $\{D_{i},\ldots,D_{i}+{\hat{d}}_{i}-1\}$. The edge set $E(\mathbb{A})$ consists of the edges $\{D_{i}-2,D_{i}-1\}$ for $i\geqslant 2$, together with the edges $\{D_{i}+k,D_{j}+\ell\}$ if $v_{i}v_{j}$ is an edge of $G$, $v_{j}$ is the $k$-th neighbour of $v_{i}$ in the ordering, and $v_{i}$ is the $\ell$-th neighbour of $v_{i}$. Notice that the edges $\{D_{i}-2,D_{i}-1\}$ are the only edges between consecutive elements, so they can be used to determine the intervals used in this construction.

For the second part we construct a structure $\mathbb{A}^{\prime}$ consisting of a disjoint union of stars and a successor relation that can be used to recover the original graph using an $\mathrm{FO}$ interpretation. Again, we assume the vertex set of $G$ to be $\{v_{1},\ldots,v_{n}\}$. A vertex $v$ is encoded by a path $v^{-1},v,v^{+1}$. The vertices of these paths are placed at the beginning of the successor relation in an arbitrary order. An edge $e$ is encoded by three vertices $e^{-1},e,e^{+1}$ such that $e$ is a direct successor of $e^{-1}$ and $e^{+1}$ is a direct successor of $e$. All these vertices are placed at the end of the successor relation. For every edge $e=vw$, assume that $v$ is smaller than $w$ in the successor relation. We connect, in $\mathbb{A}^{\prime}$, $v$ to $e^{-1}$ and $w$ to $e^{+1}$. Again, $G$ may be recovered from $\mathbb{A}^{\prime}$ using an $\mathrm{FO}$ interpretation. $\square$

As a corollary of the previous theorem we get that $\mathrm{MC}(\mathrm{FO}[+1],\mathscr{P})$ and $\mathrm{MC}(\mathrm{FO}[{<}],\mathscr{T})$ are AW$[\ast]$-hard for the class $\mathscr{P}$ of planar graphs and the class $\mathscr{T}$ of graphs of treewidth $1$ (forests). However, for $\mathrm{MC}(\mathrm{FO}[+1],\mathscr{C})$ to be AW$[\ast]$-hard it is essential that the graphs in the class $\mathscr{T}$ have unbounded degree. Indeed, on graph classes of bounded degree, successor-invariant $\mathrm{FO}$ model-checking is tractable.

Theorem 2**.**

*For every $d\geqslant 0$ let $\mathscr{D}_{d}$ be the class of graphs of maximum degree at most $d$. Then for all $d\geqslant 0$, $\mathrm{MC}(\mathrm{FO}[+1],\mathscr{D}_{d})$ is fixed-parameter tractable. In fact, we can allow any (fixed) number of successor relations on top of $\mathscr{D}_{d}$ and still have tractable first-order model-checking. *

Proof.

By a result of Seese [55] the model-checking problem for $\mathrm{FO}$ on graphs of bounded degree and also on all structures with Gaifman-graph of bounded degree is fixed-parameter tractable. Adding a successor relation increases the degree of the Gaifman-graph of a structure by at most two. $\square$

4 Order-Invariant MSO

In this section we consider order-invariant logics. The most expressive logic studied in the context of algorithmic meta-theorems is monadic second-order logic, the extension of first-order logic by quantification over sets of elements. With respect to graphs, there are two variants of $\mathrm{MSO}$ usually considered, one, called $\mathrm{MSO}_{1}$, where we can quantify over sets of vertices, and the other, called $\mathrm{MSO}_{2}$, where we can additionally quantify over sets of edges. It was shown by Courcelle [7] that $\mathrm{MSO}_{2}$ is fixed-parameter tractable on every class of graphs of bounded treewidth. Later, Courcelle et al. [9] showed that $\mathrm{MSO}_{1}$ is fixed-parameter tractable on every class of graphs of bounded clique-width, a concept more general than bounded treewidth. In this section, we show that for both logics we can allow order-invariance without increase in complexity.

We first consider the case of $\mathrm{MSO}_{2}$. As shown in Theorem 5.1.1. of [51], for every graph $G$ of treewidth $k$ there is a successor relation $S$ on $V(G)$ such that the graph obtained from $G$ by adding the edges in $S$ has treewidth at most $k+2$. From the proof one can easily derive an algorithm that takes as input a a graph $G$ and a tree decomposition of $G$ of width $k$ and outputs a successor relation as desired in polynomial time. We can use the algorithm of Bodlaender [2] to compute an optimal tree decomposition in time $2^{\mathcal{O}(k^{3})}\cdot n$ first, and then compute the desired successor relation. We also refer to [43] and [6] for proofs that for every graph $G$ of treewidth $k$ there is a successor relation $S$ on $V(G)$ such that the graph obtained from $G$ by adding the edges in $S$ has treewidth at most $k+5$. In combination with Courcelle’s theorem, this implies the following result.

Theorem 3**.**

*For any class $\mathscr{C}$ of bounded treewidth, $\mathrm{MC}(\mathrm{MSO}_{2}[{<}\mathit{-inv}],\mathscr{C})$ is fixed-parameter tractable. *

In fact, $\mathrm{MC}(\mathrm{MSO}_{2}[{<}\mathit{-inv}])$ is fixed-parameter tractable with parameter $|\varphi|+\mathrm{tw}(G)$, where $\mathrm{tw}(G)$ is the treewidth of a graph $G$. We prove next that also for $\mathrm{MSO}_{1}$ and clique-width we can allow order-invariance without loss of tractability.

Theorem 4**.**

*For any class $\mathscr{C}$ of graphs of bounded clique-width, $\mathrm{MC}(\mathrm{MSO}_{1}[{<}\mathit{-inv}],\mathscr{C})$ is fixed-parameter tractable. *

We first review the definition of clique-width. For the rest of this section we fix a relational signature $\sigma$ in which every relation symbol has arity at most $2$.

Definition 1** ($\sigma$-clique-expression of width $k$).**

Let $k\in\mathbb{N}$ be fixed. A $\sigma$-clique-expression of width $k$ is a pair $(T,\lambda)$, where $T$ is a directed rooted tree in which all edges are directed away from the root and

[TABLE]

such that for all $t\in V(T)$ we have: if $\lambda(t)\in\{\mathbf{1},\dots,\mathbf{k}\}$, then $t$ is a leaf of $T$; if $\lambda(t)=\oplus$, then $t$ has exactly two successors; and in all other cases $t$ has exactly one successor.

Definition 2**.**

Let $(T,\lambda)$ be a $\sigma$-clique-expression of width $k$. With every $t\in V(T)$ we associate a $\sigma$-structure $G(t)$ in which vertices are coloured by colours $\mathbf{1},\dots,\mathbf{k}$ as follows.

• •

If $t$ is a leaf, then $G(t)$ consists of one element coloured by $\lambda(t)$.

• •

If $\lambda(t)=\oplus$ and $t$ has successors $t_{1},t_{2}$, then $G(t)$ is the disjoint union $G(t_{1})\mathop{\dot{\cup}}G(t_{2})$.

• •

If $\lambda(t)=\textup{edge}_{R,i\to j}$ and $t_{1}$ is the successor of $t$, then $G(t)$ is the structure obtained from $G(t_{1})$ by adding to the relation $R(G(t))$ all pairs $(u,v)$ such that $u$ has colour $i$ and $v$ has colour $j$.

• •

If $\lambda(t)=\textup{rename}_{i\to j}$ and $t_{1}$ is the successor of $t$, then $G(t)$ is the structure obtained from $G(t_{1})$ by changing the colour of all vertices $v$ which have colour $i$ in $G(t_{1})$ to colour $j$ in $G(t)$.

The $\sigma$-structure generated by $(T,\lambda)$ is the structure $G(r)$, where $r$ is the root of $T$, from which we remove all colours $\{\mathbf{1},\dots,\mathbf{k}\}$. Finally, the clique-width of a $\sigma$-structure $G$ is the minimal width of a clique-expression generating $G$.

Combining results from [34] and [48] yields the following well-known result.

Theorem 5**.**

*There is a computable function $f:\mathbb{N}\to\mathbb{N}$ and an algorithm which, given a graph $G$ of clique-width at most $k$ as input, computes a clique-expression of width at most $2^{k+1}$ in time $f(k)\cdot|G|^{3}$. *

Combining this theorem with results of Courcelle et al. [9] yields the following (also well-known) result.

Theorem 6**.**

*For any class $\mathscr{C}$ of graphs of bounded clique-width, $\mathrm{MC}(\mathrm{MSO}_{1},\mathscr{C})$ is fixed-parameter tractable. *

In fact, the result applies to any $\sigma$-structure of bounded clique-width, provided that a clique-expression generating the structure (whose width is bounded by a computable function of the clique-width of the structure) is given or computable in polynomial time.

The next lemma is the main technical ingredient for the proof of Theorem 4 above.

Lemma 1**.**

*There is an algorithm which, on input a graph $G$ of clique-width at most $k$, computes a linear order $<$ on $V(G)$ and a clique-expression of width at most $2^{k+2}$ generating the structure $(G,<)$. *

Proof.

Let $G$ and $k$ be given. Using Theorem 5 we first compute an $\{E\}$-clique-expression $(T,\lambda)$ of width at most $2^{k+1}$ generating $G$. Let $r$ be the root of $T$. For every node $t\in V(T)$ we fix an ordering of its successors. Let $\prec$ be the partial order on $V(T)$ induced by this ordering.

Let $t\in V(T)$ be a node and let $s\neq t$ be the first node on the path $P$ from $t$ to $r$ with $\lambda(s)=\oplus$, if it exists. Let $t_{1},t_{2}$ be the successors of $s$ with $t_{1}\prec t_{2}$. We call $t$ a left node if $t_{1}\in V(P)$, and a right node otherwise. If there is no node labelled $\oplus$ strictly above $t$, then we call $t$ a left node as well.

For every $t\in V(T)$ let $T_{t}$ be the subtree of $T$ with root $t$, and let $\lambda_{|T_{t}}$ be the restriction of $\lambda$ to the subtree $T_{t}$. We recursively define a transformation $\rho(T_{t},\lambda_{|T_{t}})$ on the subtrees of $T$ defined as follows. Intuitively, we produce a new clique-expression $(T^{\prime},\lambda^{\prime})$ over the signature $\{E,<\}$ using colours $\{(i,a),(i,b)\,:\,1\leqslant i\leqslant k\}$. Essentially, the new clique-expression will generate the same graph as $(T,\lambda)$, but so that if $t$ is a node in $T$ and $T_{t}$ generates the graph $G_{t}$, then $T^{\prime}$ contains a node $t^{\prime}$ generating an ordered version $G^{\prime}_{t}\coloneqq(G_{t},<)$ of $G_{t}$ so that if $v\in V(G_{t})$ has colour $i$, then, in $G^{\prime}_{t}$, $v$ has colour $(i,a)$ if $t$ is a left node and $(i,b)$ if $t$ is a right node. Hence, whenever in $T$ we take the disjoint union of $G_{t}$ and $G_{s}$ and $t\prec s$, then we can define the ordering on $G^{\prime}_{t}\mathop{\dot{\cup}}G^{\prime}_{s}$ by adding all edges from nodes in $G^{\prime}_{t}$ to $G^{\prime}_{s}$, i.e. all edges from vertices coloured $(i,a)$ to $(j,b)$ for all pairs $i,j$.

Formally, the transformation is defined as follows.

• •

If $t\in V(T)$ is a leaf, then $\rho(t)\coloneqq(T^{\prime},\lambda^{\prime})$, where $T^{\prime}$ consists only of $t$ and $\lambda^{\prime}(t)\coloneqq(\lambda(t),a)$ if $t$ is a left node, and $\lambda^{\prime}(t)\coloneqq(\lambda(t),b)$ if $t$ is a right node.

• •

Suppose $\lambda(t)=\textup{rename}_{i\to j}$ and let $s$ be the successor of $t$. Then $\rho(T_{t},\lambda_{|T_{t}})\coloneqq(T^{\prime},\lambda^{\prime})$, where $T^{\prime}$ is a tree defined as follows. Let $(T^{\prime\prime},\lambda^{\prime\prime})\coloneqq\rho(T_{s},\lambda_{|T_{s}})$ and let $r^{\prime\prime}$ be the root of $T^{\prime\prime}$. Then $T^{\prime}$ is obtained from $T^{\prime\prime}$ by adding a new root $r^{\prime}$, a new vertex $v$, and new edges $(r^{\prime},v)$ and $(v,r^{\prime\prime})$. We define $\lambda^{\prime}(r^{\prime})\coloneqq\textup{rename}_{(i,a)\to(j,a)}$, $\lambda^{\prime}(v)\coloneqq\textup{rename}_{(i,b)\to(j,b)}$, and $\lambda^{\prime}(u)\coloneqq\lambda^{\prime\prime}(u)$ for $u\in V(T^{\prime\prime})$.

• •

Suppose $\lambda(t)=\textup{edge}_{E,i\to j}$ and let $s$ be the successor of $t$. Then $\rho(T_{t},\lambda_{|T_{t}})\coloneqq(T^{\prime},\lambda^{\prime})$, where $T^{\prime}$ is a tree defined as follows. Let $(T^{\prime\prime},\lambda^{\prime\prime})\coloneqq\rho(T_{s},\lambda_{|T_{s}})$ and let $r^{\prime\prime}$ be the root of $T^{\prime\prime}$. Then $T^{\prime}$ is obtained from $T^{\prime\prime}$ by adding a path $(v_{1},v_{2},v_{3},v_{4})$ of length $3$ and making $r^{\prime\prime}$ a successor of $v_{4}$. We define $\lambda^{\prime}(v_{1})\coloneqq\textup{edge}_{E,(i,a)\to(j,a)}$, $\lambda^{\prime}(v_{2})\coloneqq\textup{edge}_{E,(i,b)\to(j,a)}$, $\lambda^{\prime}(v_{3})\coloneqq\textup{edge}_{E,(i,a)\to(j,b)}$, $\lambda^{\prime}(v_{4})\coloneqq\textup{edge}_{E,(i,b)\to(j,b)}$, and $\lambda^{\prime}(u)\coloneqq\lambda^{\prime\prime}(u)$ for $u\in V(T^{\prime\prime})$.

• •

Finally, suppose $\lambda(t)=\oplus$ and let $t_{1},t_{2}$ be the successors of $t$ such that $t_{1}\prec t_{2}$. Then $\rho(T_{t},\lambda_{|T_{t}})\coloneqq(T^{\prime},\lambda^{\prime})$, where $T^{\prime}$ is a tree defined as follows. For $i=1,2$, let $(T_{i},\lambda_{i})\coloneqq\rho(T_{t_{i}},\lambda_{|T_{t_{i}}})$ and let $r_{i}$ be the root of $T_{i}$. $T^{\prime}$ consists of the union of $T_{1}$ and $T_{2}$, and the additional vertices $v_{i}$, $1\leqslant i\leqslant k$, $w_{i,j}$, $1\leqslant i,j\leqslant k$, and $v_{\oplus}$. We add the edges $(v_{i},v_{i+1})$ for $1\leqslant i<k$, the edges $(w_{i,j},w_{i,j+1})$ for $1\leqslant i\leqslant k$, $1\leqslant j<k$, and the edges $(w_{i,k},w_{i+1,1})$ for $1\leqslant i<k$, and finally the edges $(v_{k},w_{1,1})$, $(w_{k,k},v_{\oplus})$, and $(v_{\oplus},r_{i})$ for $i=1,2$. For every node $s\in V(T_{i})$ we define $\lambda^{\prime}(s)\coloneqq\lambda_{i}(s)$, $i=1,2$. Furthermore, we define $\lambda(v_{\oplus})\coloneqq\oplus$ and $\lambda^{\prime}(w_{i,j})\coloneqq\textup{edge}_{<,(i,a)\to(j,b)}$ for $1\leqslant i,j\leqslant k$. Finally, if $t$ is a left node, then we define $\lambda(v_{i})\coloneqq\textup{rename}_{(i,b)\to(i,a)}$ for $i\leqslant k$, and if $t$ is a right node, then we define $\lambda(v_{i})\coloneqq\textup{rename}_{(i,a)\to(i,b)}$ for $i\leqslant k$.

Now, it is easily seen that $(T^{\prime},\lambda^{\prime})$ generates an $\{E,<\}$-structure $(V,E,<)$ where $(V,E)$ is the graph generated by $(T,\lambda)$ and $<$ is a linear order on $V$. The width of $(T^{\prime},\lambda^{\prime})$ is twice the width of $(T,\lambda)$, and hence at most $2^{k+2}$. $\square$

We are now ready to prove Theorem 4.

Proof (Proof of Theorem 4).

Let $\mathscr{C}$ be a class of graphs of clique-width at most $k$. On input $G\in\mathscr{C}$ and $\varphi\in\mathrm{MSO}_{1}[{<}\mathit{-inv}]$, we apply Lemma 1 to obtain a clique-expression $(T,\lambda)$ of width $2^{k+2}$ generating an ordered copy $(G,<)$ of $G$ in time $f(k)\cdot|G|^{3}$, for some computable function $f$. We can now apply Theorem 6 to decide whether $(G,<)\models\varphi$ in time $g(2^{k+2})\cdot p(|G|)$, where $g$ is a computable function and $p$ a polynomial. As $\varphi$ is order-invariant, if $(G,<)\models\varphi$, then $(G,<^{\prime})\models\varphi$ for any linear order $<^{\prime}$ on $G$. Hence, if $(G,<)\models\varphi$ we can return “yes” and otherwise reject the input. This concludes the proof. $\square$

It is worth pointing out the following feature of the model-checking algorithms established in Theorems 3 and 4. Instead of designing new model-checking algorithms, we reduce the verification of order-invariant $\mathrm{MSO}$ on classes of small treewidth or clique-width to the standard model-checking algorithms for $\mathrm{MSO}$ on classes of (slightly larger) treewidth and clique-width, respectively. The advantage of this approach is that we can reuse existing results on $\mathrm{MSO}$ on such classes of graphs. For instance, in [37] the authors report on a practical implementation of Courcelle’s theorem, i.e. on the implementation of a model-checker for $\mathrm{MSO}_{2}$ on graph classes of bounded treewidth, and obtain astonishing performance results in practical tests. Our technique allows us to reuse this implementation so that with minimal effort it is possible to implement our algorithm on top of the work in [37].

Furthermore, in [22] it is shown that on graph classes $\mathscr{C}$ of bounded treewidth, the set of all satisfying assignments of a given $\mathrm{MSO}$ formula $\varphi(X)$ with free variables in a graph $G\in\mathscr{C}$ can be computed in time linear in the size of the output and the size of $G$. Again we can use the same algorithm to obtain the same result for order-invariant $\mathrm{MSO}$.

5 Successor-invariant FO on classes of bounded expansion

Classes of bounded expansion are classes of uniformly sparse graphs that have very good structural and algorithmic properties. Most notably, these classes admit efficient first-order model-checking, as shown by Dvořák et al. [15]. In this section we are going to lift this result to successor-invariant formulas. Let us give the required definitions first.

Shallow minors and bounded expansion.

A graph $H$ is a minor of $G$, written $H\preccurlyeq G$, if there are pairwise disjoint connected subgraphs $(I_{u})_{u\in V(H)}$ of $G$, called branch sets, such that whenever $uv\in E(H)$, then there are $x_{u}\in I_{u}$ and $x_{v}\in I_{v}$ with $x_{u}x_{v}\in E(G)$. We call the family $(I_{u})_{u\in V(H)}$ a minor model of $H$ in $G$. A graph $H$ is a depth-$r$ minor of $G$, denoted $H\preccurlyeq_{r}G$, if there is a minor model $(I_{u})_{u\in V(H)}$ of $H$ in $G$ such that each subgraph $I_{u}$ has radius at most $r$. For a graph $G$ and $r\in\mathbb{N}$, we write $\nabla_{r}(G)$ for the maximum edge density $|E(H)|/|V(H)|$ of a graph $H\preccurlyeq_{r}G$.

Definition 3**.**

A class of graphs $\mathscr{C}$ has bounded expansion if there is a function $f:\mathbb{N}\to\mathbb{N}$ such that $\nabla_{r}(G)\leqslant f(r)$ for all $r\in\mathbb{N}$ and all $G\in\mathscr{C}$.

Let $\tau$ be a finite and purely relational signature and let $\mathscr{C}$ be a class of $\tau$-structures. We say that $\mathscr{C}$ has bounded expansion if the class $\{G(\mathbb{A})\,:\,\mathbb{A}\in\mathscr{C}\}$ of the Gaifman graphs of the structures from $\mathscr{C}$ has bounded expansion.

Generalised colouring numbers.

We will mainly rely on an alternative characterisation of bounded expansion classes via generalised colouring numbers. Let us fix a graph $G$. By $\Pi(G)$ we denote the set of all linear orderings of $V(G)$. For $L\in\Pi(G)$, we write $u<_{L}v$ if $u$ is smaller than $v$ in $L$, and $u\leqslant_{L}v$ if $u<_{L}v$ or $u=v$.

For $r\in\mathbb{N}$, we say that a vertex $u$ is strongly $r$-reachable from a vertex $v$ with respect to $L$ if $u\leqslant_{L}v$ and there is a path $P$ of length at most $r$ that starts in $v$, ends in $u$, and all whose internal vertices are larger than $v$ in $L$. By $\mathrm{SReach}_{r}[G,L,v]$ we denote the set of vertices that are strongly $r$-reachable from $v$ with respect to $L$. Note that $v\in\mathrm{SReach}_{r}[G,L,v]$ for any vertex $v$.

We define the $r$-colouring number of $G$ with respect to $L$ as

[TABLE]

and the $r$-colouring number of $G$ (sometimes called strong $r$-colouring number) as

[TABLE]

For $r\in\mathbb{N}$ and ordering $L\in\Pi(G)$, the $r$-admissibility $\mathrm{adm}_{r}[G,L,u]$ of a vertex $v$ with respect to $L$ is defined as the maximum size of a family $\mathcal{P}$ of paths that satisfies the following two properties:

• •

each path $P\in\mathcal{P}$ has length at most $r$, starts in $v$, and is either the trivial length-zero path or ends in a vertex $u<_{L}v$ and all its internal vertices are larger than $v$ in $L$;

• •

the paths in $\mathcal{P}$ are pairwise vertex-disjoint, apart from sharing the start vertex $v$.

The $r$-admissibility of $G$ with respect to $L$ is defined similarly to the $r$-colouring number:

[TABLE]

and the $r$-admissibility of $G$ is given by

[TABLE]

The $r$-colouring numbers were introduced by Kierstead and Yang [36], while $r$-admissibility was first studied by Dvořák [14]. It was shown that those parameters are related as follows.

Lemma 2** (Dvořák [14]).**

For any graph $G$, $r\in\mathbb{N}$ and vertex ordering $L\in\Pi(G)$, we have

[TABLE]

(Note that in Dvořák’s work, the reachability sets do not include the starting vertex, hence the above inequality is stated slightly differently in [14].)

As proved by Zhu [60], the generalised colouring numbers are tightly related to densities of low-depth minors, and hence they can be used to characterise classes of bounded expansion.

Theorem 7** (Zhu [60]).**

*A class $\mathscr{C}$ of graphs has bounded expansion if and only if there is a function $f:\mathbb{N}\to\mathbb{N}$ such that $\mathrm{col}_{r}(G)\leqslant f(r)$ for all $r\in\mathbb{N}$ and all $G\in\mathscr{C}$. *

We need to be a bit more precise and use the following lemma.

Lemma 3** (Grohe et al. [30]).**

*For any graph $G$ and $r\in\mathbb{N}$ we have $\mathrm{adm}_{r}(G)\leqslant 6r\cdot(\nabla_{r}(G))^{3}$. *

As shown by Dvořák [14], on classes of bounded expansion one can compute $\mathrm{adm}_{r}(G)$ in linear fixed-parameter time, parameterised by $r$. More precisely, we have the following.

Theorem 8** (Dvořák [14]).**

*Let $\mathscr{C}$ be a class of bounded expansion. Then there is an algorithm that, given a graph $G\in\mathscr{C}$ and $r\in\mathbb{N}$, computes a vertex ordering $L\in\Pi(G)$ with $\mathrm{adm}_{r}(G,L)=\mathrm{adm}_{r}(G)$ in time $f(r)\cdot|V(G)|$, for some computable function $f$. *

We remark that Dvořák states the result in [14] as the existence of a linear-time algorithm for each fixed value of $r$. However, an inspection of the proof reveals that it is actually a single fixed-parameter algorithm that can take $r$ as input. To the best of our knowledge, a similar result for computing $\mathrm{col}_{r}(G)$ is not known, but by Lemma 2 we can use admissibility to obtain an approximation of the $r$-colouring number of a given graph from a class of bounded expansion.

Bounded expansion classes are very robust under local changes, e.g. under taking lexicographic products, as defined below.

Definition 4**.**

Let $G$ and $H$ be graphs. The lexicographic product $G\bullet H$ of $G$ and $H$ is the graph with vertex set $V\coloneqq V(G)\times V(H)$ and edge set

[TABLE]

The following lemma shows that taking lexicographic products preserves the edge density of shallow minors. This was first proved in [44]; the following improved bounds are given in [32].

Lemma 4** (**Har-Peled and Quanrud

[32]).

*For any graph $G$ and $r,t\in\mathbb{N}$ we have $\nabla_{r}(G\bullet K_{t})\leqslant 5t^{2}(r+1)^{2}\nabla_{r}(G)$. *

Bounded expansion classes are also stable under taking shallow minors, as expressed in the following lemma.

Lemma 5** (see Nešetřil and Ossona de Mendez [45, Proposition 4.1]).**

*If $J,H$ and $G$ are graphs and $r,s\in\mathbb{N}$ such that $J$ is a depth-$r$ minor of $H$ and $H$ is a depth-$s$ minor of $G$, then $J$ is a depth-$(2rs+r+s)$-minor of $G$. *

The following lemma is folklore, we provide a proof for completeness.

Lemma 6**.**

*For any graph $G$ and $r\in\mathbb{N}$ we have $\nabla_{r}(G)\leqslant\mathrm{col}_{4r+1}(G)$. *

Proof.

Set $c=\mathrm{col}_{4r+1}(G)$ and let $L$ be a linear order of $V(G)$ for which $\mathrm{col}_{4r+1}(G,L)=c$. Next let $H\preccurlyeq_{r}G$, say with a minor model $(I_{u})_{u\in V(H)}$. We will show that $|E(H)|\leqslant c\cdot|V(H)|$.

For each $u\in V(H)$ let $m_{u}$ be the $<_{L}$-minimal vertex in $I_{u}$. We define a linear order on $V(H)$ by setting $u<v$ if $m_{u}<_{L}m_{v}$. Observe that since each branch set has radius at most $r$ and $m_{u}$ and $m_{v}$ are minimum in their respective branch sets, if $u<v$, there exists a vertex in $I_{u}$ which is strongly $(4r+1)$-reachable from $m_{v}$. Hence, $H$ is $c$-degenerate and can have at most $c\cdot|V(H)|$ edges. $\square$

We are going to prove the following theorem.

Theorem 9**.**

*Let $\tau$ be a finite and purely relational signature and let $\mathscr{C}$ be a class of $\tau$-structures of bounded expansion. Then there exists an algorithm that, given a finite $\tau$-structure $\mathbb{A}\in\mathscr{C}$ and a successor-invariant formula $\varphi\in\mathrm{FO}[+1]$, verifies whether $\mathbb{A}\models_{\mathrm{succ-inv}}\varphi$ in time $f(|\varphi|)\cdot n\cdot\alpha(n)$, where $f$ is a function and $n$ is the size of the universe of $\mathbb{A}$. *

In the language of parameterised complexity, Theorem 9 essentially states that the model-checking problem for successor-invariant first-order formulas is fixed-parameter tractable on classes of finite structures whose underlying Gaifman graph belongs to a fixed class of bounded expansion. There is a minor caveat, though. The formal definition of fixed-parameter tractability, see e.g. [23], requires the function $f$ to be computable, which is not asserted by Theorem 9. In order to have this property, it suffices to assume that the class $\mathscr{C}$ is effectively of bounded expansion. In the characterisation of Theorem 7, this means that there exist a computable function $f:\mathbb{N}\to\mathbb{N}$ such that $\mathrm{col}_{r}(G(\mathbb{A}))\leqslant f(r)$ for each $\mathbb{A}\in\mathscr{C}$. See [31] for a similar discussion regarding model-checking first-order logic on (effectively) nowhere dense classes of graphs.

In principle, our approach follows that of the earlier results on successor-invariant model-checking. As $\varphi$ is successor-invariant, to verify whether $\mathbb{A}\models_{\mathrm{succ-inv}}\varphi$, we may compute an arbitrary successor relation $S$ on $V(\mathbb{A})$, and verify whether $(\mathbb{A},S)\models\varphi$. Of course, we will try to compute a successor relation $S$ so that adding it to $\mathbb{A}$ preserves the structural properties as much as possible, so that model-checking on $(\mathbb{A},S)$ can be done efficiently.

Our construction of such a structure preserving successor relation is based on the above described characterisation of bounded expansion classes by the generalised colouring numbers. As a first step, we show how to define a set $F$ of new edges with the following properties:

• •

$F$ forms a tree on the vertex set $V(G)$ of the input graph $G$,

• •

$F$ has maximum degree at most $3$, and

• •

after adding all the edges of $F$ to $G$, the colouring numbers are still bounded.

In a second step, we construct from the bounded degree spanning tree a successor relation on $V(G)$, again ensuring that the relevant parameters remain bounded.

5.1 Constructing a low-degree spanning tree

In this section we prove the following theorem.

Theorem 10**.**

There exists an algorithm that, given a graph $G$, $r\in\mathbb{N}$, and ordering $L$ of $V(G)$, computes a set of unordered pairs $F\subseteq\binom{V(G)}{2}$ such that the graph $T=(V(G),F)$ is a tree of maximum degree at most $3$ and

[TABLE]

*where $G+F$ is the graph $(V(G),E(G)\cup F)$. The running time of the algorithm is $\mathcal{O}((n+m)\cdot\alpha(m))$, where $m=|E(G)|$ and $n=|V(G)|$. *

The main step towards this goal is the corresponding statement for connected graphs, as expressed in the following lemma.

Lemma 7**.**

There exists an algorithm that, given a connected graph $G$, $r\in\mathbb{N}$, and ordering $L$ of $V(G)$, computes a set of unordered pairs $F\subseteq\binom{V(G)}{2}$ such that the graph $T=(V(G),F)$ is a tree of maximum degree at most $3$ and

[TABLE]

*The running time of the algorithm is $\mathcal{O}((n+m)\cdot\alpha(m))$, where $m=|E(G)|$ and $n=|V(G)|$. *

We first show that Theorem 10 follows easily from Lemma 7.

Proof (Proof of Theorem 10, assuming

Lemma 7).

Let $G$ be a (possibly disconnected) graph, and let $G_{1},\ldots,G_{p}$ be its connected components. For $i=1,\ldots,p$, let $L_{i}$ be the ordering obtained by restricting $L$ to $V(G_{i})$. Obviously $\mathrm{col}_{2r}(G_{i},L_{i})\leqslant\mathrm{col}_{2r}(G,L)$.

Apply the algorithm of Lemma 7 to $G_{i}$ and $L_{i}$, obtaining a set of unordered pairs $F_{i}$ such that $T_{i}=(V(G_{i}),F_{i})$ is a tree of maximum degree at most $3$ and

[TABLE]

For $i=1,\ldots,p$, select a vertex $v_{i}$ of $G_{i}$ with degree at most $1$ in $T_{i}$; since $T_{i}$ is a tree, such a vertex exists. Define

[TABLE]

Obviously we have that $T=(V(G),F)$ is a tree. Observe that it has maximum degree at most $3$. This is because each vertex $v_{i}$ had degree at most $1$ in its corresponding tree $T_{i}$, and hence its degree can grow to at most $3$ after adding edges $v_{i-1}v_{i}$ and $v_{i}v_{i+1}$. By Lemma 7, the construction of each $T_{i}$ takes time $\mathcal{O}((n_{i}+m_{i})\cdot\alpha(m_{i}))$, where $m_{i}=|E(G_{i})|$. It follows that the construction of $T$ takes time $\mathcal{O}((n+m)\cdot\alpha(m))$.

It remains to argue that $\mathrm{adm}_{r}(G+F,L)\leqslant 2+2\mathrm{col}_{2r}(G,L)$. Take any vertex $u$ of $G$, say $u\in V(G_{i})$, and let $\mathcal{P}$ be a set of paths of length at most $r$ that start in $u$, are pairwise vertex-disjoint (apart from $u$), and end in vertices smaller than $u$ in $L$, while internally traversing only vertices larger than $u$ in $L$. Observe that at most two of the paths from $\mathcal{P}$ can use any of the edges from the set $\{v_{1}v_{2},v_{2}v_{3},\ldots,v_{p-1}v_{p}\}$, since any such path has to use either $v_{i-1}v_{i}$ or $v_{i}v_{i+1}$. The remaining paths are entirely contained in $G_{i}+F_{i}$, and hence their number is bounded by $\mathrm{adm}_{r}(G_{i}+F_{i},L_{i})\leqslant 2\mathrm{col}_{2r}(G,L)$. The theorem follows. $\square$

In the remainder of this section we focus on Lemma 7.

Proof (Proof of Lemma 7).

We begin our proof by showing how to compute the set $F$. This will be a two step process, starting with an elimination tree. For a connected graph $G$ and an ordering $L$ of $V(G)$, we define the (rooted) elimination tree $S(G,L)$ of $G$ imposed by $L$ (cf. [3, 54]) as follows. If $V(G)=\{v\}$, then the rooted elimination tree $S(G,L)$ is just the tree on the single vertex $v$. Otherwise, the root of $S(G,L)$ is the vertex $w$ that is the smallest with respect to the ordering $L$ in $G$. For each connected component $C$ of $G-w$ we construct a rooted elimination tree $S(C,L|_{V(C)})$, where $L|_{V(C)}$ denotes the restriction of $L$ to the vertex set of $C$. These rooted elimination trees are attached below $w$ as subtrees by making their roots into children of $w$. Thus, the vertex set of the elimination tree $S(G,L)$ is always equal to the vertex set of $G$. See Figure 2 for an illustration. The solid black lines are the edges of $G$; the dashed blue lines are the edges of $S$. The ordering $L$ is given by the numbers written in the vertices.

Let $S=S(G,L)$ be the rooted elimination tree of $G$ imposed by $L$. For a vertex $u$, by $G_{u}$ we denote the subgraph of $G$ induced by all descendants of $u$ in $S$, including $u$. The following properties follow easily from the construction of a rooted elimination tree.

Claim 1**.**

The following assertions hold.

For each $u\in V(G)$, the subgraph $G_{u}$ is connected. 2. 2.

Whenever a vertex $u$ is an ancestor of a vertex $v$ in $S$, we have $u\leqslant_{L}v$. 3. 3.

For each $uv\in E(G)$ with $u<_{L}v$, $u$ is an ancestor of $v$ in $S$. 4. 4.

For each $u\in V(G)$ and each child $v$ of $u$ in $S$, $u$ has at least one neighbour in $V(G_{v})$.

Proof.

Assertions (1) and (2) follow immediately from the construction of $S$. For assertion (3), suppose that $u$ and $v$ are not bound by the ancestor-descendant relation in $S$, and let $w$ be their lowest common ancestor in $S$. Then $u$ and $v$ would be in different connected components of $G_{w}-w$, hence $uv$ could not be an edge; a contradiction. It follows that $u$ and $v$ are bound by the ancestor-descendant relation, implying that $u$ is an ancestor of $v$, due to $u<_{L}v$ and assertion (2). Finally, for assertion (4), recall that by assertion (1) we have that $G_{u}$ is connected, whereas by construction $G_{v}$ is one of the connected components of $G_{u}-u$. Hence, in $G$ there is no edge between $V(G_{v})$ and any of the other connected components of $G_{u}-u$. If there was no edge between $V(G_{v})$ and $u$ as well, then there would be no edge between $V(G_{v})$ and $V(G_{u})-V(G_{v})$, contradicting the connectivity of $G_{u}$. $\square$

We now define a set of edges $B\subseteq E(G)$ as follows. For every vertex $u$ of $G$ and every child $v$ of $u$ in $S$, select an arbitrary neighbour $w_{u,v}$ of $u$ in $G_{v}$; such a neighbour exists by Claim 1 (4). Then let $B_{u}$ be the set of all edges $uw_{u,v}$, for $v$ ranging over the children of $u$ in $S$. Define

[TABLE]

Let $U$ be the graph spanned by all the edges in $B$, that is, $U=(V(G),B)$. In Figure 2, the edges of $U$ are represented by the dotted red lines.

Claim 2**.**

*The graph $U$ is a tree. *

Proof.

Observe that for each $u\in V(G)$, the number of edges in $B_{u}$ is equal to the number of children of $u$ in $S$. Since every vertex of $G$ has exactly one parent in $S$, apart from the root of $S$, we infer that

[TABLE]

Therefore, since $B$ is the edge set of $U$, to prove that $U$ is a tree it suffices to prove that $U$ is connected. To this end, we prove by a bottom-up induction on $S$ that for each $u\in V(G)$, the subgraph U_{u}=\bigl{(}V(G_{u}),B\cap\binom{V(G_{u})}{2}\bigr{)} is connected. Note that for the root $w$ of $S$ this claim is equivalent to $U_{w}=U$ being connected.

Take any $u\in V(G)$, and suppose by induction that for each child $v$ of $u$ in $S$, the subgraph $U_{v}$ is connected. Observe that $U_{u}$ can be constructed by taking the vertex $u$ and, for each child $v$ of $u$ in $S$, adding the connected subgraph $U_{v}$ and connecting $U_{v}$ to $u$ via the edge $uw_{u,v}\in B_{u}$. Thus, $U_{u}$ constructed in this manner is also connected, as claimed. $\square$

Next, we verify that $U$ can be computed within the claimed running time. Note that we do not need to compute $S$, as we use it only in the analysis. We remark that this is the only place in the algorithm where the running time is not linear.

Claim 3**.**

*The tree $U$ can be computed in time $\mathcal{O}(m\cdot\alpha(m))$. *

Proof.

We use the classic Union & Find data structure on the set $V(G)$. Recall that in this data structure, at each moment we maintain a partition of $V(G)$ into a number of equivalence classes, each with a prescribed representative, where initially each vertex is in its own class. The operations are a) for a given $u\in V(G)$, find the representative of the class to which $u$ belongs, and b) merge two equivalence classes into one. Tarjan [58] gave an implementation of this data structure where both operations run in amortised time $\alpha(k)$, where $k$ is the total number of operations performed.

Having initialised the data structure, we process the vertex ordering $L$ from the smallest end, starting with an empty prefix. For an already processed prefix $X$ of $L$, the maintained classes within $X$ will represent the partition of $G[X]$ into connected components, while every vertex outside $X$ will still be in its own equivalence class. Let us consider one step, when we process a vertex $u$, thus moving from a prefix $X$ to the prefix $X^{\prime}=X\cup\{u\}$. Iterate through all the neighbours of $u$, and for each neighbour $v$ of $u$ such that $u<_{L}v$, verify whether the equivalence classes of $u$ and $v$ are different. If this is the case, merge these classes and add the edge $uv$ to $B$. A straightforward induction shows that the claimed invariant holds. Moreover, when processing $u$ we add exactly the edges of $B_{u}$ to $B$, hence at the end we obtain the set $B$ and the tree $U=(V(G),B)$.

For the running time analysis, observe that in total we perform $\mathcal{O}(m)$ operations on the data structure, thus the running time is $\mathcal{O}(m\alpha(m))$. We remark that we assume that the ordering $L$ is given as a bijection between $V(G)$ and numbers $\{1,2,\ldots,|V(G)|\}$, thus for two vertices $u,v$ we can check in constant time whether $u<_{L}v$. $\square$

By Lemma 2 we have that $U$ is a spanning tree of $G$. However its maximum degree may be too large. The idea is to use $U$ to construct a new tree $T$ with maximum degree at most $3$ (on the same vertex set $V(G)$). The way we constructed $U$ will enable us to argue that adding the edges of $T$ to the graph $G$ does not change the generalised colouring numbers too much.

Give $U$ the same root as the elimination tree $S$. From now on we treat $U$ as a rooted tree, which imposes parent-child and ancestor-descendant relations in $U$ as well. Note that the parent-child and ancestor-descendant relations in $S$ and in $U$ may be completely different. For instance, consider vertices $4$ and $15$ in the example from Figure 2: $4$ is a child of $15$ in $U$, and an ancestor of $15$ in $S$.

For every $u\in V(G)$, let $(x_{1},\ldots,x_{p})$ be an enumeration of the children of $u$ in $U$, such that $x_{i}<_{L}x_{j}$ if $i<j$. Let $F_{u}=\{ux_{1},x_{1}x_{2},x_{2}x_{3},\ldots,x_{p-1}x_{p}\}$, and define

[TABLE]

See Figure 3 for an illustration.

Claim 4**.**

*The graph $T$ is a tree with maximum degree at most $3$. *

Proof.

Observe that for each $u\in V(G)$ we have that $|F_{u}|$ is equal to the number of children of $u$ in $U$. Every vertex of $G$ apart from the root of $U$ has exactly one parent in $U$, hence

[TABLE]

Therefore, to prove that $T$ is a tree, it suffices to argue that it is connected. This, however, follows immediately from the fact that $U$ is connected, since for each edge in $U$ there is a path in $T$ that connects the same pair of vertices.

Finally, it is easy to see that each vertex $u$ is incident to at most $3$ edges of $F$: at most one leading to a child of $u$ in $U$, and at most $2$ belonging to $F_{v}$, where $v$ is the parent of $u$ in $U$. $\square$

Observe that once the tree $U$ is constructed, it is straightforward to construct $T$ in time $\mathcal{O}(n)$. Thus, it remains to check that adding $F$ to $G$ does not change the generalised colouring numbers too much.

Take any vertex $u\in V(G)$ and examine its children in $U$. We partition them as follows. Let $Z^{\uparrow}_{u}$ be the set of those children of $u$ in $U$ that are its ancestors in $S$, and let $Z^{\downarrow}_{u}$ be the set of those children of $u$ in $U$ that are its descendants in $S$. By the construction of $U$ and by Claim 1.3, each child of $u$ in $U$ is either its ancestor or descendant in $S$. By Claim 1.2, this is equivalent to saying that $Z^{\uparrow}_{u}$, respectively $Z^{\downarrow}_{u}$, comprise the children of $u$ in $U$ that are smaller, respectively larger, than $u$ in $L$. Note that by the construction of $U$, the vertices of $Z^{\downarrow}_{u}$ lie in pairwise different subtrees rooted at the children of $u$ in $S$, thus $u$ is the lowest common ancestor in $S$ of every pair of vertices from $Z^{\downarrow}_{u}$. On the other hand, all vertices of $Z^{\uparrow}_{u}$ are ancestors of $u$ in $S$, thus every pair of them is bound by the ancestor-descendant relation in $S$.

Claim 5**.**

*The graph union $G+F$ satisfies $\mathrm{adm}_{r}(G+F,L)\leqslant 2\cdot\mathrm{col}_{2r}(G,L)$. *

Proof.

Write $H=G+F$. Let $F_{\textrm{new}}=F-E(G)$ be the set of edges from $F$ that were not already present in $G$. If an edge $e\in F_{\textrm{new}}$ belongs also to $F_{u}$ for some $u\in V(G)$, then we know that $u$ cannot be an endpoint of $e$. This is because edges joining a vertex $u$ with its children in $U$ were already present in $G$. We say that the vertex $u$ is the origin of an edge $e\in F_{\textrm{new}}\cap F_{u}$, and denote it by $a(e)$. Observe that $a(e)$ is adjacent to both endpoints of $e$ in $G$ by construction. Also observe that if the endpoints of $e$ belong to $Z^{\uparrow}_{a(e)}$, then they are both ancestors of $a(e)$ in $S$, and thus are both smaller than $a(e)$ in $L$. Otherwise, if the endpoints of $e$ belong to $Z^{\downarrow}_{a(e)}$, then they are not bound by the ancestor-descendant relation in $S$ and $a(e)$ is their lowest common ancestor in $S$.

To give an upper bound on $\mathrm{adm}_{r}(H,L)$, let us fix a vertex $u\in V(G)$ and a family of paths $\mathcal{P}$ in $H$ such that

• •

each path in $\mathcal{P}$ has length at most $r$, starts in $u$, ends in a vertex smaller than $u$ in $L$, and all its internal vertices are larger than $u$ in $L$;

• •

the paths in $\mathcal{P}$ are pairwise vertex-disjoint, apart from the starting vertex $u$.

For each path $P\in\mathcal{P}$, we define a walk $P^{\prime}$ in $G$ as follows. For every edge $e=xy$ from $F_{\textrm{new}}$ traversed on $P$, replace the usage of this edge on $P$ by the following detour of length $2$: $x{-}a(e){-}y$. Observe that $P^{\prime}$ is a walk in the graph $G$, it starts in $u$, ends in the same vertex as $P$, and has length at most $2r$. Next, we define $v(P)$ to be the first vertex on $P^{\prime}$ (that is, the closest to $u$ on $P^{\prime}$) that does not belong to $G_{u}$. Since the endpoint of $P^{\prime}$ that is not $u$ does not belong to $G_{u}$, such a vertex exists. Finally, let $P^{\prime\prime}$ be the prefix of $P^{\prime}$ from $u$ to the first visit of $v(P)$ on $P^{\prime}$ (from the side of $u$). Observe that the predecessor of $v(P)$ on $P^{\prime\prime}$ belongs to $G_{u}$ and is a neighbour of $v(P)$ in $G$, hence $v(P)$ has to be a strict ancestor of $u$ in $S$. We find that $P^{\prime\prime}$ is a walk of length at most $2r$ in $G$, it starts in $u$, ends in $v(P)$, and all its internal vertices belong to $G_{u}$, so in particular they are not smaller than $u$ in $L$. This means that $P^{\prime\prime}$ certifies that $v(P)\in\mathrm{SReach}_{2r}[G,L,u]$.

Since \bigl{|}\mathrm{SReach}_{2r}[G,L,u]\bigr{|}\leqslant\mathrm{col}_{2r}(G,L), in order to prove the bound on $\mathrm{adm}_{r}(H,L)$, it suffices to prove the following claim: For each vertex $v$ that is a strict ancestor of $u$ in $S$, there can be at most two paths $P\in\mathcal{P}$ for which $v=v(P)$. To this end, we fix a vertex $v$ that is a strict ancestor of $u$ in $S$ and proceed by a case distinction on how a path $P$ with $v=v(P)$ may behave.

Suppose first that $v$ is the endpoint of $P$ other than $u$, equivalently the endpoint of $P^{\prime}$ other than $u$. (For example, $u=1$, $P=1,11,21,0$, $P^{\prime}=1,11,1,21,0$ and $v=0$, in figures 2 and 3.) However, the paths of $\mathcal{P}$ are pairwise vertex-disjoint, apart from the starting vertex $u$, hence there can be at most one path $P$ from $\mathcal{P}$ for which $v$ is an endpoint. Thus, this case contributes at most one path $P$ for which $v=v(P)$.

Next suppose that $v$ is an internal vertex of the walk $P^{\prime}$; in particular, it is not the endpoint of $P$ other than $u$. (For example, $u=6$, $P=6,11,21,0$, $P^{\prime}=6,11,1,21,0$ and $v=1$, in figures 2 and 3.) Since the only vertex traversed by $P$ that is smaller than $u$ in $L$ is this other endpoint of $P$, and $v$ is smaller than $u$ in $L$ due to being its strict ancestor in $S$, it follows that each visit of $v$ on $P^{\prime}$ is due to having $v=a(e)$ for some edge $e\in F_{\textrm{new}}$ traversed on $P$. Select $e$ to be such an edge corresponding to the first visit of $v$ on $P^{\prime}$. Let $e=xy$, where $x$ lies closer to $u$ on $P$ than $y$. (That is, in our figures, $x=11$ and $y=21$.) Since $v$ was chosen as the first vertex on $P^{\prime}$ that does not belong to $G_{u}$, we have $x\in G_{u}$.

Since $v=a(e)=a(xy)$, either $x\in Z^{\downarrow}_{v}$ or $x\in Z^{\uparrow}_{v}$. Note that the second possibility cannot happen, because then $v$ would be a descendant of $x$ in $S$, hence $v$ would belong to $G_{u}$, due to $x\in G_{u}$; a contradiction. We infer that $x\in Z^{\downarrow}_{v}$.

Recall that, by construction, $Z^{\downarrow}_{v}$ contains at most one vertex from each subtree of $S$ rooted at a child of $v$. Since $v$ is a strict ancestor of $u$ in $S$, we infer that $x$ has to be the unique vertex of $Z^{\downarrow}_{v}$ that belongs to $G_{u}$. In the construction of $F_{v}$, however, we added only at most two edges of $F_{v}$ incident to this unique vertex: at most one to its predecessor on the enumeration of the children of $v$, and at most one to its successor. Since paths from $\mathcal{P}$ are pairwise vertex-disjoint in $H$, apart from the starting vertex $u$, only at most one path from $\mathcal{P}$ can use these two edges. We can have $v=a(e)$ for this path only. Thus, this case contributes at most one path $P$ for which $v=v(P)$, completing the proof of the claim. $\square$

We conclude the proof by summarising the algorithm: first construct the tree $U$, and then construct the tree $T$. As argued, these steps take time $\mathcal{O}(m\cdot\alpha(m))$ and $\mathcal{O}(n)$, respectively. By claims 4 and 5, $T$ satisfies the required properties. $\square$

5.2 Constructing a successor relation

The preceding section provides us with a spanning tree of maximum degree at most $3$. We now show how this can be used to obtain a successor relation from this spanning tree.

We give two constructions: One which constructs an actual successor relation, at the cost of possibly adding further edges. The added edges may increase the admissibility, but in a way that preserves bounded expansion. We also give a second construction that does not add additional edges and hence preserves also other structural properties. Such a construction may thus be potentially used for model-checking on other graph classes. This construction shows how a successor relation may be first-order interpreted in a graph with bounded-degree spanning tree, without adding any edges.

Adding a successor relation.

Theorem 11**.**

There exists an algorithm that, given a graph $G$, $r\in\mathbb{N}$, the edge set $F$ of a tree of maximum degree at most $3$, and an ordering $L$ of $V(G)$, computes a set of ordered pairs $S\subseteq V(G)^{2}$ such that $S$ is a successor relation on $V(G)$ and

[TABLE]

*for an appropriately defined function $h$ where $\bar{S}=\left\{\{a,b\}\,:\,(a,b)\in S,a\neq b\right\}$. The running time of the algorithm is $\mathcal{O}(m+n)$, where $m=|E(G)|$ and $n=|V(G)|$. *

As observed e.g. in [35, 56], the cube of every connected graph contains a Hamiltonian path. (The cube of a graph $G$ is the graph on the same vertex set as $G$ and in which two vertices are connected if their distance in $G$ is at most $3$.) Furthermore, such a Hamiltonian path can be computed in linear time in the size of the original graph [42]. The set $S$ of edges whose existence is stated in Theorem 11 will simply be the Hamiltonian path computed in the cube of the spanning tree $F$ that we constructed above. It remains to prove the claimed bound on the $r$-admissibility of the new graph.

Proof (Proof of Theorem 11).

Observe that we can find $G+S$, where $S$ is as described above, as a depth-$3$ minor of $(G+F)\bullet K_{9}$. This is a simple consequence of the fact that $F$ has maximum degree $3$. Now we have

[TABLE]

Finally, by Lemma 3 we have $\mathrm{adm}_{r}(G+S)\leqslant 6r(\nabla_{r}(G+S))^{3}$, which gives us \mathrm{adm}_{r}(G+S)\leqslant g\bigl{(}r,\mathrm{col}_{40r+1}(G+F)\bigr{)}, for an appropriately defined function $g$. We have $\mathrm{col}_{40r+1}(G+F)\leqslant\mathrm{adm}_{40r+1}(G+F)^{40r+1}$ by Lemma 2, which leads to the stated result. $\square$

Interpreting a successor relation.

We show how in a graph with a spanning tree of degree $3$, a successor relation can be interpreted after suitably colouring vertices and edges, but without adding further edges. We first notice that existence of such a spanning tree guarantees the existence of a $3$-walk, i.e. a walk through the graph that visits each vertex at least once and at most three times. The following lemma allows us to interpret a successor relation from a $k$-walk in first-order logic, for arbitrary $k$. For a natural number $\ell$, let $[\ell]$ be the set $\{1,\ldots,\ell\}$.

Lemma 8**.**

Let $\sigma$ be a finite relational signature, $\mathbb{A}$ a finite $\sigma$-structure, and $w:[n]\to V(\mathbb{A})$ a $k$-walk through the Gaifman graph of $\mathbb{A}$, where $n\coloneqq|V(\mathbb{A})|$. Then there is a finite relational signature $\sigma_{k}$ and a first-order formula $\varphi^{(k)}_{\mathrm{succ}}(x,y)$, both depending only on $k$, and a $(\sigma\cup\sigma_{k})$-expansion $\mathbb{A}^{\prime}$ of $\mathbb{A}$ which can be computed from $\mathbb{A}$ and $w$ in polynomial time, such that

• •

the Gaifman-graphs of $\mathbb{A}^{\prime}$ and $\mathbb{A}$ are the same;

• •

$\varphi^{(k)}_{\mathrm{succ}}$* defines a successor relation on $\mathbb{A}^{\prime}$.*

Proof.

We define a function $f:[n]\to[k]$ which counts how many times we have visited a vertex on the walk before, by

[TABLE]

Furthermore, let $F:V(\mathbb{A})\to[k]$ count how many times we visit a vertex:

[TABLE]

To simplify notation, if $i\in[n]$ we write $F(i)$ for $F(w(i))$.

We encode the $k$-walk $w$ by binary relations $E_{ab}$ with $a,b=1,\ldots,k$, in such a way that $(u,v)\in E_{ab}$ if and only if there is some $i\in[n-1]$ such that

• •

$w(i)=u$ and $f(i)=a$, and

• •

$w(i+1)=v$ and $f(i+1)=b$.

That is, after visiting $u$ for the $a$-th time, the walk $w$ proceeds to $v$, visiting it for the $b$-th time. Note that if $k=1$, we can immediately define a successor relation by

[TABLE]

If $k>1$, we show how to interpret a $(k-1)$-walk $w^{\prime}$ in first-order logic, given a $k$-walk encoded by $\{E_{ab}\,:\,1\leqslant a,b\leqslant k\}$ as above. By daisy-chaining these interpretations we end up with a $1$-walk (i.e. a Hamiltonian path). Plugging in the interpretation of this Hamiltonian path into $\varphi^{(1)}_{\mathrm{succ}}$ defined above gives the formulas $\varphi^{(k)}_{\mathrm{succ}}$.

In order to get from a $k$-walk to a $(k-1)$-walk, we look at all vertices that are visited $k$ times, and “jump” over these vertices, either when they are visited for the $(k-1)$-th or for the $k$-th time. Jumping over a vertex can be done in first-order logic, but we must be careful to choose the vertices for jumping in such a way that we never jump over an unbounded number of vertices in a row, as this is not possible in first-order logic. We encode the information on whether to jump when visiting for the $(k-1)$-th or the $k$-th time in a new unary predicate $P_{k}$.

To be precise, let \varphi_{\text{k-times}}(x) be a formula which states that $x$ is visited $k$ times:

[TABLE]

For those $u\in V(\mathbb{A})$ which are visited $k$-times, we agree to jump over them when they are visited for the $k$-th time if $u\in P_{k}$, and when they are visited for the $(k-1)$-th time otherwise. Thus, if $w(i)=u$, $f(i)=k$ and $u\in P_{k}$, we want to remove the $i$-th step. However, it may be the case that $w(i+1)$ is also visited $k$ times and needs to be jumped over. We define first-order formulas which carry out a bounded number of such jumps as follows.

• •

For $a\in[k]$, the formula $\varphi_{\text{jump},a}(x)$ holds if we jump over $x$ when visiting it for the $a$-th time:

[TABLE]

• •

For $r\geqslant 0$ and $a,b\in[k]$, the formula $\varphi_{\text{next},a,b}^{(r)}(x,y)$ holds if, when applying at most $r$ consecutive jumps on entering $x$ for the $a$-th time, we end up in node $y$ which is visited for the $b$-th time in the (original) walk. Specifically:

[TABLE]

Here, $\delta_{ab}$ is true if the indices $a$ and $b$ are the same:

[TABLE]

• •

We will show below how to choose the predicate $P_{k}$ so that we never need to take more than two consecutive jumps. Thus, we can interpret a $(k-1)$-walk $w^{\prime}$ using, for $a,b\in[k-2]$, the formulas

[TABLE]

For $a\in[k-2]$ we set

[TABLE]

Next, for $b\in[k-2]$ we set

[TABLE]

and finally we define

[TABLE]

To define the predicate $P_{k}$, let $T\subseteq[n]$ be the set of indices $i\in[n]$ for which $F(i)=k$ and $f(i)\in\{k-1,k\}$. We obtain a perfect matching $M$ on $T$ by matching $i$ and $j$ if and only if $w(i)=w(j)$ (cf. Figure 4 (a)). We define a subset $J\subseteq[n]$ with the intended meaning that if $i\in J$, we jump over the $i$-th step of $w$. The set $J$ will satisfy the following two conditions:

• •

every vertex $v$ with $F(v)=k$ is jumped over exactly once, i.e.

[TABLE]

• •

we never jump more than twice in a row, i.e. if $i,i+1\in J$, then $i+2\not\in J$.

We partition the set $[n]$ into intervals of size $2$, setting

[TABLE]

with the last set $\{n\}$ being a singleton if $n$ is odd. Then the matching $M$ defines a multigraph without loops on $U$, and the degree of $I\in U$ is at most 2. We direct the edges of $M$, viewed as edges in the multigraph $(U,M)$, in such a way that every $I\in U$ has at most one incoming edge. The edges incident with $I$ correspond to the elements of $I\cap T$, and we put $i\in I$ into $J$ if and only if the edge corresponding to $i$ is directed towards $I$ (cf. Figure 4 (b)). For every k=1,\ldots,\bigl{\lfloor}\frac{1}{2}(n-1)\bigr{\rfloor} at most one of $2k-1$ and $2k$ is in $J$, and therefore $J$ satisfies the above requirements.

The definition of $P_{k}\subseteq V(G)$ is now straightforward:

[TABLE]

In summary, we end up with

[TABLE]

and it is clear that our construction can be carried out in polynomial time. $\square$

5.3 Proof of Theorem 9

Let us finally derive the main theorem, Theorem 9. We first need to draw upon the literature on model-checking first-order logic on classes of bounded expansion. The following statement encapsulates the model-checking results of Dvořák et al. [15] and of Grohe and Kreutzer [29]. We also refer to the new expositions given in [27, 49].

Theorem 12**.**

*Let $\tau$ be a finite and purely relational signature. Then for every formula $\varphi\in\mathrm{FO}[\tau]$ there exists a nonnegative integer $r(\varphi)$, computable from $\varphi$, such that the following holds. Given a $\tau$-structure $\mathbb{A}$, it can be verified whether $\mathbb{A}\models\varphi$ in time f\bigl{(}|\varphi|,\mathrm{adm}_{r(\varphi)}(G(\mathbb{A}))\bigr{)}\cdot n, where $n$ is the size of the universe of $\mathbb{A}$ and $f$ is a computable function. *

Observe that if $\mathbb{A}$ is drawn from a fixed class of bounded expansion $\mathscr{C}$, then $\mathrm{adm}_{r(\varphi)}(G(\mathbb{A}))$ is a parameter depending only on $\varphi$, hence we recover fixed-parameter tractability of model-checking for $\mathrm{FO}$ on any class of bounded expansion, parameterised by the length of the formula. Theorem 12 is stronger than this latter statement in that it says that the input structure does not need to be drawn from a fixed class of bounded expansion, where the colouring number is bounded in terms of the radius $r$ for all values of $r$, but it suffices to have a bound on the colouring numbers up to some radius $r(\varphi)$, which depends only on the formula $\varphi$. We need this strengthening in our algorithm for the following reason. When adding a low-degree spanning tree to the Gaifman graph, we are not able to control all the colouring numbers at once, but only for some particular value of the radius. Theorem 12 ensures that this is sufficient for the model-checking problem to remain tractable.

We now sketch how Theorem 12 may be derived from the works of Dvořák et al. [15] and of Grohe and Kreutzer [29]. We prefer to work with the algorithm of Grohe and Kreutzer [29], because we find it conceptually simpler. For a given quantifier rank $q$ and an nonnegative integer $i\leqslant q$, the algorithm computes the set of all types $\mathfrak{R}_{i}^{q}$ realised by $i$-tuples in the input structure $\mathbb{A}$: for a given $i$-tuple of elements $\overline{a}$, its type is the set of all $\mathrm{FO}$ formulas $\varphi(\overline{x})$ with $i$ free variables and quantifier rank at most $q-i$ for which $\varphi(\overline{a})$ holds. Note that for $i=0$ this corresponds to the set of sentences of quantifier rank at most $q$ that hold in the structure, from which the answer to the model-checking problem can be directly read; whereas for $i=q$ we consider quantifier-free formulas with $q$ free variables. Essentially, $\mathfrak{R}_{q}^{q}$ is computed explicitly, and then one inductively computes $\mathfrak{R}_{i}^{q}$ based on $\mathfrak{R}_{i+1}^{q}$. The above description is, however, a bit too simplified, as each step of the inductive computation introduces new relations to the structure, but does not change its Gaifman graph. We will explain this later.

When implementing the above strategy, the assumption that the structure is drawn from a class of bounded expansion is used via treedepth-$p$ colourings, a colouring notion functionally equivalent to the generalised colouring numbers. More precisely, a treedepth-$p$ colouring of a graph $G$ is a colouring $\gamma:V(G)\to\Gamma$, where $\Gamma$ is a set of colours, such that for any subset $C\subseteq\Gamma$ of $i$ colours, $i\leqslant p$, the vertices with colours from $C$ induce a subgraph of treedepth at most $i$. The treedepth-$p$ chromatic number of a graph $G$, denoted $\chi_{p}(G)$, is the smallest number of colours $|\Gamma|$ needed for a treedepth-$p$ colouring of $G$. As proved by Zhu [60], the treedepth-$p$ chromatic numbers are bounded in terms of $r$-colouring numbers as follows.

Theorem 13** (Zhu [60]).**

For any graph $G$ and $p\in\mathbb{N}$ we have

[TABLE]

Moreover, an appropriate treedepth-$p$ colouring can be constructed in polynomial time from an ordering $L\in\Pi(G)$, certifying an upper bound on $\mathrm{col}_{2^{p-2}}(G)$.

The computation of both $\mathfrak{R}_{q}^{q}$ and $\mathfrak{R}_{i}^{q}$ from $\mathfrak{R}_{i+1}^{q}$ is done by rewriting every possible type as a purely existential formula. Each rewriting step, however, enriches the signature by unary relations corresponding to colours of some treedepth-$p$ colouring $\gamma$, as well as binary relations representing edges of appropriate treedepth decompositions certifying that $\gamma$ is correct. However, the binary relations are added in a way that the Gaifman graph of the structure remains intact. For us it is important that in all the steps, the parameter $p$ used for the definition of $\gamma$ depends only on $q$ and $i$ in a computable manner. Thus, by Theorem 13, to ensure that $\gamma$ uses a bounded number of colours, we only need to ensure the boundedness of $\mathrm{col}_{r(q)}(G(\mathbb{A}))$ for some computable function $r(q)$. By taking $q$ to be the quantifier rank of the input formula, the statement of Theorem 12 follows.

We can now combine all the ingredients and show how our main result follows from Theorem 11.

Proof (Proof of Theorem 9).

Given a successor-invariant formula $\varphi\in\mathrm{FO}[\tau\cup\{S\}]$, we first compute the integer $r\coloneqq r(\varphi)$ whose existence and computability is stated in Theorem 12. Given the structure $\mathbb{A}$, we now use the algorithm of Theorem 8 to compute an order $L$ of the vertex set $V(\mathbb{A})$ of the Gaifman graph of $\mathbb{A}$, which satisfies $\mathrm{adm}_{80r+2}(G(\mathbb{A}))\leqslant c(r)$ for some constant $c(r)$. Such constant exists by the assumption that $\mathbb{A}$ is from a class of bounded expansion. We use the algorithm of Theorem 10 to compute a set of unordered pairs $F\subseteq\binom{V(\mathbb{A})}{2}$ such that the graph $T=(V(\mathbb{A}),F)$ is a tree of maximum degree at most $3$ and

[TABLE]

By Lemma 2 we find $\mathrm{col}_{80r+2}(G(\mathbb{A}),L)\leqslant\mathrm{adm}_{80r+2}(G(\mathbb{A}),L)^{80r+2}\leqslant c(r)^{80r+2}$. This means that $\mathrm{adm}_{40r+1}(G(\mathbb{A})+F,L)\leqslant g(r)$ for $g(r)=2+2c(r)^{80r+2}$. Now, using the algorithm of Theorem 11 we compute a successor relation $S$ such that

[TABLE]

where $h$ is the function from Theorem 11. Finally, we apply the algorithm of Theorem 12 to decide whether $(\mathbb{A},S)\models\varphi$ in time f\bigl{(}|\varphi|,\mathrm{adm}_{r}(G(\mathbb{A})+S)\bigr{)}\cdot n. Since $\mathbb{A}$ is drawn from a fixed class of bounded expansion $\mathscr{C}$, $\mathrm{adm}_{r}(G(\mathbb{A})+S)$ is a parameter depending only on $\varphi$. This finishes the proof of the theorem. $\square$

6 Dense Graphs

While model-checking for first-order logic has been studied rather thoroughly for sparse graph classes, few results are known for dense graphs.

• •

On classes of graphs with bounded clique-width (or, equivalently, bounded rank-width; cf. [48]), model-checking even for monadic second-order logic has been shown to be fixed-parameter tractable by Courcelle et al. [9].

• •

More recently, model-checking on coloured posets of bounded width has been shown to be in fixed-parameter tractable for existential $\mathrm{FO}$ by Bova et al. [4] and for all of $\mathrm{FO}$ by Gajarský et al. [26].

Both of these results extend to order-invariant $\mathrm{FO}$, and therefore also to successor-invariant $\mathrm{FO}$. For bounded clique-width, this has already been shown in Section 4 . For posets of bounded width we give a proof here. We first review the necessary definitions.

Definition 5**.**

A partially ordered set (poset) $(P,\leqslant^{P})$ is a set $P$ with a reflexive, transitive and antisymmetric binary relation $\leqslant^{P}$. A chain $C\subseteq P$ is a totally ordered subset, i.e. for all $x,y\in C$ one of $x\leqslant^{P}y$ and $y\leqslant^{P}x$ holds. An antichain is a set $A\subseteq P$ such that if $x\leqslant^{P}y$ for $x,y\in A$, then $x=y$. The width of $(P,\leqslant^{P})$ is the maximal size $|A|$ of an antichain $A\subseteq P$.

A coloured poset is a poset $(P,\leqslant^{P})$ together with a function $\lambda:P\to\Lambda$ mapping $P$ to some set $\Lambda$ of colours.

By $|P|$ we denote the length of a suitable encoding of $(P,\leqslant^{P})$.

We will need Dilworth’s Theorem, which relates the width of a poset to the minimum number of chains needed to cover the poset.

Theorem 14** (Dilworth’s Theorem).**

*Let $(P,\leqslant^{P})$ be a poset. Then the width of $(P,\leqslant^{P})$ is equal to the minimum number $k$ of disjoint chains $C_{i},\ldots,C_{k}\subseteq P$ needed to cover $P$, i.e. such that $\bigcup_{i}C_{i}=P$. *

A proof can be found e.g. in [12, Sec. 2.5]. Moreover, by a result of Felsner et al. [21], both the width $w$ and a set of chains $C_{1},\ldots,C_{w}$ covering $P$ can be computed from $(P,\leqslant_{P})$ in time $O(w\cdot|P|)$.

With this, we are ready to prove the following.

Theorem 15**.**

*There is an algorithm which, on input a coloured poset $(P,\leqslant^{P})$ with colouring $\lambda:P\to\Lambda$ and an order-invariant first-order formula $\varphi$, checks whether $P\models\varphi$ in time $f(w,|\varphi|)\cdot|P|^{2}$ where $w$ is the width of $(P,\leqslant^{P})$. *

Proof.

Using the algorithm of [21], we compute a chain cover $C_{1},\ldots,C_{w}$ of $(P,\leqslant^{P})$. To obtain a linear order on $P$, we just need to arrange the chains in a suitable order, which can be done by colouring the vertices with colours $\Lambda\times[w]$ via

[TABLE]

Then

[TABLE]

defines a linear order on $(P,\leqslant_{P})$ with colouring $\lambda^{\prime}$. After substituting $\varphi_{\leqslant}$ for $\leqslant$ in $\varphi$, we may apply the algorithm of Gajarský et al. [26] to check whether $P\models\varphi$. $\square$