We introduce a new data structure for answering
connectivity queries in undirected graphs subject to batched vertex
failures. Precisely, given any graph $G$ and integer parameter $k$,
we can in fixed-parameter time construct a data structure that can
later be used to answer queries of the form: “are vertices $s$
and $t$ connected via a path that avoids vertices
$u_1,\ldots, u_k$?” in time $\smash{2^{2^{\Oh(k)}}}$. In the terminology of
the literature on data structures, this gives the first
deterministic data structure for
connectivity under vertex failures where for every fixed number of
failures, all operations can be performed in constant time.

With the aim to understand the power and the limitations of our new
techniques, we prove an algorithmic meta theorem for the recently
introduced separator logic, which extends first-order logic
with atoms for connectivity under vertex failures. We prove that the
model-checking problem for separator logic is fixed-parameter
tractable on every class of graphs that exclude a fixed topological
minor. We also show a weak converse.

This implies that from the point of view of
parameterized complexity, under standard complexity theoretical
assumptions, the frontier of tractability of separator logic is
almost exactly delimited by classes excluding a fixed topological

The backbone of our proof relies on a decomposition theorem of Cygan,
Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19],
which provides a tree decomposition of a given
graph into bags that are unbreakable. Crucially, unbreakability
allows to reduce separator logic to plain first-order logic within
each bag individually. Guided by this observation, we design our
model-checking algorithm using dynamic programming over the tree
decomposition, where the transition at each bag amounts to running a
suitable model-checking subprocedure for plain first-order
logic. This approach is robust enough to provide also an extension
to efficient enumeration of answers to a query expressed in
separator logic.

§ INTRODUCTION

§.§ Connectivity under vertex failures

In many applications, we do not need to answer a query once but rather
need to repeatedly answer queries over dynamically changing data. A
prime example are databases, where a database is repeatedly modified
and queried by the users.  In most cases, the modifications to the
database can be expected to be small compared to its size, which
suggests that in a preprocessing step, we can set up a data structure
that is efficiently updated after each modification and that allows
for efficient querying.  In 1997, Frigioni and Italiano introduced the
dynamic subgraph model [20], which
allows to conveniently model such dynamic situations in the particular
case of connectivity in network infrastructures that are subject to
node or link failures.  This model, which has been studied intensively
in the data structures community under the name of
connectivity oracles under vertex failures, is as
follows. We are given a
graph $G$ and an integer $k$. We imagine that $G$ is a network in
which at every moment, at most $k$ vertices (or edges) are inactive
(are subject to failures). The goal is to construct a data
structure that supports the following two operations. First, one can
update $G$ by resetting the set of failed vertices to a given
set of size at most $k$. Second, one can query $G$ by asking,
for a given pair of vertices $s$ and $t$, whether $s$ and $t$ can be
connected by a path that avoids the failed vertices.

Following the introduction of the problem by Frigioni and
Italiano [20] and the more general problem
of batched vertex or edge failures by Pătraşcu and
Thorup [34][Strictly speaking,
in [34] Pătraşcu and Thorup considered only
edge failures. To the best of our knowledge, the first to
systematically investigate (batched) vertex failures on general
graphs were Duan and Pettie in [16].], there has been a long line of work on data
structures for connectivity oracles under vertex and edge failures.
We refer to a remarkably comprehensive literature overview in the work
of Duan and Pettie [17], which also provides the currently
best bounds for the problem as far as combinatorial and deterministic
data structures are concerned. Their data structure can be initialized
in time $\Oh(|G|\|G\|\cdot \log |G|)$, takes $\Oh(k\|G\|\log |G|)$
space, and supports updates in $\Oh(k^3\log^3 |G|)$ time and queries
in $\Oh(k)$ time. Here $\|G\|$ is the vertex count of $G$ and $\|G\|$ is the joint number of edges and
vertices in $G$.  These bounds can be slightly improved at the cost of
allowing randomization, however, the polylogarithmic dependency on the
size of the graph in the update time persists. As noted
in [17], from known results it is possible to derive data
structures with constant time complexity of operations for $k\leq 3$
(or $k\leq 4$ for edge failures), but, citing their words, “scaling
these solutions up, even to an arbitrarily large constant $k$, becomes
prohibitively complex, even in the simpler case of edge failures.”

Recently, van den Brand and Saranurak [40] proposed a very
different approach to the problem, using which they obtained a
randomized data structure that can be initialized in time
$\Oh(|G|^\omega)$, takes $\Oh(|G|^2\log |G|)$ space, and supports
updates in $\Oh(k^\omega)$ time and queries in $\Oh(k^2)$ time. In particular, the update and the query time are constant for constant $k$;
to the best of our knowledge, this is the only data structure that has
this property known so far. The approach is algebraic and, simplifying
it substantially, boils down to storing a matrix of counts of walks
between pairs of vertices and extracting answers to queries using
algebraic operations on those counts. To manipulate the counts
efficiently, one needs to work on their short hashes, for instance in
the form of elements from a fixed finite field. This introduces
randomization to the picture and avoiding it within this methodology
seems difficult. We remark that the data structure of van den Brand
and Saranurak [40] works even for the more general problem
of reachability in directed graphs under vertex failures, and can
handle arc insertions.

As the first main contribution of this paper, we prove the following
theorem.  Note that querying whether two vertices are connected by a
path avoiding failed vertices is equivalent to an update followed by a
connectivity query in the terminology of previous
works [40, 16, 17, 34].

Given a graph $G$ and an integer $k$, one can in time
$2^{2^{\Oh(k)}}\cdot |G|^2 \|G\|$ construct a data structure that
may answer the following queries in time $2^{2^{\Oh(k)}}$: given
$s,t\in V(G)$ and $k$ vertices $u_1,\ldots,u_k$ of $G$, are $s$ and
$t$ connected in $G$ by a path that avoids the vertices
$u_1,\ldots, u_k$? The space usage of the data structure is
$2^{2^{\Oh(k)}}\cdot \|G\|$.

Note that in <ref>, for every fixed $k$, all
operations are supported in constant time (which is doubly-exponential
in $k$). Also, the data structure is entirely deterministic and purely
combinatorial. To the best of our knowledge, this is the first
deterministic data structure with constant time queries. Note
also that for a fixed $k$, the space usage of our data structure is
linear in the size of the graph, as opposed to the quadratic
dependency in the result of van den Brand and
Saranurak [40].

Our approach to proving <ref> is completely new
compared to the previous approaches
. Our key
combinatorial observation is that connectivity queries over a constant
number $k$ of vertex failures can be evaluated in constant time
provided the underlying graph $G$ is sufficiently well-connected. The
requirement on the well-connectedness of $G$ depends on the number $k$. Obviously, there is no guarantee that the input graph $G$
satisfies this property. We therefore use a decomposition theorem of
Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [12] that (roughly) states the following
(see <ref> for a precise statement). For
every graph $G$ and fixed number $k$, there is a tree decomposition
where every intersection of adjacent bags has bounded size and every bag
is well-connected for parameter $k$. Moreover, such a tree
decomposition can be computed in time $2^{\Oh(k^2)}|G|^2\|G\|$. The
data structure of <ref> is constructed around the tree decomposition $\Tt$ provided by the theorem of Cygan et
al. [12]. Intuitively speaking, whether $s$ and $t$ are connected via a path that
avoids the vertices $u_1,\ldots, u_k$ can be decided using dynamic programming over $\Tt$. We employ known
techniques developed for answering queries on trees in constant time, for instance a deterministic variant of Simon's
factorization [13], to be able to compute the outcome of this dynamic programming efficiently for any query given on input.

We provide a more detailed overview of the proof of
<ref> in <ref>.  The full proof is
provided in <ref>.

The time complexity guarantees provided by <ref>
can be improved by allowing larger space usage. We give a variant of
<ref> (<ref>) that offers queries
in time $k^{\Oh(1)}$ after initialization in time
$2^{\Oh(k\log k)}\cdot |G|^{\Oh(1)}$, but assumes space usage
$k^{\Oh(1)}\cdot |G|^2$. The main idea here is to use a later variant
of the decomposition of Cygan et al. [12], proved
in [11], that provides quantitatively better bounds on
the adhesion and unbreakability of the decomposition, at the cost of
relaxing a technical condition on the unbreakability (see the
difference between strong and weak unbreakability, explained in
<ref>). The need of dealing with this relaxation turns
out to be a nuisance that, nonetheless, can be overcome in our

§.§ Algorithmic meta theorems

Once an algorithmic technique has been applied to solve a specific
problem, it is very desirable to understand the power and the
limitations of that technique, that is, to understand which other
problems can be solved with that technique and which problems
cannot. An approach to this very general goal is to prove an
algorithmic meta theorem: a theorem that establishes
tractability for a whole class of problems,
possibly on certain restricted input instances. As logic allows to
conveniently define classes of algorithmic problems, namely, the class
of all problems that can be expressed in the logic under
consideration, algorithmic meta theorems are often formulated as
model-checking problems for a logic. In the model-checking
problem for a logic $\Ll$ on a class of graphs $\CC$ we are
given a graph $G\in\CC$ and a sentence $\varphi\in \Ll$, and the task
is to decide whether $\varphi$ holds in $G$.  The archetypal result of
this form is a result of Courcelle stating that every formula of
monadic-second order logic ($\MSO_2$) can be evaluated in linear time
on all graphs whose treewidth is bounded by some fixed constant [14].
result has been extended to various other logics $\Ll$ and graph
classes $\CC$.

This approach to algorithmic meta theorems can be made precise in the
language of parameterized complexity, as follows.  Say that $\Ll$ is
tractable on $\CC$ if the model-checking problem for $\Cc$
and $\Ll$ is fixed-parameter tractable (fpt): it can be solved
in time $f(\varphi)\cdot \|G\|^c$, for some computable function $f$
and a constant $c$, both depending only on $\CC$.  Results about
tractability of a logic $\Ll$ on a class $\Cc$ imply the tractability
of a vast array of problems — namely all problems that can be
expressed in the logic $\Ll$ — on a given class of graphs.  For
instance, if model-checking first-order logic ($\FO$) is fpt on
a class of graphs $\CC$, then in particular the dominating set problem
is fpt on $\CC$, since the existence of a dominating set of size $k$
can be expressed by a first-order sentence with $k+1$ quantifiers that
range over the vertices of the graph.  Similarly, the independent set
problem is then also fpt on $\CC$.  On the other hand, if the more
powerful logic $\MSO_2$ is tractable on a class of graphs $\CC$, then
the $3$-colorability problem, or the hamiltonicity problem are
polynomial-time solvable on $\CC$, since both those problems can be
expressed using an $\MSO_2$ sentence, whose quantifiers that range
over sets of vertices and edges of the graph.

There has been a long line of work on fixed-parameter tractability of
model-checking $\FO$, as it is arguably the most fundamental logic.
This culminated in the work of Grohe, Kreutzer and
Siebertz [22], who proved that this problem is
fixed-parameter tractable on every class that is nowhere
dense. Those classes include for example the class of planar
graphs, or every class with bounded maximum degree, or of bounded
genus.  Without going into details, nowhere denseness is a general
notion of uniform sparseness in graphs, and it is broader than most
well-studied concepts of sparseness considered in structural graph
theory, such as excluding a fixed (topological) minor.  As observed by
Dvořák et al. [15], the result of Grohe et al. is
tight in the following sense: whenever $\Cc$ is not nowhere dense and
is closed under taking subgraphs, then $\FO$ model-checking on $\Cc$
is as hard as on general graphs, that is, $\AWstar$-hard. This means
that as far as subgraph-closed classes are concerned, sparsity —
described formally through the notion of nowhere denseness — exactly
delimits the area of tractability of $\FO$ and the limits of the
locality method for $\FO$ model-checking.

The aforementioned classic theorem of Courcelle [14] states
that the model-checking problem for $\MSO_2$ is fixed-parameter
tractable on a class $\Cc$ if $\Cc$ has bounded treewidth. The proof
translates the given sentence into a suitable tree automaton working
on a tree decomposition of the input graph; this approach brings a
wide range of automata-based tools to the study of $\MSO_2$ on
graphs. Again, as shown by Kreutzer and
Tazari [27] and Ganian et
al. [21], under certain complexity assumptions this
is (almost) the most one could hope for: on subgraph-closed classes
whose treewidth is poly-logarithmically unbounded, model-checking of
$\MSO_2$ becomes intractable from the parameterized perspective. So
for $\MSO_2$, bounded treewidth (almost) delimits the frontier of
tractability, at least for subgraph-closed classes, and automata-based techniques exactly explain what can be done algorithmically.

With the aim to provide a meta theorem that captures the essence of
the techniques developed to answer connectivity under vertex failures,
we search for a logic that can express these queries. It is easy to
see that $\MSO_2$ is strong enough, but in fact, $\MSO_2$ is much
stronger and as explained above, it is intractable beyond graphs of
bounded treewidth. On the other hand, $\FO$ can only express local
properties and in particular, it cannot even express the very simple
query of whether two vertices are in the same connected component. This
naturally leads to an extension of $\FO$ that may use connectivity
under vertex failures as atomic formulas. Interestingly, such a logic
was only very recently introduced independently by
Bojańczyk [8] and by Schirrmacher et
al. [36] under the name separator logic, and
denoted $\FOsep$. This logic extends $\FO$ by predicates
$\conn_k(s,t,u_1,\ldots,u_k)$ (one for each $k\ge 0$) with the
following semantics: if $s,t,u_1,\ldots,u_k$ are vertices of a graph
$G$, then $\conn_k(s,t,u_1,\ldots,u_k)$ holds if and only if there is
a path that connects $s$ with $t$ and does not pass through any of the
vertices $u_1,\ldots,u_k$.  Thus, separator logic involves very basic
connectivity queries that have a global character, unlike plain $\FO$,
which is local. On the other hand, while $\conn_k(s,t,u_1,\ldots,u_k)$
predicates are expressible in $\MSO_2$, it is no surprise that the
expressive power of $\FOsep$ is strictly weaker than that of
$\MSO_2$. For example, $\MSO_2$ can express bipartiteness, while
$\FOsep$ cannot <cit.>. Separator logic can
still express many interesting algorithmic properties, such as the
feedback vertex set problem and many recently studied elimination
distance problems [5].

As the second main result of the paper, we prove an algorithmic meta
theorem for separator logic. We show that the frontier of tractability
of $\FOsep$ is almost exactly delimited by classes of graphs that
exclude a fixed topological minor. More precisely, we prove the
following complementary results.

Let $\Cc$ be a class of graphs that exclude a fixed graph as a
topological minor. Then given $G\in \Cc$ and an $\FOsep$ sentence
$\varphi$, one can decide whether $\varphi$ holds in $G$ in time
$f(\varphi)\cdot \|G\|^3$, where $f$ is a computable function
depending on $\CC$.

For the lower bound, we will need a technical assumption.  We say that
a class $\Cc$ admits efficient encoding of topological minors
if for every graph $H$ there exists $G\in \Cc$ such that $H$ is a
topological minor of $G$, and, given $H$, such $G$ together with a
suitable topological minor model can be computed in time polynomial in
$|H|$. Note that in particular such $G$ can be only polynomially
larger than $H$.

Let $\Cc$ be a subgraph-closed class of graphs that admits efficient
encoding of topological minors. Then the model-checking of
$\FOsep$ on $\Cc$ is $\AWstar$-hard, even for the fragment that uses
only $\conn_k$ predicates with $k\le 2$.

On the one hand, these results show that separator logic is a natural
logic whose expressive power lies strictly between $\FO$ and $\MSO_2$,
and which corresponds, in the sense described above, to a natural
property of classes of graphs that lies between bounded treewidth and
nowhere denseness, see <ref>.

[r, "⊊"]
[r, "⊊"] [leftrightsquigarrow]d(∗)
_2[leftrightsquigarrow]d[14, 27]

2cmnowhere dense

2cmexcluded top. minor
[l, swap, "⊋"]

2cmbounded treewidth
[l, swap, "⊋"]

Correspondences between logics and properties of graph classes. An arrow $\cal L\leftrightsquigarrow \cal P$
between a logic $\cal L$ and a property $\cal P$ of graph classes denotes a correspondence:
the logic $\cal L$ is tractable on a graph class $\CC$ if and, under additional assumptions, only if, the class $\CC$ has the property $\cal P$.
Our result is the central correspondence $(\ast)$.

On the other hand, the proof of <ref> takes the technique
of dynamic programming over tree decompositions with unbreakable parts
to the limit. The tractability result generalizes several recent
algorithmic results for concrete problems
expressible in
separator logic [3, 6, 33].

The proof of <ref> is easy (see <ref>),
so we focus on sketching the proof of <ref>, which
is the main technical contribution of the second part of the paper.

Let us fix
an $\FOsep$ sentence $\varphi$, and let $k+2$ be the maximum arity of
connectivity predicates appearing in $\varphi$. Again, the key observation is
that $\conn_k$ predicates can be rewritten to
plain $\FO$ provided the graph is well-connected, and the reason for this is the same combinatorial observations that underlies the proof of <ref>.
Coming back to our dynamic programming on the tree decomposition,
we choose to present it using
a new framework based on automata, as this brings us closer
to the classic understanding of logic on tree-decomposable
graphs. Intuitively, the automaton processes a given tree in a
bottom-up manner, but we assume that on the children of every node
there is an additional structure of a graph. We say that such trees are augmented with graphs.
When the automaton processes a node $x$,
it chooses a transition based on an $\FO$ query executed on the
graph on the children of $x$, where each child is labeled with the
state computed for it before in the run. Then testing whether a
formula $\varphi\in \FOsep$ holds on a graph $G$ is reduced to deciding
whether an automaton constructed from $\varphi$ accepts such an
augmented tree, constructed from the tree decomposition
provided by the theorem of Cygan et al. [12].

The benefit of this approach is that other questions related to the
logic $\FOsep$ can be reduced in the same way to questions about tree
automata over augmented trees.  We showcase this by proving that given
an $\FOsep$ query $\varphi(\bar x)$ with free variables and a graph
$G$ from a fixed topological-minor-free class $\Cc$, the answers to
$\varphi(\bar x)$ on $G$ can be enumerated with constant delay after
fpt preprocessing (see <ref> for a precise
statement). Similarly, the formula $\varphi(\bar x)$ can be queried in
constant time after fpt preprocessing (see
<ref>).  In general, we believe that the
framework of automata over augmented trees may be of independent
interest, as it seems to be a convenient model for understanding
dynamic programming procedures over tree-decomposable structures.

Similar fpt query-answering and enumeration algorithms for
plain  have been obtained for classes with bounded expansion
[26, 39] and
nowhere dense classes [35] and for
$\MSO_2$ on trees and graphs of bounded
treewidth [4, 25, 1].  Our general
approach based on augmented trees allows us to generalize those results
to trees that are augmented with graphs coming from a nowhere dense
class, and to a certain logic combining the power of  on trees and
on graphs.

Let us comment on the novelty of using the decomposition theorem of
Cygan et al. [12].  The result of Cygan et
al. [12] has been used several times for various graph
problems [11, 12, 32, 30, 38]. Our
application is the most similar to (and in fact, draws inspiration
from) the work of Lokshtanov et al. [31], who proved
the following statement: for every $\CMSO_2$ sentence $\varphi$ and
$k\in \N$, model-checking $\varphi$ on general graphs can be
reduced to model-checking $\varphi$ on $(q,k)$-unbreakable graphs,
where $q$ is a constant depending on $\varphi$ and $k$. As $\FOsep$ is
subsumed by $\CMSO_2$, this result can be almost applied to establish
<ref>. The caveat is that the unbreakable graph output by
the reduction needs to admit efficient $\FO$ model-checking so that
the considered $\FOsep$ sentence can be decided in fpt time after
rewriting it to plain $\FO$. In essence, we show that it is possible
to guarantee this provided the input graph excludes a fixed
topological minor. We remark that the work of Lokshtanov et
al. [31] does not use the decomposition theorem of
Cygan et al. [12] directly, but relies on its conceptual
predecessor, the recursive understanding
technique [10, 28].

In <ref> we give an overview of the proofs of
our main results: <ref>,
<ref>, and <ref>.  In the main body of the paper, after formal
preliminaries, we present the proof of <ref> in
<ref> and
<ref>. <ref> presents
<ref>, a variant of <ref> that
offers faster queries.  The proof of <ref> is presented
in <ref> and <ref>, devoted
respectively to introducing the framework of automata over augmented
trees and applying them to $\FOsep$ on classes excluding a fixed
topological minor. <ref> is proved in <ref>.

§ OVERVIEW

In this section we provide an overview of the proofs of our main results: <ref>, <ref>, and <ref>.
We start with <ref>, as this proof exposes all main ideas in a purely algorithmic setting. Then we discuss how
the same methodology can be used for <ref>. In this
introduction we assume familiarity with basic terminology of tree
decompositions; see <ref> for details.

§.§ Data structure for
connectivity under vertex failures: proof of

As mentioned in <ref>, the central idea of this work
is to tackle problems involving connectivity predicates using a decomposition into well-connected — or, more formally, unbreakable — parts. We
first need to recall a few definitions.

A separation in a graph $G$ is a pair $(A,B)$ of vertex subsets
such that $A\cup B=V(G)$ and there are no edges in $G$ between
$A\setminus B$ and $B\setminus A$. The order of the separation
is the cardinality of the separator $A\cap B$. A vertex subset
$X$ is $(q,k)$-unbreakable in a graph $G$ if for every
separation $(A,B)$ in $G$ of order at most $k$ in $G$, either
$|A\cap X|\leq q$ or $|B\cap X|\leq q$. So intuitively speaking, a
separation of order $k$ cannot break $X$ in a balanced way: one of the
sides must contain at most $q$ vertices of $X$.

The notion of unbreakability has been implicitly introduced in the
context of parameterized algorithms by Kawarabayashi and Thorup in
their work on the $k$-Way Cut problem [28].
This work has brought about the method of recursive
understanding, which was then made explicit by Chitnis, Cygan,
Hajiaghayi, Pilipczuk, and Pilipczuk in the technique of
randomized contractions [10]. Intuitively,
recursive understanding is a Divide&Conquer scheme using which one
can reduce problems on general graphs to problems on suitably
unbreakable graphs, provided certain technical conditions are
satisfied. The technique was also applied in the context of
model-checking: Lokshtanov, Ramanujan, Saurabh, and
Zehavi [31] proved that the problem of deciding a
property expressed in $\CMSO_2$ in fpt time on general graphs can be
reduced to the same problem on suitably unbreakable graphs. This
result was used to provide algorithms for computing elimination
distance to certain graph
classes [2, 19, 24],
which is very much related to separator logic
(see <cit.>).

In this work, we will not use recursive understanding or randomized
contractions per se, but their conceptual successor: the
decomposition into unbreakable parts. Precisely, the following theorem
was proved by Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and
Saurabh [12].

There is a function $q(k)\in 2^{\Oh(k)}$ such that given a graph $G$
and $k\in \N$, one can in time $2^{\Oh(k^2)}\cdot |G|^2\|G\|$
construct a (rooted) tree decomposition $\Tt=(T,\bag)$ of $G$
satisfying the following.

* All adhesions in $\Tt$ are of size at most $q(k)$; and

* every bag of $\Tt$, say at node $x$, is
$(q(k),k)$-unbreakable in the subgraph of $G$ induced by the
union of bags at all descendants[We follow the
convention that every node is its own ancestor and descendant.]
of $x$.

We remark that a different variant of
<ref> was later proved by Cygan, Komosa,
Lokshtanov, Pilipczuk, Pilipczuk, and
Wahlström [11]. This variant provides much stronger
unbreakability guarantees — $q(k)=k$ — at the cost of relaxing the
unbreakability to hold only in the whole graph $G$. See
<ref> for a discussion. The variant
of [11] can be also used in our context and this leads
to improving some quantitative bounds, however for simplicity, we focus
on <ref> in this overview.

A typical usage of <ref> is to
apply bottom-up dynamic programming on the obtained tree
decomposition $\Tt=(T,\bag)$. The subproblem for a node $x$ of $T$
corresponds to finding partial solutions in the subgraph of $G$
induced by the union of bags at descendants of $x$, for every possible
behavior of such a partial solution on the adhesion connecting $x$
with its parent. That this adhesion has size at most $q(k)$ gives an
upper bound on the number of different behaviors. To solve such a
subproblem one needs to aggregate the solutions computed for the
children of $x$ by solving an auxiliary problem on the subgraph
induced by the bag of $x$. In various problems of interest, the
unbreakability of the bag becomes helpful in solving the auxiliary
problem. This general methodology has been successfully used to give
multiple fpt algorithms for cut
problems [12, 11, 38], most prominently
for Minimum Bisection [12]. More recent uses
include a parameterized approximation scheme for the Min
$k$-Cut problem [32] and a fixed-parameter
algorithm for Graph Isomorphism parameterized by the size of
the excluded minor [30]. On a high level, we apply
the same methodology here.

*The case of totally unbreakable graphs. Let us come back
to the problem of evaluating connectivity queries: we are given a
graph $G$ and after some preprocessing of $G$, we would like to be
able to quickly evaluate for given vertices $s,t,u_1,\ldots,u_k$
whether $\conn_k(s,t,u_1,\ldots,u_k)$ holds. Consider first the
following special case: the whole $G$ is $(q,k)$-unbreakable for some
parameter $q$ (or more formally, $V(G)$ is $(q,k)$-unbreakable in
$G$). The key observation is that then, whether
$\conn_k(s,t,u_1,\ldots,u_k)$ holds can be easily decided in time
polynomial in $q$ and $k$ as follows.

Run a breadth-first search from $s$ in $G-\{u_1,\ldots,u_k\}$, but
terminate the search once $q+1$ different vertices have been reached.
If the search reached $t$, then for sure $\conn_k(s,t,u_1,\ldots,u_k)$
holds. If the search finished before reaching $q+1$ different vertices
and it did not reach $t$, then for sure $\conn_k(s,t,u_1,\ldots,u_k)$
does not hold. In the remaining case, perform a symmetric procedure
starting from $t$. The key observation is that if both breadth-first
searches — from $s$ and from $t$ — got terminated after reaching
$q+1$ different vertices, then the $(q,k)$-unbreakability of $G$
implies that $\{u_1,\ldots,u_k\}$ do not separate $s$ from $t$. So
then $\conn_k(s,t,u_1,\ldots,u_k)$ holds. It is straightforward to
implement this procedure in time polynomial in $q$ and $k$ given the
standard encoding of $G$ through adjacency lists.

In the general case, we cannot expect the given graph $G$ to be
$(q,k)$-unbreakable for any parameter $q$ bounded in terms of $k$.
However, we can use <ref> to compute a
tree decomposition $\Tt$ of $G$ into parts that are
$(q,k)$-unbreakable for $q\in 2^{\Oh(k)}$. The idea is that then, a
query $\conn_k(s,t,u_1,\ldots,u_k)$ can be evaluated by bottom-up
dynamic programming on $\Tt$. By suitably precomputing enough
auxiliary information about $\Tt$, this evaluation can be performed in
time depending only on $q$ and $k$.

*Evaluating a query on the decomposition. Consider then
the following setting: we are given the decomposition $\Tt=(T,\bag)$
provided by <ref>, and for given
$s,t,u_1,\ldots,u_k$ we would like to decide whether
$\conn_k(s,t,u_1,\ldots,u_k)$ holds. So far let us not optimize the
complexity: the goal is only to design a general algorithmic
mechanism which will be later implemented efficiently using
appropriate data structures.

For every node $x$ of $T$, let $\adh(x)$ be the adhesion between $x$
and its parent (or $\emptyset$ if $x$ is the root), let $\cone(x)$ be
the union of the bags at the descendants of $x$, and let
$\cmp(x)=\cone(x)\setminus \adh(x)$. Call a node $x$ affected
if $\cmp(x)$ contains a vertex of $\{s,t,u_1,\ldots,u_k\}$, and
unaffected otherwise. Further, let
$D(x)=\adh(x)\cup (\cmp(x)\cap \{s,t\})$; note that $|D(x)|\leq q+2$.
Our goal is to compute the following (connectivity) profile for
every node $x$ of $T$:

$$\profile(x)=\left\{\{a,b\}\in\binom{D(x)}{2}\quad\Big|\quad a\textrm{ and }b\textrm{ are connected in }G[\cone(x)\setminus \{u_1,\ldots,u_k\}]\right\}.$$

We remark that the tree decomposition $\Tt$ can be chosen so that it
satisfies the following basic connectivity property: for every node
$x$ and vertices $a,b\in \adh(x)$, there is a path connecting $a$
and $b$ whose all internal vertices belong to $\cmp(x)$. Thus, for
every unaffected node $x$, we have that
$\profile(x)=\binom{D(x)\setminus \{u_1,\ldots,u_k\}}{2}$.

It is easy to see that the profile of $x$ is uniquely determined by
the profiles of the children of $x$ and the subgraph induced by the
bag of $x$. The following lemma shows that this can be done

Let $x$ be a node of $T$. Suppose that for each affected child $z$
of $x$ we are given $\profile(z)$. Then, subject to suitable
preprocessing of $G$, one can compute $\profile(x)$ in time
polynomial in $q$.

Note that every node has at most $k+2$ affected children, hence the
input to the algorithm of <ref> is of size
polynomial in $q$.

Let us sketch the proof of <ref>. In essence, we
apply the same strategy as the one from the case when the whole
graph $G$ is unbreakable. Let $\bgraph(x)$ be the
graph obtained from $G[\bag(x)]$ by turning the adhesion $\adh(z)$
into a clique, for every child $z$ of $x$. Note that $\bgraph(x)$ does
not depend on the query, and thus can be precomputed upon
initialization. As $\bag(x)$ is
$(q,k)$-unbreakable in $G[\cone(x)]$, to test whether two vertices
$a,b\in \bag(x)$ are connected in
$G[\cone(x)\setminus \{u_1,\ldots,u_k\}]$ it suffices to apply
breadth-first searches from $a$ and $b$ in $\bgraph(x)$ that are
terminated after reaching $q+1$ different vertices, except that these
searches are forbidden to use vertices from
$\{u_1,\ldots,u_k\}\cap \bag(x)$ as well as those edges originating
from turning adhesions of affected children into cliques that are not
in respective profiles. Provided $\bgraph(x)$ is precomputed and a
list of affected children together with their profiles is given on
input, it is easy to implement this algorithm so that it runs in time
polynomial in $q$. Thus we can decide for every pair
$\{a,b\}\in \binom{\adh(x)}{2}$ whether it should be included in
$\profile(x)$. A similar reasoning can be applied to pairs in
$\binom{D(x)}{2}$ that include $s$ or $t$.

By applying <ref> bottom-up, we can compute all the
profiles in time $q^{\Oh(1)}\cdot |T|\leq q^{\Oh(1)}\cdot |G|$. Then
we can read whether $\conn_k(s,t,u_1,\ldots,u_k)$ holds by checking
whether $\{s,t\}$ belongs to the profile of the root of $T$. Hence,
the query $\conn_k(s,t,u_1,\ldots,u_k)$ can be evaluated in time
$q^{\Oh(1)}\cdot |G|$.

*Data structure. Our final goal is to enrich the
decomposition $\Tt$ with some additional information so that the
mechanism presented above can be executed in time depending only on

For a vertex $v$ of $G$, let $\hm(v)$ be the unique top-most node
of $T$ whose bag contains $v$. Let
$\Sh\coloneqq \{s,t,u_1,\ldots,u_k\}$ and let
$X=\{\hm(v)\colon v\in \Sh\}$.

The sets $X,Y$ and $Y'$. Only the nodes from $Y\cup Y'$ are
marked in the figure, wheras
the shaded areas indicate subtrees consisting of
nodes which are not marked in the figure. Every affected node lies on a path from some $y\in Y$ to $f(y)\in Y'$.

Note that $|X|\leq |\Sh|\leq k+2$ and
that a node of $T$ is affected if and only if it is an ancestor of a
node from $X$. Let now $Y$ be the lowest common ancestor
closure of $X$: the set comprising $X$ and all lowest common
ancestors of pairs of vertices of $X$. It is well-known that then
$|Y|\leq 2|X|-1\leq 2k+3$. We also add the root of $T$ to $Y$ in case
it is not already present; thus $|Y|\leq 2k+4$. Observe that if for
every vertex $v$ we store a pointer to $\hm(v)$, and we set up the
data structure for lowest common ancestor queries of Harel and
Tarjan [23] on $T$, then for given $s,t,u_1,\ldots,u_k$ the
set $Y$ can be computed in time polynomial in $k$.
For every node $y$ in $Y$ let $f(y)$ denote the closest ancestor of $y$
whose parent belongs to $Y$, or $y$ if no such ancestor exists
(see <ref>).
Note that every affected node lies on a path joining $y$ with $f(y)$,
for some $y\in Y$.
Let $Y'=\setof{f(y)}{y\in Y}$.
Then $Y'$ is the set of all nodes that are affected children of
a node in $Y$. Note that every element in $Y'$ has exactly one
preimage under $f$, that is, there is an function $f^{-1}\from Y'\to Y$
such that $f(f^{-1}(y'))=y'$ for all $y'\in Y'$.
In particular, $|Y'|\le |Y|$.
Using a
slight modification of the data structure of Harel and
Tarjan [23], we can compute $Y'$ as well as the function $f^{-1}\from Y'\to Y$ in time polynomial in $k$.

The idea is that when evaluating query $\conn_k(s,t,u_1,\ldots,u_k)$,
we can compute the profiles only for the nodes of $Y\cup Y'$, instead of all
affected nodes of $T$. Note that the root of $T$ was explicitly added to
$Y$, so we will still be able to read the answer to
$\conn_k(s,t,u_1,\ldots,u_k)$ from the profile of the root.

We process the nodes of $Y\cup Y'$ in a bottom-up manner. Consider then any element
$x\in Y\cup Y'$; our task is to compute its profile based on the profiles
of its strict descendants belonging to $Y\cup Y'$.
We distinguish two cases.
In the first case, $x\in Y$, so we may compute $\profile(x)$ using the algorithm of
The second case is of an element  $x\in Y'$; then $x=f(y)$ where $y=f^{-1}(x)$.
Observe that the path from $y$ to $x$ consists of affected nodes,
whose siblings are unaffected nodes.
We now show how $\profile(x)$ can be
computed from $\profile(y)$.

For two nodes
$c,d$ of $T$, where $c$ is an ancestor of $d$, let $\torso(c,d)$ be
the set of all pairs $\{a,b\}\in \binom{\adh(c)\cup \adh(d)}{2}$ such
that in $G$ there is a path from $a$ to $b$ whose all internal
vertices belong to $\cmp(c)\setminus \cone(d)$. Then to compute
$\profile(x)$ from $\profile(y)$, construct an
auxiliary graph with vertices
$(\adh(x)\cup \adh(y)$ and edges $\profile(y)\cup \torso(x,y)$.
observe that $\profile(x)$ is the reachability relation in this graph
restricted to $\adh(x)\setminus \{u_1,\ldots,u_k\}$. The key point
implying the correctness of this observation is that there are no
vertices from $X$ in $\cmp(x)\setminus \cmp(y)$.

Observe now that the values of $\torso(c,d)$ for $(c,d)$ ranging over
ancestor/descendants pairs in $T$ are independent of the query.
Therefore, upon initialization we can compute a data structure that
can be queried for those valued efficiently. The statement below
describes two possible implementations.

Given $\Tt$, one can
set up data structures that can answer $\torso(c,d)$ queries with
the following specifications:

* initialization time $q^{\Oh(1)}\cdot |G|^2\|G\|$, memory usage
$q^{\Oh(1)}\cdot |G|^2$, query time $q^{\Oh(1)}$; or

* initialization time $2^{\Oh(q^2)}\cdot |G|$, memory usage
$2^{\Oh(q^2)}\cdot |G|$, query time $2^{\Oh(q^2)}$.

The first point of <ref> is actually straightforward:
just compute and store all the $\Oh(|T|^2)=\Oh(|G|^2)$ answers to the
torso queries, each in time $q^{\Oh(1)}\cdot \|G\|$ using $q^{\Oh(1)}$
applications of breadth-first search. The second point, which trades
exponential dependency on $q$ for obtaining linear memory usage and
initialization time, is more interesting. Before we discuss it, let us
observe that we may now complete the proof of
<ref>. Indeed, using the data structure from the
second point of <ref>, we can compute $\profile(x)$
from $\profile(y)$ for each $x\in Y'$ and $y=f^{-1}(x)$. By
performing this procedure for all the at most $2(2k+4)$ nodes of $Y\cup Y'$ in a
bottom-up manner, we eventually compute the profile of the root of
$T$, from which the answer to the query can be read. The running time
is dominated by $q^{\Oh(1)}$ calls to the data structure of the second
point of <ref>, each taking
$2^{\Oh(q^2)}=2^{2^{\Oh(k)}}$ time.

Finally, let us discuss the proof of the second point of
<ref>. We reduce this problem to the problem of
evaluating product queries in a semigroup-labeled tree,
defined as follows. Suppose $T$ is a rooted tree whose edges are
labeled with elements of a finite semigroup $S$. The task is to set
up a data structure that for given nodes $x,y$, where $x$ is an
ancestor of $y$, outputs the product of the elements of $S$ on the
path in $T$ from $x$ to $y$. The problem of evaluating torso queries
can be reduced to this abstract setting by considering a suitable
semigroup of bi-interface graphs, which represent connectivity
between corresponding adhesions; see [9] for the
origin of this concept. This semigroup has size $2^{\Oh(q^2)}$. So it
then suffices to use the following result.

There is a data structure for the problem of evaluating product
queries in a tree $T$ labeled with elements of a finite semigroup
$S$ that achieves query time $|S|^{\Oh(1)}$, memory usage
$|S|^{\Oh(1)}\cdot |T|$, and initialization time
$|S|^{\Oh(1)}\cdot |T|$.

<ref> can be easily derived from the
deterministic variant of Simon's factorization, due to
Colcombet [13]. However, in <ref> we
also present a direct and arguably simpler proof that may be of
independent interest.

This finishes the proof of <ref>. Note that in
the argumentation there are two modules that can be replaced with
other solutions:

* The decomposition of <ref> can be
replaced with the more recent variant from [11]. This allows us to have $q=k$, implying that
all the $\smash{2^{2^{\Oh(k)}}}$ factors are replaced with $\smash{2^{\Oh(k^2)}}$.
The cost is increasing the polynomial factor of the initialization
time to an unspecified term $\smash{|G|^{\Oh(1)}}$ and several technical
complications in the analysis, which nevertheless can be overcome.

* Instead of using the data structure of the second point of
<ref>, we can use the first point. This allows us
to have polynomial dependency on $q$ in the query time at the
cost of quadratic dependence on $|G|$ in the memory usage.

In particular, if both these replacements are performed, we obtain a data structure with initialization time $2^{\Oh(k\log k)}\cdot |G|^{\Oh(1)}$, memory usage $k^{\Oh(1)}\cdot |G|^2$, and query time $k^{\Oh(1)}$. See <ref>.

§.§ Model-checking $\FOsep$:

We now turn to the proofs of <ref> and <ref>.
In those theorems, we fix a class $\CC$
and consider the model-checking problem for the logic $\FOsep$,
that is, the problem of deciding whether a given $\FOsep$ sentence holds in a given graph $G\in\CC$.

*Lower bound.
First let us explain why we require $\CC$ to exclude a fixed topological minor
in <ref>.
Clearly, the model-checking problem for  generalizes the model-checking problem for , so $\CC$ should be in particular a class for which it is known that
$\FO$ model-checking is $\FPT$.
This is the case not only for classes that exclude a topological minor but also for all nowhere dense classes [22]. So let us see why it is not enough to merely assume that $\CC$ is  nowhere dense.

For a graph $G$ and $k\in \N$, the $k$-subdivision $G^{(k)}$ of $G$ is obtained from $G$ by replacing each edge by a path of length $k+1$.
It follows from the definition of nowhere denseness that the class $\CC$ of all graphs of the form $G^{(n)}$, where $G$ is an arbitrary graph on $n$ vertices, is nowhere dense.
However, a formula of $\FOsep$ can easily recover $G$ from $G^{(n)}$, at least when $G$ has no vertices of degree $2$. Indeed, the original vertices of $G$ are precisely the vertices of $G^{(n)}$ that have degree at least $3$, which can be expressed by an $\FO$ formula $\phi_V(x)$. Furthermore, two such vertices $u,v$ are adjacent in $G$ if and only if there is some vertex $z$ of degree $2$ in $G^{(n)}$ such that
for every vertex $w$ of $G^{(n)}$, $\conn(z,w,u,v)$ holds only if $w$ has degree $2$ in $G^{(n)}$. This condition can be written using an $\FOsep$ formula $\phi_E(u,v)$.
Using this observation, any $\FO$ sentence $\phi$ can be replaced by an $\FOsep$ sentence $\phi'$, so that for every graph $G$ as above, $\phi$ holds in $G$ if and only if $\phi'$ holds in $G^{(n)}$. Essentially, $\phi'$ is obtained from $\phi$ by replacing every atomic formula $E(x,y)$ (denoting adjacency) by $\phi_E(x,y)$, and guarding all quantifiers by $\phi_V(x)$.
Therefore, if we could efficiently model-check $\phi'$ on the nowhere dense class $\CC$, we could as well model-check $\phi$ on the class of all graphs (of size at least $3$ and minimum degree at least $3$), as follows:
given an arbitrary graph $G$, first construct the graph $G^{(n)}\in \CC$ (in time polynomial in $n=|V(G)|$)
and then test $\phi'$ on $G^{(n)}$. Hence, if $\FOsep$ model-checking was fpt on $\CC$, then $\FO$ model-checking would be fpt on the class of all graphs, implying $\FPT=\AWstar$. So nowhere dense graph classes are too general for the statement of <ref> to hold. Intuitively, the notion of nowhere denseness is not preserved under contracting long paths, which can be simulated in the logic .

The same simple argument proves <ref>.
Indeed, the argument works not only for the graph $G^{(n)}$ obtained as the $n$-subdivision of $G$ but also for any subdivision $G'$ (obtained by replacing each edge independently by any number of vertices) of $G$,
as long as $G'$ can be computed from $G$ in polynomial time. The condition that $\CC$ is subgraph-closed and admits efficient encoding of topological minors guarantees precisely that for any given graph $G$ we can construct, in polynomial time, a graph $G'$ which is a subdivision of $G$ and belongs to $\CC$. This yields <ref>
(see <ref> for details).

*Upper bound.
We now give some details concerning the proof of <ref>, which is the second main contribution of the paper.

The starting observation is that for a
$(q,k)$-unbreakable graph $G$, the query $\conn_k(u,v,x_1,\ldots,x_k)$ can be expressed in plain . Indeed, this query fails if and only if there is a set $A$ of at most $q$ vertices which contains exactly one of the vertices $u$ and $v$, and such that all neighbors of vertices of $A$ outside of $A$ are contained in $\set{x_1,\ldots,x_k}$. The existence of such a set of $q$ vertices can be expressed using $q$ existential quantifiers followed by a universal quantifier.
So $\FOsep$ with connectivity queries of arity at most $k+2$
is equally expressive as plain $\FO$ on $(q,k)$-unbreakable graphs, as long as $q$ is a constant.

Now, if the graph $G$ is not $(q,k)$-unbreakable, we work with the
tree decomposition into $(q,k)$-unbreakable parts given by <ref>, where $q=q(k)$ is a constant depending on $k$.
The next observation is that the constant-time querying algorithm used in the proof of <ref> and explained above, can be seen as a formula on a suitably defined logical structure. Indeed,
if we look into the data structure answering the queries $\conn_k(u,v,x_1,\ldots,x_k)$, we notice that each such query triggers a constant number
of operations asking about the least common ancestor of two nodes in the tree decomposition, or asking about the membership of a vertex to a bag.
Additionally, the algorithm may ask, for two vertices $u,v$ belonging to a bag $x$,
whether $u$ and $v$ are adjacent in the original graph, or whether they are adjacent in the bag graph $\bgraph(x)$. Finally, the algorithm also performs torso queries.
We may therefore construct a logical structure, corresponding to the data structure, such that this basic functionality
is expressible by a first-order formula in this structure. Then the query
$\conn_k(u,v,x_1,\ldots,x_k)$ becomes expressible using a plain  formula in the logical structure. It will then remain to show that we can model check  formulas in fpt on the resulting logical structure.

It is convenient to abstract away the details of our logical structure, and represent it in the following form:
It is a tree $T$ (possibly vertex-labeled), together with additional edges (possibly labeled) between some nodes which are siblings in the tree; see <ref>. We call such a structure an augmented tree.
In such a tree, the set of children of any node $v$ carries a structure of a graph.
In the particular case of our construction, those graphs will precisely correspond to bag graphs.
Recall that a bag graph is obtained from the subgraph induced by a bag by turning all adhesions towards children into cliques. It is not difficult to show (see <ref>) that if the original graph $G$ is $H$-topological-minor free, then the resulting bag graphs
are $H'$-topological-minor-free for some $H'$ depending on $H$ and on $k$.
Hence, we obtain a tree augmented with $H'$-topological-minor-free graphs.
And the original query $\conn_k(u,v,x_1,\ldots,x_k)$ can be now represented as an
formula in the augmented tree, where the  formula may use the ancestor relation $\le$ on the tree nodes, as well as the adjacency relation between the siblings.
Showing this basically amounts to revisiting the proof of <ref> and arguing that the atomic algorithmic operations can now be simulated by  formulas in the augmented tree.

Let us note here that the remainder of the argument would go through even if we assumed that the resulting tree is augmented with graphs from a fixed nowhere dense class $\CC'$
which is not necessarily topological-minor-free.
However, if the original graph $G$ merely belongs to a nowhere dense class $\CC$,
then the bag graphs, and hence the graphs in the augmented tree, no longer need to belong to any fixed nowhere dense class. In fact, they may contain arbitrarily large cliques.

Continuing with the proof, now it remains to show that we can solve  model-checking on trees augmented with $H'$-topological-minor-free graphs in fixed-parameter time,
where the  formulas may use the ancestor relation in the tree as well as the edge relation among the siblings.

For this, we lift the usual, automata-based techniques for model-checking on trees, to the case of augmented trees. We define automata that process augmented trees in a bottom-up fashion, labeling the nodes of the tree with states from a finite set of states, starting from the leaves and proceeding towards the root.
At any node $x$, to determine the state of the automaton at $x$, we consider the graph induced on the children of $x$ in the augmented tree, vertex-labeled by the states computed earlier. Then the state at $x$ is determined by evaluating a fixed collection of first-order sentences on this labeled graph. In this way, all nodes of the tree are labeled by states, and the automaton accepts the augmented tree depending on the state at the root.

By construction, it can be decided in fpt time whether or not
a given such automaton accepts a given  tree that is augmented with graphs
that come from, say, a nowhere dense class. Additionally, using standard techniques,
we show that for every first-order sentence $\phi$ on augmented trees there is such an automaton that determines whether $\phi$ holds in a given augmented tree.
Therefore,  model-checking is fpt on trees augmented with graphs from a nowhere dense class; this in particular applies to classes with excluded topological minors.

To summarize, to  model-check a sentence $\phi$ of  on a $H$-topological-minor-free graph $G$, we perform the following reasoning:

* Using <ref>, compute a tree decomposition $\cal T$ of $G$ with $(q,k)$-unbreakable bags, where $k+2$ is the maximal arity of the connectivity predicates in $\phi$, and $q=q(k)$.

* Turn
$\cal T$ into a tree $\cal T'$ augmented with $H'$-topological-minor free graphs, where $H'$ depends on $H$ and $k$.

* In the augmented tree $\cal T'$, the connectivity predicate $\conn_k(u,v,x_1,\ldots,x_k)$ can be expressed using a plain  formula. This follows by analyzing how  connectivity predicates are evaluated in constant time, and observing that the atomic operations can be performed using  formulas in the augmented trees.

* Therefore, also $\phi$ can be expressed as a plain  formula $\phi'$, which is evaluated in
$\cal T'$.

* Convert $\phi'$ into an automaton $\cal A$ processing augmented trees,
using standard automata-based techniques.

* Run $\cal A$ on $\cal T'$ in a bottom-up fashion. This involves performing  queries on the graphs induced on the children of any given node, and uses one of the known algorithms for  model-checking on $H'$-topological-minor-free graphs.

<ref> describes the basic toolbox of automata on augmented trees,
explaining in detail the last two steps above, abstracting away from the specific application, and providing further results on augmented trees, e.g. concerning query enumeration.
In fact, with the same methods we can show that not only $\FO$ model-checking is fpt on trees augmented with graphs from a nowhere dense class,
but also a more general logic $\FOMSO$ combining the power of $\FO$ on the augmenting graphs with $\MSO$ on trees can be solved in fpt on augmented trees.

We then show in <ref> how to express the predicates $\conn_k$ on augmented trees using this more general logic $\FOMSO$.

§ PRELIMINARIES

Throughout this paper we assume the standard word RAM model with
machine words of length $\Oh(\log n)$, where $n$ is the total size of
the input. Recall that in this model we allow using arrays indexed by
integers in the range $\{1,\ldots,n^{\Oh(1)}\}$, which is sufficient
for the existence of data structures for least common ancestor queries
in trees in constant time [23].

§.§ Graphs

*Basic notation. We consider finite, undirected graphs
without loops. For a graph $G$, we write $|G|$ for $|V(G)|$ and
$\|G\|$ for $|V(G)|+|E(G)|$. For a pair of vertices $u,v\in V(G)$, a
$u$-$v$ path is a path with endpoints $u$ and $v$. We say that
$u$ and $v$ are connected in $G$ if there is a $u$-$v$ path in
$G$; otherwise $u$ and $v$ are disconnected. The graph $G$ is
connected if all pairs of its vertices are connected. The
interior of a path consists of all its vertices apart from the
endpoints, and two paths are internally vertex-disjoint if each
of them is disjoint with the interior of the other. For a vertex
subset $X\subseteq V(G)$ we write $G[X]$ for the subgraph of $G$
induced by $X$.

*Trees and ancestors.
A (rooted) tree is an acyclic and connected graph $T$ with a
distinguished root vertex $r$. We write $\parent(x)$ for the parent of
a node $x$ of $T$, and $\children(x)$ is the set of children of $x$
in $T$. By convention we set $\parent(r)=\bot$. We call a vertex
$x\in V(T)$ an ancestor of a vertex $y\in V(T)$, written
$x\preceq_T y$, or simply $x\preceq y$ if $T$ is clear from the
context, if $x$ lies on the unique path between $y$ and the root $r$.
Note that we consider every node to be an ancestor of itself.  For
nodes $x,y\in V(T)$, we write $\lca(x,y)$ for the least common
ancestor of $x$ and $y$ in $T$. Note that $x$ is an ancestor of $y$ if
and only if $\lca(x,y)=x$. If $x$ is a strict ancestor of $y$ (that
is, $x\preceq y$ and $x\neq y$), then we define the $y$-directed
child of $x$ to be the unique child $y'$ of $x$ that is an
ancestor of $y$; we denote it by $\dir(x,y)$.

*Topological minors. A topological minor model of a
graph $H$ in a graph $G$ is an injective mapping $\eta$ that maps
vertices of $H$ to vertices of $G$ and edges of $H$ to pairwise
internally vertex-disjoint paths in $G$ so that for every
$uv\in E(H)$, the endpoints of $\eta(uv)$ are $\eta(u)$ and
$\eta(v)$. We say that $G$ is $H$-topological-minor-free if
there is no topological minor model of $H$ in $G$. A class of graphs
$\Cc$ is topological-minor-free if there exists a graph $H$
such that every member of $\Cc$ is $H$-topological-minor-free.

Tree decompositions. A tree decomposition of a
graph $G$ is a pair $\Tt=(T,\bag)$, where $T$ is a rooted tree and
$\bag\colon V(T)\to 2^{V(G)}$ is a mapping that assigns to each node
$x$ of $T$ its bag $\bag(x)$, which is a subset of vertices of
$G$. The following conditions have to be satisfied:

* For every $u\in V(G)$, the set of nodes $x\in V(T)$ satisfying
$u\in \bag(x)$ induces a connected and nonempty subtree of $T$.

* For every edge $uv\in E(G)$, there exists a node $x\in V(T)$
such that $\{u,v\}\subseteq \bag(x)$.

Recall that if $r$ is the root of $T$, then by convention
$\parent(r)=\bot$ and $\bag(\bot)=\emptyset$.

With a tree decomposition $\Tt=(T,\bag)$ we associate a few auxiliary
mappings. For a node $x\in V(T)$, we define the following:

* The adhesion of $x$ is

$$\adh(x)\coloneqq \bag(\parent(x))\cap \bag(x).$$

* The margin of $x$ is

$$\mrg(x)\coloneqq \bag(x)\setminus \adh(x).$$

* The cone at $x$ is

$$\cone(x)\coloneqq \bigcup_{y\succeq_T x} \bag(y).$$

* The component at $x$ is

$$\cmp(x)\coloneqq \cone(x)\setminus \adh(x)= \bigcup_{y\succeq_T x} \mrg(y).$$

It is easy to see that the margins $\{\mrg(x)\colon x\in V(T)\}$ are
pairwise disjoint and cover the whole vertex set of $G$. Whenever we
use the notation introduced above, the tree decomposition $\Tt$ will
be always clear from the context.

The adhesion of a tree decomposition $\Tt=(T,\bag)$ is defined
as the largest size of an adhesion, that is,
$\max_{x\in V(T)}|\adh(x)|$.

We will commonly assume (without loss of generality) that the tree
decompositions that we work with satisfy some basic connectivity
conditions, subsumed in the following definition. A tree decomposition
$\Tt=(T,\bag)$ is regular if for every non-root node
$x\in V(T)$ we have that

*  the margin $\mrg(x)$ is nonempty;

*  the graph $G[\cmp(x)]$ is connected; and

*  every vertex of $\adh(x)$ has a neighbor in $\cmp(x)$.

Note that the last two conditions imply that for every node $x$ and
every pair of distinct vertices $u,v\in \adh(x)$ there is a $u$-$v$
path in $G[\cone(x)]$ whose interior is contained in $\cmp(x)$.

*Unbreakability. A separation in a graph $G$ is a
pair of vertex subsets $A,B\subseteq V(G)$ such that $A\cup B=V(G)$
and there is no edge with one endpoint in $A\setminus B$ and the other
in $B\setminus A$. The order of the separation $(A,B)$ is the
size of its separator $A\cap B$.

For $q,k\in \N$, a vertex subset $X$ in a graph $G$ is
$(q,k)$-unbreakable if for every separation $(A,B)$ of $G$ of
order at most $k$, we have

\[|A\cap X|\leq q\qquad\textrm{or}\qquad |B\cap X|\leq q.\]

The notion of unbreakability can be lifted to tree decompositions by
requiring it from every individual bag. There are, however, two
different ways of understanding this.

Fix $q,k\in \N$.  A tree decomposition $\Tt=(T,\bag)$ of a graph $G$

* weakly $(q,k)$-unbreakable if for every $x\in V(T)$,
$\bag(x)$ is $(q,k)$-unbreakable in $G$; and

* strongly $(q,k)$-unbreakable if for every $x\in V(T)$,
$\bag(x)$ is $(q,k)$-unbreakable in $G[\cone(x)]$.

It is straightforward to see that strong $(q,k)$-unbreakability
implies weak $(q,k)$-unbreakability, but the converse is not true.

We recall known results about the existence and computability of
unbreakable tree decompositions (<ref> was already stated as

For every graph $G$ and $k\in \N$ there exists a weakly
$(k,k)$-unbreakable tree decomposition of $G$ of adhesion at most
$k$. Moreover, given $G$ and $k$, such a tree decomposition can be
computed in time $2^{\Oh(k\log k)}\cdot |G|^{\Oh(1)}$.

There is a function $q(k)\in 2^{\Oh(k)}$ such that for every graph
$G$ and $k\in \N$ there exists a strongly $(q(k),k)$-unbreakable
tree decomposition of $G$ of adhesion at most $q(k)$.  Moreover,
given $G$ and $k$, such a tree decomposition can be computed in time
$2^{\Oh(k^2)}\cdot |G|^2\cdot \|G\|$.

In this paper we will mostly use <ref>, as
working with strong unbreakability yields a cleaner presentation of
arguments. However, in <ref> we show that weak
unbreakability can be used in the context of
<ref>, yielding a variant of the theorem that
offers better time complexity for queries.

Given any weakly or strongly $(q,k)$-unbreakable decomposition we can,
if necessary, refine it so that it becomes regular.  Hence, we may
assume that the tree decompositions constructed by the algorithms of
<ref> and <ref>
are regular. More precisely, this refinement can be achieved by
applying a folklore refinement procedure for instance presented in the
proof of <cit.>, which takes linear
time. This refinement does not increase the sizes of adhesions nor
spoils unbreakability, because every new bag is a subset of an old
bag. Note here that [9] allows tree decompositions to
be rooted forests rather than rooted trees. However, a rooted forest
can be turned into a rooted tree by adding a fresh root with an empty
bag, whose children are all the former roots. Note here that
properties mentioned in the definition of regularity are not required
from this new root.

*Bag graphs.
Let $\Tt=(T,\bag)$ be a regular tree decomposition of a graph $G$.
With a node $x$ of $G$ we associate the bag graph $\bgraph(x)$,
which is the graph obtained from $G[\cone(x)]$ by contracting, for
each $y\in \children(x)$, the set $\cmp(y)$ into a single vertex,
identified with $y$. More precisely, $\bgraph(x)$ is a graph defined
as follows:

* The vertex set of $\bgraph(x)$ is the disjoint union of
$\bag(x)$ and the set of children of $x$ in $T$.

* For $u,v\in \bag(x)$, $u$ and $v$ are adjacent in $\bgraph(x)$
if and only if they are adjacent in $G$.

* For $u\in \bag(x)$ and $y\in \children(x)$, $u$ and $y$ are
adjacent in $\bgraph(x)$ if and only if there exists $w\in \cmp(y)$
that is adjacent to $u$ in $G$.

* No two distinct $y,y'\in \children(x)$ are adjacent in $\bgraph(x)$.

Since $\Tt$ is regular, for every $y\in \children(x)$, the
neighborhood of $y$ in $\bgraph(x)$ is equal to $\adh(y)$.

We observe that the sizes of all bag graphs roughly sum up to the size
of the graph $G$.

Let $\Tt=(T,\bag)$ be a regular tree decomposition of a graph $G$,
say of adhesion $a$. Then

$$\sum_{x\in V(T)} |\bgraph(x)|\leq (a+2)|G|\qquad\textrm{and}\qquad \sum_{x\in V(T)} \|\bgraph(x)\|\leq \|G\|+(a+2)^2|G|.$$

For the bound on $\sum_{x\in V(T)} |\bgraph(x)|$, observe the vertex
set of $\bgraph(x)$ is the disjoint union of $\adh(x)$, $\mrg(x)$,
and $\children(x)$. Every adhesion has size at most $a$, every node
of $T$ has at most one parent, and every vertex of $G$ is in exactly
one margin. Finally, $|T|\leq |G|$, hence

$$\sum_{x\in V(T)} |\bgraph(x)|\leq a|T|+|G|+|T|\leq (a+2)|G|.$$

For the bound on $\sum_{x\in V(T)} \|\bgraph(x)\|$, call an edge
$uv\in E(\bgraph(x))$ vital in the graph $\bgraph(x)$ if
$u,v\in \mrg(x)$.  Note that every edge of $G$ is vital in at most
one bag graph $\bgraph(x)$, hence the sum over all $x\in V(T)$ of the
number of vital edges in $\bgraph(x)$ is at most $|E(G)|$. On the
other hand, the non-vital edges of $\bgraph(x)$ are those incident to
the vertices of $\adh(x)$ and those incident to the children of
$x$. The total number of non-vital edges of the first kind is at most
$a\cdot |\bgraph(x)|$, as $|\adh(x)|\leq a$, and the total number of
edges of the second kind is at most $a\cdot |\children(x)|$, as every
child of $x$ has degree at most $a$ in $\bgraph(x)$. We conclude that

\begin{eqnarray*}
\sum_{x\in V(T)} \|\bgraph(x)\| & \leq & \sum_{x\in V(T)} |\bgraph(x)|+|E(G)|+a\cdot \sum_{x\in V(T)} \left(|\bgraph(x)|+|\children(x)|\right) \\
& \leq & (a+2)|G|+|E(G)|+a(a+2)|G| +a|T|\\
& \leq & \|G\|+(a+2)^2|G|.
\end{eqnarray*}

This concludes the proof.

We observe that topological-minor-freeness of $G$ carries over to bag

Let $\Tt=(T,\bag)$ be a regular tree decomposition of a graph $G$,
say of adhesion $a$. Suppose further that $G$ is
$K_t$-topological-minor-free. Then for each $x\in V(T)$, the graph
$\bgraph(x)$ is -minor-free, where

Suppose there is a topological minor model $\eta$ of $K_{t'}$ in
$\bgraph(x)$. Observe that no child of $x$ can be in the image of
the vertex set of $K_{t'}$ under $\eta$, for these vertices have
degree at most $a$ in $\bgraph(x)$ while $t'\geq a+2$. Therefore,
the only way any $y\in \children(x)$ can participate in the image of
$\eta$ is that $y$ is an internal vertex of a path $\eta(e)$, for
some edge $e$ of $K_{t'}$.

We construct a topological minor model $\eta'$ of $K_{t'}$ in
$G[\cone(x)]$ as follows:

* For each $u\in V(K_{t'})$, set $\eta'(u)=\eta(u)$.

* For each $e\in E(K_{t'})$, construct $\eta'(e)$ from $\eta(e)$
by replacing, for each $y\in \children(x)$, the subpath $u-y-v$,
where $u,v\in \bag(x)$ are the neighbors of $y$ on $\eta(e)$, with
any $u$-$v$ path in $G[\cone(y)]$ whose interior is entirely
contained in $\cmp(y)$. Such a path exists by the assumption that
$\Tt$ is regular.

Since the paths in $\{\eta(e)\colon e\in E(K_{t'})\}$ are pairwise
internally vertex-disjoint and $\cmp(y)$ and $\cmp(y')$ are disjoint
for distinct $y,y'\in \children(x)$, it follows that the paths in
$\{\eta'(e)\colon e\in E(K_{t'})\}$ are also pairwise internally
vertex-disjoint. Thus, $\eta'$ is a topological minor model of
$K_{t'}$ in $G[\cone(x)]$, hence also in $G$; a contradiction.

Finally, we need an observation about how strong unbreakability of a
tree decomposition influences unbreakability properties of bag graphs.
For this, it will be convenient to work with another type of a bag
graph, defined as follows. Suppose $\Tt=(T,\bag)$ is a regular tree
decomposition of a graph $G$, $x$ is a node of $T$, and
$S\subseteq \cone(x)$. The $S$-restricted bag graph of $x$,
denoted $\bgraph_S(x)$, is the graph obtained from $\bgraph(x)$ by the
following operations:

* Remove every vertex of $S\cap \bag(x)$.

* For every $y\in \children(x)$, remove $y$ and for every pair of
vertices $\{u,v\}\in \binom{\adh(y)\setminus S}{2}$, add an edge
$uv$ provided it was not already there and in $G[\cone(y)]$ there
is a $u$-$v$ path that is disjoint with $S$.

For example, as $\Tt$ is regular, $\bgraph_\emptyset(x)$ is the graph
obtained from $\bgraph(x)$ by removing all $y\in \children(x)$ and,
for each of them, turning $\adh(y)$ into a clique.

Let $\Tt=(T,\bag)$ be a regular and strongly $(q,k)$-unbreakable
tree decomposition of a graph $G$. Let $x\in V(T)$ and
$S\subseteq \cone(x)$ be such that $|S|\leq k$. Then for any
$u,v\in \bag(x)\setminus S$, we have the following.

* Vertices $u$ and $v$ are connected in $G[\cone(x)]-S$ if and
only if they are connected in $\bgraph_S(x)$.

* If $u$ and $v$ are disconnected in $\bgraph_S(x)$, and
$C_u,C_v$ are the connected components of $\bgraph_S(x)$
containing $u$ and $v$, respectively, then either $|V(C_u)|\leq q$
or $|V(C_v)|\leq q$.

The first assertion follows directly from the construction, so we
focus on the second one.

Let $L$ consist of all vertices reachable in $G[\cone(x)]-S$ from
$u$, and let $R=\cone(x)\setminus (L\cup S)$. Thus,
$(L\cup S,R\cup S)$ is a separation in $G[\cone(x)]$ of order
$|S|\leq k$. From the first assertion it follows that
$V(C_u)\subseteq L$ and $V(C_v)\subseteq R$. As
$V(C_u),V(C_v)\subseteq \bag(x)$, from the strong
$(q,k)$-unbreakability of $\Tt$ we conclude that either
$|V(C_u)|\leq q$ or $|V(C_v)|\leq q$.

Connectivity queries.
Suppose $G$ is a graph, $k$ an integer, $s$ and $t$ are vertices of
$G$, and $S$ is a set of $k$ vertices $u_1,\ldots,u_k$ of $G$.  We say
that $\conn_k(s,t,u_1,\ldots,u_k)$ holds in $G$ if and only if in $G$
there is an $s$-$t$ path that does not pass through any vertex of
$S$. Note that in particular, $\conn_k(s,t,u_1,\ldots,u_k)$ does not
hold if $\{s,t\}\cap S\neq \emptyset$. We may also write

§.§ Logic

We will only consider finite relational signatures $\Sigma$ consisting
of unary (arity $1$) and binary (arity $2$) relation symbols.  A
signature consisting only of unary relation symbols will be called an
alphabet. A $\Sigma$-structure $\str A$ consists of a finite universe
$V(\str A)$ and an interpretation $R(\str A)\subseteq V(\str A)^m$ of
each $m$-ary relation symbol $R\in\Sigma$. When there is no ambiguity,
we will not distinguish between relation symbols and their

Graphs are represented as $\Sigma$-structures where the universe is
the vertex set and $\Sigma$ consists of one binary relation symbol
$E(\cdot,\cdot)$, interpreted as the edge relation.

First-order logic ().
We assume an infinite supply $\textsc{Var}_1$ of first-order variables
and an infinite supply $\textsc{Var}_2$ of second-order set
variables. First-order variables will always be denoted by small
letters $x,y,z,\ldots$, while second-order variables will be denoted
by capital letters $X,Y,Z,\ldots$.

For a fixed signature $\Sigma$, formulas of first-order logic ($\FO$)
are constructed from atomic formulas of the form $x=y$, where
$x,y\in \textsc{Var}_1$, and $R(x_1,\ldots, x_m)$, where $R\in \Sigma$
is an $m$-ary relation symbol and $x_1,\ldots, x_m\in \textsc{Var}_1$,
by applying the Boolean operators $\neg$, $\wedge$ and $\vee$, and
existential and universal quantification $\exists x$ and $\forall x$.

A variable $x$ not in the scope of a quantifier is a free variable (we
will not consider formulas with free set variables). A formula without
free variables is a sentence.

We write $\phi(\tup x)$ to indicate that the free variables of a
formula $\phi$ are contained in the set of variables $\tup x$. A
valuation of $\tup x$ in a set $A$ is a function
$\tup a\from\tup x\to A$. Let $A^{\tup x}$ denote the set of all
valuations of $\tup x$ in $A$.

The satisfaction relation between $\Sigma$-structures and formulas is
defined as usual by structural induction on the formula. When $\str A$
is a $\Sigma$-structure, $\phi(\bar x)$ is a formula with free
variables contained in $\bar x$, and $\bar a\in V(\str A)^{\bar x}$ is
a valuation of $\bar x$, we write
$(\str A,\bar a)\models \phi(\bar x)$ or $\str A\models\phi(\bar a)$
to denote that $\phi$ holds in $\str A$ when the variables are
evaluated by $\bar a$. We let
$\phi(\str A):=\{\tup a\in A^{\tup x}~|~\str A\models \varphi(\tup

Separator logic ().
Assume that $\Sigma$ contains a distinguished binary relation symbol
$E(\cdot,\cdot)$ that will always be interpreted as the edge relation
of a graph, that is, as an irreflexive and symmetric relation. For a
$\Sigma$-structure $\str A$, write $G(\str A)$ for the graph
$(V(\str A), E(\str A))$.  Separator logic () is
first-order logic extended by the predicates
$\conn_k(x,y,z_1,\ldots,z_k)$, for all $k\ge 0$, where
${x,y,z_1,\ldots,z_k\in \textsc{Var}_1}$. The satisfaction relation
between $\Sigma$-structures and $\FOsep$ formulas is as for
first-order logic, where the atomic formula
$\conn_k(x,y,z_1,\ldots,z_k)$ holds in a $\Sigma$-structure $\str A$
with a valuation $\tup a$ of the variables $x,y,z_1,\ldots,z_k$ to
elements $s,t,u_1,\ldots,u_k\in V(\str A)$, if:

${G(\str A)\models \conn_k(s,t,u_1,\ldots,u_k)}$.

Monadic second-order logic ().

Monadic second-order logic ($\MSO$) extends $\FO$ by existential and
universal quantification $\exists X$ and $\forall Y$ over second-order
set variables. We will consider $\MSO$ formulas over the signature
$A\cup \{\preceq\}$, where $A$ is a finite alphabet and $\preceq$ is a
binary relation symbol that will always be interpreted as the ancestor
relation in a tree. By $\MSO(\preceq,A)$ we denote the set of $\MSO$
formulas over such signatures.

Hence, formulas of $\MSO(\preceq,A)$ will only be evaluated over
rooted trees (represented by the ancestor relation $\preceq$)
decorated with predicates from $A$, and the semantics are defined as
usual by structural induction on the formula.

First-order logic with  atoms. We will also consider
formulas with restricted  atoms.  Fix a signature $\Sigma$
and an alphabet $A$.  The logic $\FO(\MSO(\preccurlyeq, A), \Sigma)$
denotes first-order logic over signature $\Sigma$ where in addition to
the standard syntax, one can use formulas of $\MSO(\preceq,A)$ as
atomic formulas. Semantics are defined as expected.

§ CONNECTIVITY QUERIES IN GENERAL GRAPHS: PROOF OF <REF>

In this section we prove <ref>.

The first step of the construction of the data structure is to apply
the algorithm of <ref> to compute, in time
$2^{\Oh(k^2)}\cdot |G|^2\cdot \|G\|$, a strongly $(q,k)$-unbreakable
tree decomposition $\Tt=(T,\bag)$ of $G$ of adhesion at most $q$,
where $q=q(k)=2^{\Oh(k)}$. As argued, we may assume that $\Tt$ is
regular. We fix the parameters $k$ and $q$ for the remainder of this

§.§ Basic ingredients

Before we proceed to the main construction, we need to set up some
auxiliary data structures that enable us to navigate and query the
tree decomposition $\Tt$.

We will need the following lemma for navigation in $T$. Recall that we
write $\lca(x,y)$ for the least common ancestor of $x$ and $y$ in $T$
and $\dir(x,y)$ (if $x$ is a strict ancestor of $y$) for the unique
child $y'$ of $x$ that is an ancestor of $y$. The proof of the
following lemma relies on the classic data structure for
$\lca(\cdot,\cdot)$ queries of Harel and Tarjan [23].

Given a tree $T$, one can compute in time $\Oh(|T|)$ a data
structure that may answer the $\lca(x,y)$ and $\dir(x,y)$ queries in
time $\Oh(1)$.

For the $\lca(\cdot,\cdot)$ queries we may
use the data structure of Harel and Tarjan [23], which
can be initialized in time $\Oh(|T|)$ and supports queries in
constant time. We now show that we can use this data structure as
well for the $\dir(\cdot,\cdot)$ queries.

For every node $x$ of $T$, arbitrarily enumerate the children of $x$
with numbers $1,\ldots,d(x)$, where $d(x)$ is the number of children
of $x$. By applying a linear-time preprocessing, we may assume that
every $x$ is supplied with an array of length $d(x)$ containing
pointers to its children, in this order.  Construct a tree $T'$ from
$T$ as follows:

* Replace every node $x$ with a path consisting of nodes
$(x,0),(x,1),\ldots,(x,d(x))$, where $(x,i)$ is the parent of
$(x,i-1)$ for each $i\in \{1,\ldots,d(x)\}$.

* For each $i\in \{1,\ldots,d(x)\}$, if $y$ is the $i$th child
of $x$ in $T$, then we make $(y,d(y))$ a child of $(x,i)$.

See <ref> for an illustration. Note that the number of nodes of $T'$
is upper bounded by the total number of nodes and edges of $T$,
hence $|T'|<2|T|$.

Construction of $T'$ from $T$ in the proof of Lemma <ref>. A node $v$ of degree $d$ is replaced by a path $(v,d),\ldots,(v,1)$ of $d$ nodes of degree  $2$, followed by a leaf node $(v,0)$.
If $u$ is a descendant of $v$ in $T$, then
$\dir(v,u)$ can be deduced from $\lca((u,0),(v,0))$ in $T'$.

The following claim is clear.

If $x$ is a strict ancestor of $y$ in $T$, then the least common
ancestor of $(x,0)$ and $(y,0)$ in $T'$ is the node $(x,i)$ such
that $\dir(x,y)$ is the $i$th child of $x$ in $T$.

Hence, if we set up the data structure of Harel and Tarjan for the
tree $T'$, then a $\dir(x,y)$ query in $T$ can be answered as
follows: compute the least common ancestor of $(x,0)$ and $(y,0)$ in
$T'$, read its second coordinate $i$, and output the $i$th child of
$x$ in $T$. This takes time $\Oh(1)$.

Next, we set up a data structure to encode and quickly evaluate
connectivity in subgraphs that are “between” the adhesion of two
nodes. These subgraphs are defined by the following notion of

*Torsos. For a graph $H$ and a subset of its vertices $X$,
the torso of $X$ in $H$ is the graph $\torso_H(X)$ on vertex
set $X$ where a pair of vertices $u,v\in X$ is adjacent if and only if
in $H$ there exists a $u$-$v$ path whose interior is disjoint with
$X$. For a pair of nodes $x$ and $y$ of $T$, where $x$ is an ancestor
of $y$, we define

$$\torso(x,y)\coloneqq \torso_{G[\cone(x)\setminus \cmp(y)]}(\adh(x)\cup \adh(y)).$$

Note that $\torso(x,y)$ is a graph on the vertex set
$\adh(x)\cup \adh(y)$, which comprises of at most $2q$ vertices.
Intuitively, $\torso(x,y)$ encodes the connectivity pattern between
the elements of $\adh(x)$ and of $\adh(y)$ within the subgraph induced
by the context in $\Tt$ between $x$ and $y$.

We will need a data structure for evaluating the torsos quickly.

One can compute in time $2^{\Oh(q^2)}\cdot |G|^2\cdot \|G\|$ a data
structure that can answer the following query in time
$2^{\Oh(q^2)}$: for given $x,y\in V(T)$, where $x$ is an ancestor of
$y$, output the graph $\torso(x,y)$.  The data structure takes space
$2^{\Oh(q^2)}\cdot |G|$.

The proof of <ref> is postponed to
<Ref>. Here is a quick sketch. By
appropriately coloring the vertices of the adhesions with colors from
$\{1,\ldots,q\}$, we can reinterpret each graph $\torso(x,y)$ as an
element of a semigroup of size $2^{\Oh(q^2)}$, in the same way as was
done in [9]. Then $\torso(x,y)$ can be obtained as
the semigroup product of the graphs $\torso(z_{i-1},z_{i})$ for
$i=1,\ldots,\ell$, where $x=z_0-z_1-\ldots-z_\ell=y$ is the path from
$x$ to $y$ in $T$. We design a data structure for path product queries in semigroup-labeled
trees. We believe that this data structure is a general tool of
independent interest, hence we actually give two different proofs. The
first one is based on a classic approach using deterministic Simon's
factorization of Colcombet [13], and can be viewed as a
reinterpretation of ideas from [13]. The second is a
self-contained, simpler argument that seems new.

§.§ Data structure

With the basic ingredients in place, we may proceed with the proof of
<ref>. Let us describe the data structure we are
going to use. It consists of:

* The tree decomposition $\Tt$, constructed using the algorithm of
<ref>, with underlying tree $T$. Each
vertex $u\in V(G)$ has a pointer to the unique node $x\in V(T)$ such
that $u\in \mrg(x)$.

* For each $x\in V(T)$, the $\emptyset$-restricted bag graph

* The data structure for $\lca(x,y)$ and $\dir(x,y)$ queries,
provided by <ref>. Call it $\Lb$.

* The data structure for $\torso(x,y)$ queries, provided by
<ref>. Call it $\Db$.

As for initialization, the time needed to compute $\Tt$ is
$2^{\Oh(k^2)}\cdot |G|^2\cdot \|G\|$. It is straightforward to see
that for each particular $x\in V(T)$, the graph $\bgraph_\emptyset(x)$
can be computed in time
$\Oh(q^{\Oh(1)}\cdot \|G\|)=2^{\Oh(k)}\cdot \|G\|$, hence the
construction of those graphs takes time
$2^{\Oh(k)}\cdot |G|\cdot \|G\|$ in total. The time needed to
construct $\Db$ is
$2^{\Oh(q^2)}\cdot |G|^2\cdot \|G\|=2^{2^{\Oh(k)}}\cdot |G|^2\cdot
\|G\|$. Finally, the time needed to construct $\Lb$ is
$\Oh(|V(T)|)\leq \Oh(|G|)$. All in all, the total initialization time
is $2^{2^{\Oh(k)}}\cdot |G|^2\cdot \|G\|$, as promised.

We now estimate the space usage of the data structure. The data
structures $\Lb$ and $\Db$ take space $\Oh(|T|)\leq \Oh(|G|)$ and
$2^{\Oh(q^2)}\cdot |T|\leq 2^{2^{\Oh(k)}}\cdot |G|$, respectively, by
<ref> and <ref>. By
<ref>, we have
$\sum_{x\in V(T)} |\bag(x)|\leq \Oh(q|G|)\leq 2^{\Oh(k)}\cdot |G|$,
hence the total size of the description of the tree decomposition
$\Tt$ is $2^{\Oh(k)}\cdot |G|$ as well. Finally, by
<ref> we have
$\sum_{x\in V(T)} \|\bgraph(x)\|\leq \Oh(q^2|G|)$. Recall that
$\bgraph_\emptyset(x)$ is obtained from $\bgraph(x)$ by removing all
the children of $x$ and turning their neighborhoods into cliques. As
each of these neighborhoods has size at most $q$ and
$\sum_{x\in V(T)}|\children(x)|\leq |T|\leq |G|$, we conclude that
these operations add at most $\binom{q}{2}\cdot |G|$ edges to graphs
$\bgraph_\emptyset(x)$ in total. It follows that
$\sum_{x\in V(T)} \|\bgraph(x)\|\leq \Oh(q^2|G|)$, so storing the
graphs $\bgraph_\emptyset(x)$ takes $\Oh(q^2|G|)=2^{\Oh(k)}\cdot |G|$
space. This concludes the analysis of the space complexity.

Before continuing, we need to clarify how exactly each graph
$\bgraph_\emptyset(x)$, for $x\in V(T)$, is represented in the data

The edges of $G$ can be partitioned into original edges —
those existing in $G[\bag(x)]$ — and adhesion edges — edges
$uv$ that are not present in $G[\bag(x)]$, but for which there exists
$y\in \children(x)$ with $\{u,v\}\subseteq \adh(y)$. In the latter
case we say that $y$ supports the adhesion edge $uv$. The edge
set of $\bgraph_\emptyset(x)$ is stored as usual using neighborhood
lists: every vertex is supplied with a list of edges incident to
it. However, for every edge on this list we remember whether it is an
original or an adhesion edge, and in the latter case we also remember
the list of all children of $x$ supporting the edge. It is easy to see
that this representation of $\bgraph_\emptyset(x)$ can be computed and
stored within the time and space complexity claimed above.

§.§ Implementation of queries

We are left with implementing connectivity queries using the data
structure described above. Suppose we are given a query $\conn(u,v,S)$
to answer, where $u,v\in V(G)$ and $S$ is a vertex subset of size at
most $k$.  Let $\Sh\coloneqq S\cup \{u,v\}$. Note that
$|\Sh|\leq k+2$.

For $x\in V(T)$, let

$$D(x)\coloneqq \adh(x)\cup (\{u,v\}\cap \cone(x)).$$

The profile of $x$ is the set
$\profile(x)\subseteq\binom{D(x)}{2}$ consisting of all pairs
$\{a,b\}\in \binom{D(x)}{2}$ satisfying the following condition: in
$G[\cone(x)]$ there is an $a$-$b$ path that does not pass through any
vertex of $S$.

Let $r$ be the root of $T$. Then $D(r)=\{u,v\}$ and $\profile(r)$ is
non-empty if and only if . Therefore, it
suffices to compute $\profile(r)$. We will do this by computing the
profiles of a selection of $\Oh(k)$ nodes of $T$ in a bottom-up

Precisely, let

$$X\coloneqq \set{r}\cup \setof{x\in V(T)}{\mrg(x)\cap \Sh\neq \emptyset}.$$

Note that $|X|\leq k+3$ and $X$ can be computed in time $\Oh(k)$,
because every vertex of $G$ has a pointer to the node of $T$ whose
margin contains it. Further, let

$$Y\coloneqq \textrm{least common ancestor closure of }X;$$

that is, $Y$ comprises of $X$ and all least common ancestors of pairs of nodes from $X$. Then

\[|Y|\leq 2|X|-1\leq 2k+5\]
and $Y$ is closed under taking least
common ancestors. Note that $Y$ can be computed in time $\Oh(k^2)$
using the data structure $\Lb$. Our goal is to compute

\[\profile(x)\quad \textrm{for each}\quad x\in Y\]

in a bottom-up manner. Each set $\profile(x)$ is stored as a list;
note that its size is at most $\binom{q+2}{2}=\Oh(q^2)$.

The next two lemmas provide the main ingredients for the
computation. Here, we say that a node $x$ of $T$ is affected if
$\cmp(x)$ contains a vertex of $\Sh$, and $x$ is unaffected

Suppose $z$ is an ancestor of $y$ in $T$, and $\Sh$ is disjoint with
$\cmp(z)\setminus \cone(y)$. Then given $\profile(y)$, one can
compute $\profile(z)$ using one query to the data structure $\Db$
and $q^{\Oh(1)}$ additional time.

Using a query to $\Db$, compute $\torso(z,y)$. Construct a graph $J$
on vertex set $D(y)\cup \adh(z)$ by defining the edge set of $J$ to
be the union of $\profile(y)$ and the edge set of
$\torso(z,y)$. Note that $|V(J)|\leq 2q+2$ and $D(z)\subseteq
V(J)$. The following claim is clear from the construction and the
assumption that $\Sh$ is disjoint with $\cmp(z)\setminus \cone(y)$.

For every pair of vertices $a,b\in V(J)$, there is an $a$- $b$
path in $G[\cone(z)]$ that does not pass through any vertex of $S$
if and only if there is such a path in the graph $J$.

Therefore, for every pair $\{a,b\}\in \binom{D(z)}{2}$, we can find
out whether $\{a,b\}\in \profile(z)$ using a breadth-first search in
$J$.  Since $J$ had $\Oh(q)$ vertices and hence $\Oh(q^2)$ edges,
this takes $\Oh(q^2)$ time per pair, hence $\Oh(q^4)$ time in total.

Let $x$ be a node of $T$. Suppose we are given the set $Z$
comprising of all affected children of $x$ and, for each $z\in Z$,
we are given $\profile(z)$. Then one can compute $\profile(x)$ in
time $q^{\Oh(1)}$.

Note that this statement holds in particular when $x$ has no affected

Note that since the components at the children of $Z$ are pairwise
disjoint, we have
$$|Z|\leq |\Sh|\leq k+2.$$

Recall that the data structure contains the $\emptyset$-restricted
bag graph $\bgraph_\emptyset(x)$, represented as described at the
end of <ref>. We now show that we can emulate
the neighborhood lists of the $S$-restricted bag graph
$\bgraph_S(x)$ using this representation.

Given $a\in \bag(x)\setminus S$, one can in time $q^{\Oh(1)}$
either conclude that the degree of $a$ in $\bgraph_S(x)$ is larger
than $q$, or list all the neighbors of $a$ in $\bgraph_S(x)$.

Note that $\bgraph_S(x)$ is a subgraph of
$\bgraph_\emptyset(x)$. Therefore, it suffices to iterate over the
neighborhood list of $a$ in $\bgraph_\emptyset(x)$ and for each
edge $ab$ on this list, decide whether it is present in

Note that the edge $ab$ is not present in $\bgraph_S(x)$ if and
only if at least one of the following conditions holds:

* $b\in S$; or

* $ab$ is an adhesion edge and for every node $z$ supporting
$ab$, we have $z\in Z$ and $\{a,b\}\notin \profile(z)$.

We observe that the second condition can be checked in time
$q^{\Oh(1)}$. Indeed, since $|Z|\leq k+2$, if there are more than
$k+2$ nodes supporting $ab$, then the condition must be
false. Otherwise we can iterate through the list of all nodes $z$
supporting $ab$ (stored along with $ab$ in the representation of
$\bgraph_\emptyset(x)$), and for each of them check whether it
belongs to $Z$ and satisfies $\{a,b\}\notin
\profile(z)$. Implemented in a straightforward way, this takes
time polynomial in $q$.

Hence, for every particular edge $ab$ present in
$\bgraph_\emptyset(x)$ we can decide whether it is present also in
$\bgraph_S(x)$ in time $q^{\Oh(1)}$. The next observation is that
only for at most $(k+2)\binom{q}{2}$ edges this check will yield a
negative answer. Indeed, at most $|S|\leq k$ edges $ab$ may not be
present in $\bgraph_S(x)$ due to $b\in S$, and every $z\in Z$
supports at most $\binom{|\adh(z)|}{2}\leq \binom{q}{2}$ edges,
resulting in at most
$|Z|\cdot \binom{q}{2}\leq k+(k+2)\binom{q}{2}$ edges $ab$ not
being present in $\bgraph_S(x)$ due to the second
condition. Therefore, if the degree of $a$ in
$\bgraph_\emptyset(G)$ is larger than $q+k+(k+2)\binom{q}{2}$,
then its degree in $\bgraph_S(G)$ must be larger than $q$, and we
may report this outcome without analyzing the neighborhood list of
$a$. Otherwise, we process all the $\Oh(q^2k)$ edges incident to
$a$ in $\bgraph_\emptyset(G)$, and for each of them we decide
whether it is present in $\bgraph_S(G)$ in time $q^{\Oh(1)}$. This
results in listing all edges incident to $a$ in $\bgraph_S(G)$ in
time $q^{\Oh(1)}$.

The next claim is the key observation: connectivity in
$\bgraph_S(x)$ can be decided in time $q^{\Oh(1)}$, and the crux is
to use <ref>.

Given $a,b\in \bag(x)\setminus S$, one can decide whether $a$ and
$b$ are connected in $\bgraph_S(x)$ in time $q^{\Oh(1)}$.

By <ref>, the following algorithm
solves this problem:

* Run a breadth-first search from $a$ in $\bgraph_S(x)$,
terminating the search whenever any of the following conditions
is met (by reaching a vertex we mean that it is added to
the bfs queue):

* $b$ has been reached;

* a vertex of degree larger than $q$ in $\bgraph_S(x)$ is
popped from the queue;

* in total, the search has reached $q+1$ vertices.

If the search terminated due to the queue being empty before any
of the conditions above is met, conclude that $a$ and $b$ are not
connected in $\bgraph_S(x)$.

* Do the same with the roles of $a$ and $b$ swapped.

* If neither of the steps above reached the conclusion that $a$
and $b$ are not connected in $\bgraph_S(x)$, then conclude that
$a$ and $b$ are connected in $\bgraph_S(x)$.

Note here that the second termination condition stated above —
when a vertex of degree larger than $q$ is popped from the queue
— is also correct for the following reason: such a vertex
witnesses that the connected component of $\bgraph_S(x)$ on which
the search is employed has more than $q$ vertices.

Now it is straightforward to see that the algorithm presented above
can be implemented in time $q^{\Oh(1)}$ with the help of
<ref>. Namely, when in a breadth-first search a
vertex $w$ is popped from the queue, we need to iterate through all
the neighbors of $w$ and add them to the queue provided they were
not reached before. By <ref>, we can either list
those neighbors in time $q^{\Oh(1)}$ or conclude that the search
can be immediately terminated. Since the search will not reach more
than $q+1$ vertices in total, for each of those neighbors we can
check whether it was already reached in time $\Oh(q)$. At most
$q+1$ vertices will be processed in this way, resulting in the
total time complexity of $q^{\Oh(1)}$.

Now observe that for every pair
$\{a,b\}\in \binom{D(x)\cap \bag(x)}{2}$, $\{a,b\}$ should be
included in $\profile(x)$ if and only if $a$ and $b$ are connected in
$\bgraph_S(x)$; this follows from
<ref>. We can use <ref> to
decide this in time $q^{\Oh(1)}$ per pair, so also also in time
$q^{\Oh(1)}$ for all such pairs in total.

We are left with making the same decision for pairs
$\{a,b\}\in \binom{D(x)}{2}$ where either $a$ or $b$ is contained in
$D(x)\setminus \bag(x)$. Noting that
$D(x)\setminus \bag(x)\subseteq \{u,v\}$, by symmetry suppose that
$a=u$ and $u\notin \bag(x)$. Let $z$ be the child of $x$ satisfying
$u\in \cmp(z)$. Note that $z=\dir(x,y)$ where $y$ is such that
$u\in \mrg(y)$, hence $z$ can be computed in time $\Oh(1)$ using a
query to $\Lb$.

Suppose first that $b\in \bag(x)$. Then $\{u,b\}$ should be included
in $\profile(x)$ if and only if there exists $w\in D(z)$ such that
$\{u,w\}\in \profile(z)$ and $w,b$ are connected in
$\bgraph_S(x)$. This condition can be checked in time $q^{\Oh(1)}$
for each particular $w\in \adh(z)$ using the algorithm of
<ref>, hence every pair $\{u,b\}$ as above can be
decided in time $q^{\Oh(1)}$. There are $\Oh(q)$ vertices
$b\in D(x)\cap \bag(x)$ to check, hence these pairs can be decided in
total time $q^{\Oh(1)}$.

Finally, we are left with the case when $b=v$ and $v\notin
\bag(x)$. Let $z'$ be the child of $x$ such that $v\in \cmp(z')$;
similarly as before, we can find $z'$ in time $\Oh(1)$ using
$\Lb$. Then $\{u,v\}$ should be included in $\profile(x)$ if and only
if at least one of the following conditions is satisfied:

* $z=z'$ and $\{u,v\}\in \profile(z)$.

* There exist $w\in \adh(z)$ and $w'\in \adh(z')$ such that
$\{u,w\}\in \profile(z)$, $\{w',v\}\in \profile(z')$, and $w,w'$
are connected in $\bgraph_S(x)$.

The first condition can be checked in time $\Oh(q^2)$, while the
second can be checked in time $q^{\Oh(1)}$ by applying the algorithm
of <ref> for every pair
$(w,w')\in \adh(z)\times \adh(z')$.

Altogether, we have decided which pairs of $\binom{D(x)}{2}$ should be
included in $\profile(x)$ in time $q^{\Oh(1)}$ and the proof is

We may now implement the $\conn(u,v,S)$ query using <ref>
and <ref>. Let $T_Y$ be the tree on node set $Y$ with
the ancestor order inherited from $T$; that is, $x$ is the parent of
$y$ in $T_Y$ if $x$ is a strict ancestor of $y$ in $T$ and the
interior of the $x$-$y$ path in $T$ is disjoint with $Y$. Note that
$T_Y$ can be constructed in time $\Oh(k^2)$ using the data structure

Now, we compute $\profile(x)$ for all $x\in Y$ in a bottom-up manner
over $T_Y$. Let $y_1,\ldots,y_\ell$ be the children of $x$ in $T_Y$
(possibly $\ell=0$ if $x$ is a leaf of $T_Y$). For each
$i\in \{1,\ldots,\ell\}$, let

$$z_i\coloneqq \dir(x,y_i).$$

Note that each $z_i$ can be found in time $\Oh(1)$ using a query to
$\Lb$, hence computing $z_1,\ldots,z_\ell$ takes time $\Oh(k)$. The
following claim follows immediately from taking $Y$ to be the least
common ancestor closure of $X$.

For each $i\in \{1,\ldots,\ell\}$, $\Sh$ is disjoint with
$\cmp(z_i)\setminus \cone(y_i)$.

Note that the profiles $\profile(y_i)$ for $i\in \{1,\ldots,\ell\}$ have
already been computed before. Therefore, we may apply <ref>
$\ell$ times to compute the profiles $\profile(z_i)$ for
$i\in \{1,\ldots,\ell\}$, each using one query to $\Db$ and
$q^{\Oh(1)}$ additional time.

Finally, observe that $z_1,\ldots,z_\ell$ are precisely the affected
children of $x$. Therefore, we may apply <ref> to
compute $\profile(x)$ in time $q^{\Oh(1)}$. Remember that this works in
particular when $x$ is a leaf of $T_Y$ and has no affected children.

At the end we compute $\profile(r)$ for $r$ being the root of $T$. As
we argued, $G\models\conn(u,v,S)$ if and only if $\profile(r)$ is
non-empty, hence we may now answer the query.

As for the time complexity, the whole procedure uses $\Oh(k)$ queries
to $\Db$ and $q^{\Oh(1)}$ additional time. Since every query to $\Db$
takes time $2^{\Oh(q^2)}$, by <ref>, and $q=2^{\Oh(k)}$,
the total running time is bounded by a doubly-exponential function of
$k$, as promised. This concludes the proof of

§ TORSO QUERIES

In this section we give a proof of <ref>. As mentioned,
the main idea is to reinterpret torso queries as queries about
products along paths in a tree labeled with elements of a fixed finite
semigroup, and then design a data structure for this more general kind
of queries. We start by introducing the setting of semigroup-labeled
trees and showing how torso queries fit into this setting. Then we
design a data structure for path product queries in semigroup-labeled
trees. We believe that this data structure is a general tool of
independent interest, hence we actually give two different proofs. The
first one is based on a classic approach using deterministic Simon's
factorization of Colcombet [13], and can be viewed as a
reinterpretation of ideas from [13]. The second is a
self-contained, simpler argument that seems new.

*Semigroup-labeled trees and path product queries.
Recall that a semigroup $S$ consists of a set of elements, called the
support and also denoted by $S$, and a binary associative
operation on the support called the product and denoted
$\cdot$. A semigroup is finite if it has finite support.

For a semigroup $S$, an $S$-labeled tree is a rooted tree $T$ together with a map that with each edge $e$ of $T$ associates an element $\sigma(e)\in S$. Suppose $x,y$ are nodes of $T$, where $x$ is a strict ancestor of $y$. Then we define

\[\sigma(x,y)\coloneqq \sigma(e_1)\cdot \sigma(e_2)\cdot\ldots\cdot\sigma(e_\ell),\]

where $e_1,\ldots,e_\ell$ are the consecutive edges of the path from
$x$ to $y$ in $T$ (that is, $e_1$ is incident with $x$ and $e_\ell$ is
incident with $y$).

The following theorem is the main result of this section: it provides
an efficient data structure for path product queries, parameterized by
the size of the semigroup.

Fix a finite semigroup $S$ and suppose we are given an $S$-labeled
tree $T$. Then one can in time $|S|^{\Oh(1)}\cdot |T|$ construct a
data structure that can answer the following query in time
$|S|^{\Oh(1)}$ and using $|S|^{\Oh(1)}$ operations in $S$: given
nodes $x,y\in V(T)$, where $x$ is a strict ancestor of $y$, output
$\sigma(x,y)$. The data structure uses $|S|^{\Oh(1)}\cdot |T|$
memory and stores $|S|^{\Oh(1)}\cdot |T|$ elements of $S$.

Later we give two proofs of <ref>, but let us see
now how torso queries can be understood through path product queries
in a semigroup-labeled tree. That is, we are going to prove
<ref> assuming <ref>.

*Torso queries as path product queries. Assume the setting
from the statement of <ref>. We interpret torso queries
as path product queries over trees labeled with a finite semigroup of
size $2^{\Oh(q^2)}$. For this, we shall use the semigroup of
bi-interface graphs, introduced for a similar purpose
in [9].

Let $r\in \N$. A bi-interface graph of arity $r$ consists of a
graph $G$ and two partial mappings $\lft,\rgt\colon V(G)\partto [r]$
that are injective and satisfy the following property: if
$u\in \dom{\lft}\cap \dom{\rgt}$, then $\lft(u)=\rgt(u)$. The domains
of the mappings $\dom{\lft}$ and $\dom{\rgt}$ are called the left
interface and the right interface, respectively.

A bi-interface graph is basic if its vertex set is a subset of
$[r]\times \{\Lsf,\Rsf,\Ssf\}$,
$\dom{\lft}\setminus \dom{\rgt}\subseteq [r]\times \{\Lsf\}$,
$\dom{\rgt}\setminus \dom{\lft}\subseteq [r]\times \{\Rsf\}$,
$\dom{\lft}\cap \dom{\rgt}\subseteq [r]\times \{\Ssf\}$, and
$V(G)=\dom{\lft} \cup \dom{\rgt}$. By $\Basic_r$ we denote the set of
all basic bi-interface graphs of arity $r$. Note that

$$|\Basic_r|\leq 2^{\Oh(r^2)},$$

as this is an upper bound on the total number of different graphs on
vertex set $[r]\times \{\Lsf,\Rsf,\Ssf\}$.

Next, we define the abstraction operation, which takes a
bi-interface graph $\Gb=(G,\lft,\rgt)$ and outputs the basic
bi-interface graph $\abstr{\Gb}$, of same arity, defined as follows:

* First, for a vertex $u\in \dom{\lft}\cup \dom{\rgt}$, define
$\iota(u)$ as

$$ \iota(u) :=
\begin{cases}
(\lft(u),\Lsf) &\text{if } u\in \dom\lft\setminus \dom{\rgt},\\
(\rgt(u),\Rsf) &\text{if } u\in \dom\rgt\setminus \dom{\lft}, \text{and}\\
(\lft(u),\Ssf)=(\rgt(u),\Ssf) &\text{if } u\in \dom\lft\cap \dom{\rgt}.
\end{cases}

* The vertex set of $\abstr{\Gb}$ is
$\{\iota(u)\colon u\in \dom\lft \cup \dom{\rgt}\}$.

* In $\abstr{\Gb}$ there is an edge between $\iota(u)$ and
$\iota(v)$ if and only if in $G$ there is a path from $u$ to $v$
that does not pass through any other vertex of
$\dom{\lft}\cup \dom{\rgt}$.

* The interface mappings $\lft',\rgt'$ of $\abstr{\Gb}$ are
naturally inherited from $\Gb$: $\lft'(\iota(u))=\lft(u)$ for
$u\in \dom{\lft}$ and $\rgt'(\iota(u))=\rgt(u)$ for
$u\in \dom{\rgt}$.

Thus, intuitively speaking, $\abstr{\Gb}$ is obtained by applying the
torso operation in $\Gb$ with respect to the union of the interfaces,
and reindexing the vertices according to the labels assigned to the

Let $\Gb=(G,\lft_G,\rgt_G)$ and $\Hb=(H,\lft_H,\rgt_H)$ be two
bi-interface graphs of arity $r$. The composition of $\Gb$ and
$\Hb$ is the bi-interface graph $\Gb\cdot \Hb=(J,\lft_G,\rgt_H)$,
where $J$ is obtained from the disjoint union of $G$ and $H$ by fusing
a vertex $u\in \dom{\rgt_G}$ with a vertex $v\in \dom{\lft_H}$
whenever $\rgt_G(u)=\lft_H(v)$. Thus, bi-interface graphs of arity $r$
with the composition operation form an (infinite) semigroup; call it
$S_r$. We can now endow the basic bi-interface graphs of arity $r$
with composition operation $\odot$ defined as follows: for basic
bi-interface graphs $\Ab$ and $\Bb$, we set

\[\Ab\odot\Bb\coloneqq \abstr{\Ab\cdot \Bb}.\]

Thus, basic bi-interface graphs of arity $r$ endowed with $\odot$ form
a semigroup of size $2^{\Oh(r^2)}$; call this semigroup $B_r$. It is
straightforward to check that the abstraction operation
$\abstr{\cdot}$ is a semigroup homomorphism from $S_r$ to $B_r$, for
every $r\in \N$.

With the definitional layer introduced, we can state a lemma that
encapsulates the translation from torso queries to queries over
$B_q$-labeled trees. This lemma will be used not only in this section,
but also later on for the purpose of viewing computation of torsos in
algebraic terms.

Suppose we are given a tree decomposition $\Tt=(T,\bag)$ of a graph
$G$ of adhesion $q$. Then one can in time $q^{\Oh(1)}\cdot |T|\|G\|$
compute injective colorings
$\{\lambda_x\colon \adh(x)\to [2q]\colon x\in V(T)\}$ and a mapping
$\sigma\colon E(T)\to B_{2q}$ such that the following properties are

* If $x$ is the parent of $y$ in $T$, $u\in \adh(x)$, and
$v\in \adh(y)$, then

$$\lambda_x(u)=\lambda_y(v)\qquad\textrm{if and only if}\qquad u=v.$$

* If $x$ is a strict ancestor of $y$ in $T$, and we denote

$$\Gb(x,y)=(G[\cone(x)\setminus \cmp(y)],\lambda_x,\lambda_y),$$

then $\Gb(x,y)$ is a correctly defined bi-interface graph and

Compute the colorings $\lambda_x$ in a top-down manner as follows:

* If $r$ is the root of $T$, then $\adh(r)$ is empty, hence set
$\lambda_r$ to be the empty coloring.

* If $y$ is a child of $x$ and $\lambda_x$ has already been
defined, then construct $\lambda_y$ as follows: for each
$u\in \adh(x)\cap \adh(y)$ set
$\lambda_y(u)\coloneqq \lambda_x(u)$, and then color the vertices
of $\adh(y)\setminus \adh(x)$ using colors from
$[2q]\setminus \lambda_x(\adh(x))$ in an arbitrary injective
manner. Note that since $|\adh(x)|\leq q$, we have
$|[2q]\setminus \lambda_x(\adh(x))|\geq q$, so such an injective
coloring always exists.

That the colorings $\{\lambda_x\colon x\in V(T)\}$ satisfy the first
point from the lemma statement follows immediately from the
construction. Clearly, they can be computed in time $\Oh(q|T|)$ by
performing a depth-first search in $T$.

Next, for an edge $xy\in E(T)$, where $x$ is the parent of $y$, we construct

\[\sigma(xy)\coloneqq \abstr{\Gb(x,y)},\]

where $\Gb(x,y)$ is defined as in the lemma statement. Computing
$\sigma(xy)$ boils down to running a breadth-first search in
$\Gb(x,y)$ from each vertex of $\adh(x)\cup \adh(y)$; this can be
done in time $q^{\Oh(1)}\cdot \|G\|$ per node $y$, so in time
$q^{\Oh(1)}\cdot |T|\|G\|$ in total.

It remains to note that if $x$ is a strict ancestor of $y$ and
$x=z_0-z_1-\ldots-z_\ell=y$ is the path from $x$ to $y$ in $T$, then

$$\Gb(x,y)=\Gb(z_0,z_1)\cdot \Gb(z_1,z_2)\cdot\ldots\cdot \Gb(z_{\ell-1},z_\ell),$$

from which it follows that

\[\abstr{\Gb(x,y)}=\sigma(z_0z_1)\odot \sigma(z_1z_2)\odot \ldots
\odot \sigma(z_{\ell-1}z_\ell)=\sigma(x,y).\hfill\qedhere\]

Now <ref> follows directly from combining
<ref> and <ref>. More precisely,
using <ref> we compute the mapping $\sigma$ and
colorings $\{\lambda_x\colon x\in V(T)\}$, and then we set up the data
structure for $\sigma(x,y)$ queries provided by
<ref>. To answer a query about $\torso(x,y)$, we
first query this data structure to obtain $\sigma(x,y)$, and then we
translate the names of vertices from $[q]\times \{\Lsf,\Rsf,\Ssf\}$
back to $\adh(x)\cup \adh(y)$ by reverting the colorings $\lambda_x$
and $\lambda_y$.

We now proceed to <ref>. In both proofs we use the
following easy corollary of <ref>.

Given a tree $T$ and a set of nodes $L\subseteq V(T)$, one can in
time $\Oh(|T|)$ construct a data structure that may
answer the following query in time $\Oh(1)$: given nodes $x$ and
$y$, where $x$ is an ancestor of $y$ in $T$, find the topmost node
on the $x$-$y$ path in $T$ that belongs to $L$, or report that no
such node exists.

For every $x\in V(T)$, we store whether $x\in L$. Further, let
$\anc(x)$ be the closest (deepest) strict ancestor of $x$ that
belongs to $L$, or $\bot$ if no such ancestor exists. Note that the
values of $\anc$ can be computed in time $\Oh(|T|)$ using a
depth-first search in $T$.

Next, let $T_L$ be the rooted tree on node set $L\cup \{\bot\}$
constructed from $T$ as follows:

* Restrict the node set to $L$ keeping the ancestor relation;
that is, for $x,y\in L$ we have that $x$ is an ancestor of $y$ in
$T_L$ if and only if $x$ is an ancestor of $y$ in $T$. Thus, $T_L$
is now a rooted forest.

* Add a fresh root $\bot$ to $T_L$ and make all former roots of
$T_L$ into children of $\bot$.

Again, $T_L$ can be computed (through its parent relation) in time
$\Oh(|T|)$ by applying a depth-first search.

Apply <ref> to the tree $T_L$, thus constructing a
suitable data structure $\Lb$ in time $\Oh(|T|)$. It can be now
easily seen that whenever $x$ is an ancestor of $y$ in $T$, the
answer to the query from the lemma statement is equal to

where $\dir_{\Lb}(\cdot,\cdot)$ is a query to the data structure
$\Lb$. In case $\anc(x)=\anc(y)$, we report $y$ provided $y\in L$,
and otherwise we report that there is no node on the $x$-$y$ path
that belongs to $L$.

*Proof of <ref> using deterministic Simon's factorization.
We now give a proof that follows closely the combinatorial idea
presented by Colcombet in <cit.>. See also the
work of Kazana and Segoufin [25] that applies this idea in
the context of enumeration of $\MSO$ queries on trees. We need a few
definitions, which are taken directly from [13].

Fix a finite semigroup $S$. Let $P$ be an oriented path whose edges
are labeled by elements of $S$; let $\sigma\colon E(P)\to S$ be this
labeling. As $P$ is oriented, there is a natural order $<$ on $V(P)$
signifying which vertex is earlier. For two nodes $x<y$ of $P$, we
denote $\sigma(x,y)=\sigma(e_1)\cdot \ldots \cdot \sigma(e_\ell)$,
where $e_1,\ldots,e_\ell$ are the consecutive edges of the subpath of
$P$ from $x$ to $y$.

For $h\in \N$, a split of height $h$ of $P$ is a labeling
$\lambda\colon V(P)\to [h]$. In such a split $\lambda$, two nodes
$x<y$ of $P$ are called $i$-neighbors if
$\lambda(x)=\lambda(y)=i$ and $\lambda(z)\geq i$ for all $x<z<y$.
Clearly, being $i$-neighbors is an equivalence relation on
$\lambda^{-1}(i)$. Then the split $h$ is called forward Ramsey
if for all vertices $x,y,x',y'$ that are pairwise $i$-neighbors and
satisfy $x<y$ and $x'<y'$, we have

$$\sigma(x,y)\cdot \sigma(x',y')=\sigma(x,y).$$

Now let $T$ be a rooted tree with edges labeled by elements of $S$
through a labeling $\sigma\colon E(T)\to S$. Again, a split of height
$h$ of $T$ is a labeling $\lambda\colon V(T)\to [h]$. We say that such
a split is forward Ramsey if it is forward Ramsey when
restricting it to any root-to-leaf path in $T$. Here, the path is
oriented from the root to the leaf.

Colcombet's theorem states that in every tree there is always a
forward Ramsey split of height bounded by $|S|$. The following
statement follows easily from the results presented
in [13].

Let $T$ be a rooted tree with edges labeled by elements of a finite
semigroup $S$. Then there is a forward Ramsey split of $T$ of height
at most $|S|$. Moreover, such a split can be computed in time
$|S|^{\Oh(1)}\cdot |T|$.

To be more precise, Colcombet states his result in terms of the
existence of a forward Ramsey split on a path that can be computed by
a deterministic automaton that processes the path in the given order.
As in [13] and multiple other applications, the tree
variant stated above can be obtained by running the automaton on every
root-to-leaf path of the tree. For computing the split within the
promised time complexity, it suffices to construct the automaton in
time $|S|^{\Oh(1)}$ and run it on the root-to-leaf paths in $T$ using
depth-first search.

With <ref> recalled, we can proceed to the proof
of <ref>. Let $\lambda$ be a split of height
$h\coloneqq |S|$ for the input tree $T$, computed using the algorithm
of <ref>. With every $x\in V(T)$ we will store
the value $\lambda(x)$. Further, letting
$L_i\coloneqq \lambda^{-1}(i)$ for each $i\in [h]$, we apply
<ref> to $T$ and the node subset $L_i$, thus
obtaining a suitable data structure $\Kb_i$. Finally, we apply
<ref> to compute a suitable data structure $\Lb$ for
$\lca(\cdot,\cdot)$ and $\dir(\cdot,\cdot)$ queries. All of these take
time $|S|^{\Oh(1)}\cdot |T|$ in total.

Recall that within $\Kb_i$, with every $x\in V(T)$ we store a pointer
$\anc_i(x)$ to the closest (deepest) strict ancestor of $x$ that
belongs to $L_i$; if there is no such strict ancestor, $\bot$ is
stored instead. In case $\anc_i(x)$ is well-defined, alongside it we
also store the value
\[\val_i(x)\coloneqq \sigma(\anc_i(x),x)\in S.\]

Again, using a depth-first search it is straightforward to compute all
these values in time $|S|^{\Oh(1)}\cdot |T|$ and using
$|S|^{\Oh(1)}\cdot |T|$ operations in $S$.

This concludes the definition of the data structure. Clearly, the time
complexity of the construction algorithm, as well as the space
complexity, are as promised. We are left with implementing the
$\sigma(x,y)$ queries within the promised time complexity.

Let $x$ and $y$ be a pair of nodes of $T$, where $x$ is a strict
ancestor of $y$. Let $R(x,y)$ be the set of all nodes that lie on the
unique path from $x$ to $y$ in $T$, including $x$ but excluding $y$.
Further, let

\[r(x,y)\coloneqq \min \{\lambda(z)\colon z\in R(x,y)\}.\]

We are going to give an algorithm that computes $\sigma(x,y)$ in time
$|S|^{\Oh(1)}$ and using $|S|^{\Oh(1)}$ operations in $S$, and makes
at most one recursive call to compute $\sigma(x,z)$ for some $z$ that
is a strict ancestor of $y$ and a strict descendant of $x$. We will
have a guarantee that if such a call is invoked, then $r(x,z)>r(x,y)$.
Since the co-domain of $r(\cdot,\cdot)$ is $[h]$, this means that the
depth of the recursion is at most $h=|S|$, so the whole algorithm will
run within the promised complexity.

First, for every $i\in [h]$ we would like to test whether $R(x,y)$
contains a node $z$ with $\lambda(z)=i$, and if so, find the topmost
such node. This can be done using one call to the data structure
$\Kb_i$, applied to $x$ and the parent of $y$. Using this procedure
for each $i\in [h]$, we can determine the value of $r(x,y)$ in
time $\Oh(|S|)$, and also find the suitable node $z$: the topmost node
satisfying $\lambda(z)=r(x,y)$.

Next, we would like to determine whether there exists a node
$z'\in R(z,y)$, $z'\neq z$, such that $\lambda(z')=r(x,y)$, and if so,
to find the topmost such $z'$. Again, this can be done using one call
to the data structure $\Kb_{r(x,y)}$, applied to $z$ and the parent of

Finally, let

\[z''\coloneqq \anc_{r(x,y)}(y).\]

With these definitions in place, it can be readily seen that
$\sigma(x,y)$ can be expressed as

\begin{equation}\label{eq:split}
\sigma(x,y)=\sigma(x,z)\cdot \sigma(z,z')\cdot \sigma(z',z'')\cdot
\sigma(z'',y), \end{equation}
where the terms

* $\sigma(x,z)$ ought to be omitted if $x=z$;

* $\sigma(z,z')\cdot\sigma(z',z'')$ ought to be omitted if $z'$ does not exist (note that this implies that $z=z''$); and

* $\sigma(z',z'')$ ought to be omitted if $z'=z''$.

Now observe that we can compute the consecutive factors on
the right hand side of (<ref>) as follows:

* We have $\sigma(z'',y)=\val_i(y)$, and this value is stored
directly in the data structure.

* Similarly, provided $z'$ exists, $\sigma(z,z')=\val_i(z')$.
Furthermore, if $z'\neq z''$, then $z,z',z''$ are all
$r(x,y)$-neighbors on the root-to-$y$ path in $T$, hence
$\sigma(z,z')\cdot \sigma(z',z'') = \sigma(z,z')$ by the
forward-Ramseyanity of the split.

* Provided $x\neq z$, $\sigma(x,z)$ can be computed by a recursive call.
Here, observe that by the definition of $z$, no node of $R(x,z)$ is
assigned value $r(x,y)$ under $\lambda$, hence $r(x,z)>r(x,y)$, as
was promised.

Therefore, using (<ref>) we can compute $\sigma(x,y)$ using
one call to $\sigma(x,z)$ with $r(x,z)>r(x,y)$ and, additionally,
$|S|^{\Oh(1)}$ time and $|S|^{\Oh(1)}$ operations in $S$. This
concludes the proof of <ref>.

§ TRADING SPACE USAGE FOR QUERY COMPLEXITY

In this section we show how to modify the approach presented in
<ref> to construct a data structure that offers
queries in time $k^{\Oh(1)}$, at the cost of increasing the space
usage to quadratic in the size of the graph. The outcome is captured
in the following statement.

Given a graph $G$ and an integer $k$, one can in time
$2^{\Oh(k\log k)}\cdot |G|^{\Oh(1)}$ construct a data structure
that may answer the following queries in time $k^{\Oh(1)}$:
given $u,v\in V(G)$ and a set $S$ consisting of at most $k$ vertices
of $G$, does $G\models \conn(u,v,S)$? The space usage of the data
structure is $k^{\Oh(1)}\cdot |G|^2$.

Compared to <ref>, <ref> offers a
much faster implementation of queries: the complexity is polynomial in
$k$, instead of doubly-exponential. The drawback is that while the
space usage is also polynomial in $k$, the dependency on the total
number of vertices becomes quadratic. Note that the initialization
time still depends exponentially on $k$.

The remainder of this section is devoted to the proof of
<ref>. We will heavily rely on the approach presented in
<ref>, so we only discuss the modifications and
this section needs to be read in conjunction with

*The tree decomposition. The main idea of the proof is to
rely only on weak unbreakability, instead of strong unbreakability as
in <ref>. This reduces the sizes of adhesions
from exponential in $k$ to just $k$. More precisely, given the input
graph $G$ and the parameter $k$, we apply
<ref> to compute, in time
$2^{\Oh(k\log k)}\cdot |G|^{\Oh(1)}$, a tree decomposition $\Tt$ with
the following properties:

* the adhesion of $\Tt$ is at most $k$; and

* every bag of $\Tt$ is $(k,k)$-unbreakable in $G$.

Recall from the earlier discussion that we may assume that the
decomposition is regular. Obviously, the fact that $\Tt$ is only
weakly unbreakable renders the bulk of correctness argumentation
presented in <ref> invalid. Fixing this issue is
the main technical task of this section.

*Torso queries. Note that even though now the adhesion of
$\Tt$ is bounded by $q=k$, if we just used <ref> for
torso queries, we would still end up with exponential dependence on
$k$ in the query time. This can be mitigated by replacing the data
structure of <ref> with a trivial one that just
memorizes all the answers. The drawback is that the space usage
becomes quadratic in $|G|$, as this is the total number of different
torso queries that can be asked.

One can compute in time $q^{\Oh(1)}\cdot |G|^{2}\|G\|$ a data
structure that can answer the following query in time
$q^{\Oh(1)}$: for given $x,y\in V(T)$, where $x$ is an ancestor of
$y$, output the graph $\torso(x,y)$.
The data structure takes space $q^{\Oh(1)}\cdot |T|^2$.

Note that there are at most $\binom{|T|}{2}$ pairs $(x,y)\in V(T)^2$
such that $x$ is a strict ancestor of $y$ in $T$, and for each of
them $\torso(x,y)$ can be computed in time $q^{\Oh(1)}\cdot \|G\|$
by running a breadth-first search from each vertex of
$\adh(x)\cup \adh(y)$. Hence, all those graphs can be computed in
time $q^{\Oh(1)}\cdot |G|^{2}\|G\|$ and stored in a two-dimensional
table indexed by nodes of $T$, which takes space
$q^{\Oh(1)}\cdot |T|^2$. Upon query, the data structure just returns
the relevant graph $\torso(x,y)$.

We remark that in what follows, we could still use <ref>
instead of <ref>. This would result in a variant
of <ref> where the query time complexity would be
$2^{\Oh(k^2)}$ and the space usage would be $2^{\Oh(k^2)}\cdot \|G\|$.

*Dealing with weak unbreakability. The data structure for
<ref> is now the same as the one presented in
<ref>, except for the two modifications presented
above: we use <ref> instead of
<ref> for the computation of a tree
decomposition, and we use <ref> instead of
<ref> for torso queries.

It remains to show how, given this data structure, to implement a
$\conn(u,v,S)$ query, where $u,v\in V(G)$ and $S\subseteq V(G)$ is
such that $|S|\leq k$. The algorithm is actually exactly the
same as the one presented in <ref>. As argued
through <ref> and <ref>, this algorithm takes
time $q^{\Oh(1)}$ and uses $\Oh(k)$ queries to a data structure
supporting torso queries. Since now the torso queries
take $q^{\Oh(1)}$ time and $q=k$, it follows that the whole algorithm
runs in $k^{\Oh(1)}$ time. So we are left with arguing that the
outcome is still correct.

As in <ref>, let $X$ be the set of nodes of $T$
whose margins intersect $\wh{S}\coloneqq S\cup \{u,v\}$ (plus the root
of $T$), and let $Y$ be the least common ancestor closure of $X$.
Recall that the algorithm presented in <ref>
computes, for each $x\in Y$, the set
$\profile(x)\subseteq \binom{D(x)}{2}$, where
$D(x)=\adh(x)\cup (\{u,v\}\cap \cone(x))$, consisting of all pairs of
vertices of $D(x)$ that are connected in $G[\cone(x)]-S$.

The idea is that we relax the condition on what the algorithm computes
to the following over-approximation of $\profile(x)$. For a node
$x\in V(T)$, we say that $\Pi_x\subseteq \binom{D(x)}{2}$ is a
semi-correct profile at $x$ if the following two conditions
hold for all $\{a,b\}\in \binom{D(x)}{2}$:

* If $a$ and $b$ are connected in $G[\cone(x)]-S$, then
$\{a,b\}\in \Pi_x$.

* If $\{a,b\}\in \Pi_x$, then $a$ and $b$ are connected in $G-S$.

Thus, a semi-correct profile at $x$ necessarily contains all the pairs
that belong to $\profile(x)$, but it can contain some more pairs.
These additional pairs are not connected in $G[\cone(x)]-S$, but we
are certain that they are connected in the whole graph $G-S$.

The remainder of this section is devoted to arguing the following

Assuming $\Tt$ is weakly $(q,k)$-unbreakable and the algorithm of
<ref> is run to answer a query $\conn(u,v,S)$,
the following holds: whenever the algorithm computes the profile at
any node $x$, this profile is semi-correct.

Note that for the root $r$ of $T$, we have $G[\cone(r)]=G$, so any
semi-correct profile at $r$ is equal to $\profile(r)$. Therefore,
<ref> implies that the outcome of the
algorithm is correct.

To prove <ref> it suffices to argue that the
assumption of semi-correctness can be pushed through the computation
presented in the proofs of <ref> and <ref>.
This we do in the next two lemmas.

Suppose $z$ is an ancestor of $y$ in $T$ such that $\wh{S}$ is
disjoint with $\cmp(z)\setminus \cone(y)$, and $\Pi_y$ is a
semi-correct profile for $y$. Let $J$ be a graph on vertex set
$D(y)\cup \adh(z)$ whose edge set is the union of  $\Pi_y$ and the
edge set of $\torso(z,y)$. Further, let
$\Pi_z\subseteq \binom{D(z)}{2}$ consist of all pairs
$\{a,b\}\in \binom{D(z)}{2}$ that are connected in $J-S$. Then
$\Pi_z$ is a semi-correct profile for $z$.

Suppose first that $\{a,b\}\in \binom{D(z)}{2}$ are connected in
$G[\cone(z)]-S$. Let $P$ be a path witnessing this. Then $P$ can be
uniquely written as concatenation of paths $P_1,P_2,\ldots,P_\ell$,
where each path $P_i$ has endpoints in $V(J)$, but is otherwise
vertex-disjoint with $V(J)$. Note that each path $P_i$ has all
internal vertices either contained in $\cmp(z)\setminus \cone(y)$,
or in $\cmp(y)$. Paths of the first kind correspond to edges with
the same endpoints present in the edge set of $\torso(z,y)$, while
paths of the second kind correspond to edges with the same endpoints
present in $\Pi_y$, due to the semi-correctness of $\Pi_y$. It
follows that $a$ and $b$ are connected by a path in $J$ that avoids
$S$, so $\{a,b\}\in \Pi_z$ by the definition of $\Pi_z$.

Conversely, suppose $\{a,b\}\in \Pi_z$. Then in $J$ there is a path
$P'$ that connects $a$ and $b$ and is disjoint with $S$. For every
edge $e$ of $P'$, let $P_e$ be a path in $G-S$ defined as follows:

* If $e$ originates from the edge set of $\torso(z,y)$, then let
$P_e$ be the path in $G[\cone(z)\setminus \cmp(y)]$ with the same
endpoints as $e$ that witnesses the existence of $e$ in
$\torso(z,y)$. Note that $P_e$ is disjoint with $S$, because all
its internal vertices belong to $\cmp(z)\setminus \cone(y)$.

* If $e\in \Pi_y$, then by semi-correctness of $\Pi_y$, there is
a path $P_e$ in $G-S$ with the same endpoints as $e$.

By concatenating paths $\{P_e\colon e\in E(P')\}$ in order we obtain
a walk connecting $a$ and $b$ in $G-S$.

<ref> proves that the procedure presented in the proof
of <ref> outputs a semi-correct profile for $z$, provided it
is supplied with a semi-correct profile for $y$.

Let $x\in Y$ and let $Z$ be the set of affected children of $x$.
Suppose for each $z\in Z$ we have a semi-correct profile $\Pi_z$.
Let $\bgraph'$ be a graph obtained from $G[\bag(x)]$ by adding the
following edges:

* for each $z\in Z$, add all pairs of  $\Pi_z$ as edges; and

* for each child $w$ of $x$ such that $w\notin Z$, add all pairs
of $\binom{\adh(w)}{2}$ as edges.

Then for each pair of distinct vertices $a,b\in \bag(x)$, the
following implications hold:

* If $a$ and $b$ are connected in $\bgraph'-S$, then $a$ and $b$
are connected in $G-S$.

* If there exist $A,B\subseteq \bag(x)$, each of size $q+1$ and
disjoint from $S$, such that $a\in A$, $b\in B$, $\bgraph'[A]$ is
connected, and $\bgraph'[B]$ is connected, then $a$ and $b$ are
connected in $G-S$.

For the first implication, observe that if $P'$ is a path connecting
$a$ and $b$ in $\bgraph'-S$, then by the semi-correctness of
profiles $\Pi_z$ and regularity of $\Tt$, every edge of $P'$ that is
not present in $G[\bag(x)]-S$ can be replaced by a path in $G-S$
connecting same endpoints. This yields a walk in $G-S$ connecting
$a$ and $b$.

For the second implication, the same argument as above shows that
$A$ is contained in the vertex set of a single connected component
of $G-S$, and the same goes for $B$. Since $A,B\subseteq \bag(x)$,
$\bag(x)$ is $(q,k)$-unbreakable in $G$, and $|S|\leq k$, it follows
that this must be the same connected component for both $A$ and $B$.
So $a$ and $b$ belong to the same connected component of $G-S$.

It is straightforward to verify that in the algorithm presented in
<ref>, the considered graph $\bgraph_S$ is exactly the
graph $\bgraph'-S$ from <ref> (considered there
for $\Pi_z=\profile(z)$ for $z\in Z$). Further, a pair
$\{a,b\}\in \binom{\bag(x)}{2}$ is deemed connected in $G[\cone(x)]-S$
if and only if one of the preconditions of the two implications
mentioned in <ref> holds. Hence, if we run the
algorithm supplied with the semi-correct profiles
$\{\Pi_z\colon z\in Z\}$, then the outcome is
$\Pi_x\subseteq \binom{D(x)}{2}$ satisfying the following.

* If distinct $a,b\in D(x)$ are connected in $G[\cone(x)]-S$, then
$\{a,b\}\in \Pi_x$. This follows from the fact that the sets
$\{\Pi_z\colon z\in Z\}$ are supersets of the profiles
$\{\profile(z)\colon z\in Z\}$, so the edge set of the graph
$\bgraph'-S$ is a superset of the edge set of the graph $\bgraph_S$
considered in the proof of <ref>.
Consequently, every pair $\{a,b\}\in \profile(x)$ is included in

* If $\{a,b\}\in \Pi_x$, then $a$ and $b$ are connected in $G-S$.
This follows from the construction of $\Pi_x$ and
<ref>. (Semi-correctness of
$\{\Pi_z\colon z\in Z\}$ needs also to be used for the corner cases
when $\{a,b\}\nsubseteq \binom{\bag(x)}{2}$.)

In other words, the constructed set $\Pi_x$ is a semi-correct profile
for $x$. We conclude that if the algorithm presented in the proof of
<ref> is supplied with semi-correct profiles
$\{\Pi_z\colon z\in Z\}$, then it produces a semi-correct profile
$\Pi_x$ for $x$.

Now, <ref> follows by a straightforward
bottom-up induction using <ref> and
<ref>. This concludes the proof of

§ AUTOMATA ON AUGMENTED TREES

We consider augmented trees, that are, rooted trees in which the set of children of any given
node carries the structure of a graph, or more generally, a relational
structure (see <ref>).

A tree augmented with graphs. The root is at the top, the edges of the tree
are marked black, while the edges of the graphs are marked red,
and they may only connect nodes that are siblings in the tree.
As a first-order relational structure, the tree is equipped with
the ancestor relation induced by the tree, as well as the red edge relation.

Unranked, unordered trees are a special case of this, by
assuming the children form a set with no relations, while ordered
trees are a special case where the children form a total order. Here,
we allow the children to carry an arbitrary structure, but in our
application, this structure will be an edge- and vertex-colored
graph that excludes some fixed topological minor.  We also consider
automata that process such trees from the leaves towards the root in a deterministic fashion, by labeling each node by a state from a finite state space. To determine whether a node $v$ should be labeled with a state $q$,
a first-order sentence $\delta_q$ is evaluated in the structure induced by the children of $v$.

Augmented trees can be viewed as relational structures equipped with
the ancestor relation $\preceq$ of the tree, as well as the relations $\Sigma$ relating the children of any given node, with which the tree is augmented.
Therefore, the logic $\FO(\preceq, \Sigma)$ is able to mix the two
structures, and express for example that every node whose children satisfy
a certain $\FO(\Sigma)$-definable property has an ancestor that satisfies another $\FO(\Sigma)$-definable property.

We use those automata as a tool for solving various computation problems related to the logic $\FO(\preceq, \Sigma)$.
Namely, the main results of this section are:

* every formula of $\FO(\preceq, \Sigma)$ can be converted into an equivalent automaton on augmented trees

* automata on augmented trees, and hence $\FO(\preceq, \Sigma)$ sentences, can be efficiently evaluated on trees augmented with structures from a class $\CC$, assuming that the model-checking of first-order logic can efficiently be solved on $\CC$

* automata on augmented trees, and hence $\FO(\preceq, \Sigma)$ formulas, can be efficiently queried on trees augmented with structures from a class $\CC$, assuming   first-order queries can be efficiently answered on $\CC$

* satisfying valuations to automata on augmented trees, and hence $\FO(\preceq, \Sigma)$ formulas, can be efficiently enumerated on trees augmented with structures from a class $\CC$, assuming first-order queries can be efficiently enumerated on $\CC$

All the results proved in this section are generic and can be applied to trees augmented with various kinds of structures.
More generally, they are proved for the more
powerful logic $\FOMSO$ that
allows to access the tree structure using not only the relation $\preceq$, but indeed any $\MSO$-definable relation on trees labeled with labels from a finite alphabet $A$.
Our results generalize known results concerning the evaluation and enumeration of $\MSO$ queries on usual trees, e.g. [25].

In the next section, we use the results from this section
in the context of topological minor-free graph classes. Namely, we reduce the problem of evaluating/enumerating $\FOsep$ queries on such classes to the problem of evaluating/enumerating $\FOMSO$ queries on trees augmented with topological minor-free graph classes.
However,  the results obtained in this section may be of independent interest,
and potentially of broader applicability.

In the algorithmic statements proved in this section, we will assume that the class $\CC$ with which the trees are augmented
is a class for which $\FO$ model-checking,
query answering or query enumeration can be solved efficiently.
We remark here that all these assumptions are satisfied whenever $\CC$ is a topological minor-free graph class,
as will happen in our applications.
More generally, they are satisfied
for any class with bounded expansion, by results of [26] or [39].

§.§ Augmented trees and their automata

Fix a signature $\Sigma$ and an alphabet $A$. We assume that
$\Sigma\cap A=\emptyset$ and that $\Sigma$ does not contain the symbol
$\preceq$. Let $\CC$ be a class of $\Sigma$-structures. A
$\Cc$-augmented tree over the alphabet $A$ is a rooted tree $T$
where each node $v$ is labeled with a letter from $A$ and is associated with a
$\Sigma$-structure $\str A_v\in \CC$, called the whorl[
In botany, a whorl is an arrangement of similar parts,
e.g. branches, that radiate from a single point and surround the
stem of a tree or plant.] at $v$, whose elements are the children
of $v$ in $T$.
In some applications, it may be convenient to each node to be labeled with
a set of letters from $A$, rather than a single letter.
This scenario can be modeled using the above definition,
by replacing the alphabet $A$ by $2^A$.

We view an augmented tree $T$ over the alphabet $A$ as relational
structure over the signature $\Sigma\cup\set\preceq\cup A$, as

* the domain consists of the nodes of $T$,

* the unary relation $a$, for $a\in A$, contains a node $v$
if and only if $v$ has label $a$,

* $v\preceq w$ denotes that $v$ is an ancestor of $w$ in $T$
(possibly $v=w$),

* for each $R\in \Sigma$ of arity $t$, $R(v_1,\ldots,v_t)$ holds
if and only if $v_1,\ldots,v_t$ have the same parent $v$, and
$R(v_1,\ldots,v_t)$ holds in the whorl $\str A_v$ at $v$.

We now define automata that input augmented trees, and process them
from the leaves towards the root. As an automaton proceeds, it labels
each node by a state from a finite set $Q$ of states. To determine the
new state at a node $v$, assuming each child of $v$ already has an
assigned state, the automaton evaluates first-order sentences on the
whorl of $v$, which is now a $Q$-labeled $\Sigma$-structure (see <ref>).

A run of an automaton on a tree augmented with graphs. The underlying tree is unlabeled, that is, over an alphabet with one element. The color of a node represents the state assigned in the run.
The transition sentences are described above, and can be expressed using first-order sentences.
The automaton accepts those augmented trees that contain two nodes $u$ and $v$ such that $u$ and $v$ are adjacent in the (red edge) graph relation, the whorl at $u$ contains a triangle, and the whorl at $v$ does not contain a triangle.

Formally, an automaton $\aut A$ on augmented trees consists of:

* an input alphabet $A$: the automaton will process
augmented trees over the alphabet $A$,

* a finite set of states $Q$,

* a set of accepting states $F\subset Q$,

* for each state $q\in Q$ and letter $a\in A$, a first-order
sentence $\delta_{q,a}$ in the signature $\Sigma\cup Q$, where each
$q\in Q$ is viewed as a unary relation symbol, such that for every
fixed $a\in A$, the sentences $(\delta_{q,a})_{q\in Q}$ are mutually
inconsistent and their disjunction $\bigvee_{q\in Q}\delta_{q,a}$ is
equivalent to true. The sentences $\delta_{q,a}$ are called the
transition sentences of $\aut A$.

A run of $\aut A$ on an augmented tree $T$ is a labeling
$\rho\from V(T)\to Q$ such that for every node $v$ with letter $a$ and
whorl $\str A_v$, the state $q=\rho(v)$ is the unique state such that
$\delta_{q,a}$ holds in the  structure $\str A_v$
with labeling $\rho$ restricted to $\str A_v$.  Formally, $\str A_v$
is viewed as a structure over the signature ,
where a predicate $q\in Q$ holds on a vertex $v$ if and only if
$\rho(v)=q$.  The run is accepting if it labels the root with
an accepting state. The automaton $\aut A$ accepts an augmented
tree $T$ if it has an accepting run on it.

Note that there is exactly one run of $\aut A$ on any given augmented
tree $T$, by the assumption that the sentences
$(\delta_{q,a})_{q\in Q}$ are mutually inconsistent and their
disjunction is equivalent to true. It is undecidable if a given
collection of transition sentences satisfies the