2EXP

# Ramsey Quantifiers over Automatic Structures: Complexity and Applications to
Verification

Pascal Bergsträßer  0000-0002-4681-2149 Department of Computer Science, TU
KaiserslauternKaiserslauternGermany ,  Moses Ganardi  0000-0002-0775-7781 Max
Planck Institute for Software Systems (MPI-SWS)KaiserslauternGermany ,
Anthony W. Lin  0000-0003-4715-5096 Department of Computer Science, TU
Kaiserslautern Max Planck Institute for Software Systems (MPI-
SWS)KaiserslauternGermany and  Georg Zetzsche  0000-0002-6421-4388 Max Planck
Institute for Software Systems (MPI-SWS)KaiserslauternGermany

(2022)

###### Abstract.

Automatic structures are infinite structures that are finitely represented by
synchronized finite-state automata. This paper concerns specifically automatic
structures over finite words and trees (ranked/unranked). We investigate the
“directed version” of Ramsey quantifiers, which express the existence of an
infinite directed clique. This subsumes the standard “undirected version” of
Ramsey quantifiers. Interesting connections between Ramsey quantifiers and two
problems in verification are firstly observed: (1) reachability with Büchi and
generalized Büchi conditions in regular model checking can be seen as Ramsey
quantification over transitive automatic graphs (i.e., whose edge relations
are transitive), (2) checking monadic decomposability (a.k.a. recognizability)
of automatic relations can be viewed as Ramsey quantification over co-
transitive automatic graphs (i.e., the complements of whose edge relations are
transitive). We provide a comprehensive complexity landscape of Ramsey
quantifiers in these three cases (general, transitive, co-transitive), all
between and . In turn, this yields a wealth of new results with precise
complexity, e.g., verification of subtree/flat prefix rewriting, as well as
monadic decomposability over tree-automatic relations. We also obtain
substantially simpler proofs, e.g., for complexity for monadic decomposability
over word-automatic relations (given by DFAs).

Ramsey quantifier, automatic structures, recurrent reachability, monadic
decomposability

††copyright: acmcopyright††journalyear: 2022††conference: LICS ’22: ACM/IEEE
Symposium on Logic in Computer Science; August 02–05, 2022; Haifa,
Israel††ccs: Theory of computation Logic and verification††ccs: Theory of
computation Regular languages††ccs: Theory of computation Tree languages

##  1\. Introduction

Automatic structures are infinite structures whose domains are _regular sets_
(represented by finite automata over finite words/trees) and whose relations
are _regular relations_ (represented by synchronized finite word/tree
automata) (Blumensath and Grädel, 2000, 2004). They have been intensively
studied in the logic and automata community, and have been also applied to
infinite-state verification, especially the area of regular model checking. In
this paper, we are interested in algorithmic aspects of the so-called _Ramsey
quantifiers_ , which state the existence of infinite cliques. We pinpoint a
surprising connection between Ramsey quantifiers and the verification of
liveness properties in regular model checking, as well as monadic
decomposability of regular relations (a.k.a. finite recognizability).
Exploiting this connection, we establish a comprehensive picture of the
computational complexity landscape of Ramsey quantifiers over automatic
structures, as well the aforementioned verification problems. We first discuss
the state-of-the-art of these seemingly disconnected problems.

#### Ramsey Quantifiers over Automatic Structures

Blumensath and Grädel were the first to systematically study automatic
structures (Blumensath and Grädel, 2000, 2004). A fundamental fact is that,
given a first-order formula $\varphi(\bm{x})$ and a word/tree automatic
structure $\mathfrak{A}$ (with domain $A$), one can effectively compute a
synchronized word/tree automaton representing the set
$[\\![\varphi]\\!]_{\mathfrak{A}}=\\{\bm{a}\in
A^{|\bm{x}|}:\mathfrak{A}\models\varphi(\bm{a})\\}$ of solutions of $\varphi$.
In other words, regular relations are _effectively closed under all first-
order operations_. Consequently, first-order (FO) model checking over
automatic structures is decidable.

In the seminal paper (Blumensath and Grädel, 2000) on automatic structures, it
was already observed that FO can be enriched with the quantifier “there exist
infinitely many” — i.e., $\exists^{\infty}x\varphi(x,\bm{y})$, which is true
iff there exist infinitely many $x$ such that $\varphi(x,\bm{y})$ — while
preserving the above effective closure property and decidability of model
checking. In fact, assuming nondeterministic automata as finite
representations of $[\\![\varphi]\\!]_{\mathfrak{A}}$, one can compute
$[\\![\exists^{\infty}x\varphi]\\!]_{\mathfrak{A}}$ in polynomial-time. A few
years later, in the case of word automatic structures, Rubin (Rubin, 2008)
studied Ramsey quantifiers, which generalize $\exists^{\infty}$ by enforcing
that these infinitely many elements form an infinite undirected clique, and
showed that Ramsey quantifiers preserve regularity as well, meaning FO
extended with Ramsey quantifiers is still decidable. Upon closer inspection,
Rubin’s construction runs in doubly exponential time. _Is this optimal?_ _Does
the same extend to tree-automatic structures?_

#### Liveness in Regular Model Checking

_Regular model checking (RMC)_ is a generic verification framework that
exploits regular languages and relations (e.g., over finite/$\omega$-words or
trees) as symbolic representations of infinite systems (Abdulla et al., 2002,
2004; Lin and Rümmer, 2021). Various flavors of automata and transducers for
representing the transition relations are employed, e.g., word/tree automatic
relations (or subsets thereof), $\omega$-automatic relations (or subsets
thereof), and rational relations. Since safety and reachability are
undecidable in RMC (e.g., over automatic graphs), one focus of RMC has been to
develop acceleration/widening techniques, which are semi-algorithms for
computing reachability sets (i.e., $post^{*}(S)$) and reachability relations
(i.e., transitive closure $R^{*}$ of the edge relation in the graph), that may
terminate on many interesting cases. Some of these semi-algorithms have
general completeness and termination guarantee, e.g., bounded local-depth
acceleration for automatic relations are guaranteed to compute reachability
relations for pushdown systems (PDS) and ground-tree rewrite systems (GTRS)
(Abdulla et al., 2002; Lin, 2012), while flattable acceleration for
Presburger-definable relations is guaranteed to compute reachability relations
for reversal-bounded counter systems and 2-dimensional vector addition systems
with states (Leroux and Sutre, 2006).

Reachability sets/relations can be directly used to solve safety. The
challenge of verifying liveness is the necessity to deal with genuinely
infinite paths (with no repeated configurations). To and Libkin (To and
Libkin, 2008, 2010) showed that one can decide liveness (in the form of
recurrent reachability) over word- and tree-automatic graphs, when the
transitive closure $R^{*}$ of the edge relation is additionally supplied
(e.g., by the aforementioned acceleration methods or otherwise). The algorithm
runs in time polynomial in the size of the problem, with $R^{*}$ supplied as
part of inputs. Their technique uses a kind of “staircase argument” combined
with Ramsey’s Theorem to construct a Büchi automaton that represents some
witnessing infinite runs.

#### Monadic Decomposability and Recognizability

A classic task in the theory of finite-state transductions is the problem to
decide whether a given regular relation $R\subseteq(\Sigma^{*})^{k}$ is
_recognizable_ , i.e., if it can be expressed as a finite union of cartesian
products of regular languages (in symbols:
$R=\bigcup_{i=1}^{n}L_{i,1}\times\cdots\times L_{i,k}$ for some
$n\in\mathbb{N}$ and regular sets $L_{i,j}\subseteq\Sigma^{*}$). In the formal
verification terminology (Veanes et al., 2017), such a relation is said to be
_monadically decomposable_ , i.e., that it can be expressed as a Boolean
combination of monadic predicates. The first important result was by Stearns
(Stearns, 1967) and Valiant (Valiant, 1975): Their algorithms for checking
regularity of deterministic pushdown automata imply that given deterministic
rational relation—i.e., a relation $R\subseteq\Sigma^{*}\times\Sigma^{*}$
recognized by _deterministic asynchronous automata_ , which is strictly more
general than binary automatic relations—can be checked to be recognizable in
doubly exponential time. This decidability was extended to general $k$-ary
deterministic rational relations by Carton et al. (Carton et al., 2006), which
yields decidability as well for the subclass of automatic relations. As noted
by Löding and Spinrath (Löding and Spinrath, 2019), the complexity of the
algorithm for automatic relations in (Carton et al., 2006) runs in doubly
exponential time. Using their new polynomial-time algorithm for checking
regularity for deterministic visibly pushdown automata, Löding and Spinrath
showed that this could be improved to single exponential time for binary
automatic relations. The complexity for automatic relations was fully settled
by Barceló et al. (Barceló et al., 2019) by showing that this problem is
-complete (resp. -complete) when $R$ is presented as a deterministic (resp.
nondeterministic) automaton. The proof technique in (Barceló et al., 2019) is
an extremely intricate refinement and analysis of the staircase argument used
by To and Libkin (To and Libkin, 2008) for recurrent reachability for
automatic relations.

#### Contributions

Our account of the state-of-the-art of the aforementioned three research
directions seems to suggest that there might be some connections between them.
To what extent are they connected? Is there a more fundamental notion that
unifies them? These questions are hitherto open, but as we shall see in this
paper the answer is a resounding yes. We pinpoint that the _directed Ramsey
quantifiers_ —which ask for the existence of infinite directed cliques
(instead of infinite undirected cliques as in (Rubin, 2008))—is a fundamental
concept that underlies the above three problems, and lets us study them under
the same umbrella, while inferring the optimal complexity and even new
results. On the one hand, the directed Ramsey quantifiers subsume the standard
Ramsey quantifiers.

On the other hand, recurrent reachability over automatic graphs (To and
Libkin, 2008) can be seen as a Ramsey quantifier over a transitive binary
relation, whereas monadic decomposability over automatic relations (Carton et
al., 2006; Barceló et al., 2019; Löding and Spinrath, 2019) can be construed
as a Ramsey quantifier over co-transitive binary relations. Our results are
summarized in Table 1.

Firstly, from the proof by Barceló et al. (Barceló et al., 2019), it is
possible to infer that the Ramsey quantifier can be evaluated on regular
relations in $\NL$, which substantially improves the doubly exponential-time
algorithm of Rubin (Rubin, 2008). Unfortunately, their argument relies on an
intricate Ramsey argument on the transition monoid of the automaton. Our
contribution is a substantially simpler argument that avoids the use of the
transition monoid altogether, which we show to generalize to the case of tree-
regular relations (which is not the case with the proof of (Barceló et al.,
2019)). More precisely, our approach divides the proof for regular relations
into two steps: (i) First, we argue that one can assume infinite cliques
witnessed by accepting runs that form a comb of combs. (ii) Then, we argue
that the runs can be “merged” together so that it can be witnessed by a single
run of a polynomial-size Büchi automaton. This way, we obtain the same
complexity as (Barceló et al., 2019).

For tree-regular relations we can easily extend step (i). The comb of combs
structure of the accepting runs can be witnessed by an alternating Büchi tree
automaton, which yields the complexity of $\EXP$ for the Ramsey quantifier on
tree-regular relations. However, step (ii) is provably impossible over tree-
regular relations, since as we show, the infinite clique problem is
$\EXP$-hard. For the special cases of transitive and co-transitive relations
we need further separate arguments that enable us to evaluate the Ramsey
quantifier in $\P$. The case for transitive relations can be inferred from the
proof in (To and Libkin, 2008), but not so for the co-transitive case.

Finally, we apply our results to decidability and complexity of recurrent
reachability with generalized Büchi conditions, and automatic structures over
unranked trees. We show, for example, decidability (in fact in polynomial-
time) of recurrent reachability of subtree/flat prefix rewriting, answering an
open question by Löding and Spelten (Löding and Spelten, 2007) and
decidability (in fact, $\EXP$-completeness) of recurrent reachability with
generalized Büchi conditions of ground tree rewrite systems, answering an open
question by Löding (Löding, 2006).

#### Organization

We provide a more detailed summary of our main results in Section 2. We fix
notation and basic terminologies in Section 3. We then start with the word
case in Section 4 and proceed to the tree case in Section 5. Applications and
generalizations to unranked trees are given in, respectively, Section 6 and
Section 7.

|  regular relations |  tree-regular relations
---|---|---
Automaton construction for Ramsey quantifier |  logspace |  exponential time poly-time for (co)transitive relations
Recurrent reachability & infinite clique |  -complete∗ |  -complete for NTA, D$\downarrow$TA ¶-complete for transitive relations∗ or D$\uparrow$TA
Recurrent reachability with generalized Büchi condition |  -complete |  -complete
Monadic decomposability |  -complete for DFA∗ -complete for NFA∗ |  ¶-complete for D$\uparrow$TA, D$\downarrow$TA -complete for NTA
Table 1. Complexity results. Those marked with ∗ were known, but we provide
simpler proofs. The other results are new.

##  2\. Detailed summary of main results

To improve readability, we provide a detailed summary of our main results in
this section before we take a deeper dive into the proofs. Unless otherwise
specified, the completeness results mentioned in this section (and Table 1)
hold for NFAs and DFAs in the word case and NTAs, D$\uparrow$TAs, and
D$\downarrow$TAs in the tree case. We define the directed Ramsey quantifier:

###### Definition 2.1.

Let $\mathfrak{A}$ be a structure with domain $A$. The _Ramsey quantifier_
$\exists^{\mathrm{ram}}$ over an $\mathfrak{A}$-formula $\varphi$ with $k+2$
free variables is defined for all $\bm{c}\in A^{k}$ by
$\mathfrak{A}\models\exists^{\mathrm{ram}}x,y\colon\varphi(x,y,\bm{c})$ if and
only if there is an infinite sequence $(a_{i})_{i\geq 1}$ of pairwise distinct
elements $a_{i}\in A$ so that $\mathfrak{A}\models\varphi(a_{i},a_{j},\bm{c})$
for all $1\leq i<j$.

We deviate from the definition of the Ramsey quantifier found in the
literature, see (Grädel, 2020), requiring
$\mathfrak{A}\models\varphi(a_{i},a_{j},\bm{c})$ for all $i\neq j$, in the
definition above. Over (tree-)regular relations the two quantifier definitions
can be simulated by each other, see Appendix A. Furthermore, there are also
higher-dimensional versions $\exists^{d\text{-}\mathrm{ram}}$ of the Ramsey
quantifier, which will not be considered in this paper.

#### Evaluating Ramsey quantifiers

If $R$ is a binary (tree-) regular relation, then evaluating
$\exists^{\mathrm{ram}}x,y\colon R(x,y)$ is the problem of checking whether
$R$ contains an _infinite (directed) clique_ , i.e., an infinite sequence
$(a_{i})_{i\geq 1}$ of distinct elements of $A$ such that $(a_{i},a_{j})\in R$
for all $1\leq i<j$. It follows from (Barceló et al., 2019) that the infinite
clique problem over word-regular relations is $\NL$-complete. We provide a
much simpler proof by considering a slightly more general setting. Instead of
the infinite clique problem we consider the evaluation of the Ramsey
quantifier on a $(k+2)$-ary (tree-)regular relation $R\subseteq A^{k+2}$,
i.e., compute an automaton for $[\\![\exists^{\mathrm{ram}}x,y\colon
R(x,y,\bm{z})]\\!]=\\{\bm{c}\in A^{k}\mid\exists^{\mathrm{ram}}x,y\colon
R(x,y,\bm{c})\\}$.

###### Theorem 2.2.

Given a regular relation $R\subseteq(\Sigma^{*})^{k+2}$ by an NFA
$\mathcal{A}$111In this and the following theorems, the parameter $k$ is part
of the input., one can construct in logspace an NFA for the relation
$[\\![\exists^{\mathrm{ram}}x,y\colon R(x,y,\bm{z})]\\!]$. In particular, the
infinite clique problem over regular relations is in $\NL$.

We show that the complexity of the infinite clique problem increases from
$\NL$ to $\EXP$ when considered over tree-regular relations given by NTAs or
D$\downarrow$TAs. Let $\mathcal{T}_{\Sigma}$ denote the set of ranked trees
over alphabet $\Sigma$.

###### Theorem 2.3.

The infinite clique problem over tree-regular relations
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ is $\EXP$-complete
if $R$ is given as NTA or D$\downarrow$TA, and $\P$-complete if $R$ is given
as D$\uparrow$TA.

For the exponential lower bound, we present a reduction from intersection
nonemptiness for NTAs and D$\downarrow$TAs. This is surprising, because an
analogue reduction in the word case does not exist: This would yield a
$\PSPACE$ lower bound for the infinite clique problem over words, but the
latter belongs to $\NL$.

For the exponential upper bound of Theorem 2.3, we prove the tree analogue of
Theorem 2.2. It even holds when the relation $R$ is given as an alternating
tree automaton (ATA), which allows us to apply it to recurrent reachability
with generalized Büchi condition.

###### Theorem 2.4.

Given an ATA (D$\uparrow$TA) $\mathcal{A}$ for a tree-regular relation
$R\subseteq(\mathcal{T}_{\Sigma})^{k+2}$, one can construct in exponential
(polynomial) time an NTA for the relation
$[\\![\exists^{\mathrm{ram}}x,y\colon R(x,y,\bm{z})]\\!]$.

If we make further assumptions on the relation $R$, we obtain a better
complexity for NTAs. We say that a $(k+2)$-ary relation $R$ over $A$ is
_transitive_ if the binary relation $\\{(a,b)\mid(a,b,\bm{c})\in R\\}$ is
transitive for all $\bm{c}\in A^{k}$.

###### Theorem 2.5.

Given an NTA $\mathcal{A}$ for a transitive tree-regular
$R\subseteq(\mathcal{T}_{\Sigma})^{k+2}$, one can construct in polynomial time
an NTA for the relation $[\\![\exists^{\mathrm{ram}}x,y\colon
R(x,y,\bm{z})]\\!]$. In particular, the infinite clique problem over
transitive tree-regular relations is in $\P$.

A binary relation $R\subseteq A\times A$ is co-transitive if its complement
$(A\times A)\setminus R$ is a transitive relation.

###### Theorem 2.6.

The infinite clique problem over co-transitive tree-regular relations
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ given as NTA is in
$\P$.

In Section 7 we show by a reduction that the Ramsey quantifier can be
evaluated over unranked tree-regular relations with the same complexity as in
the ranked case.

#### Recurrent reachability

Since reachability in automatic graphs is in general undecidable (Blumensath
and Grädel, 2004), we will instead use transitive paths, i.e., infinite
sequences $(a_{i})_{i\geq 1}$ with $(a_{i},a_{j})\in R$ for all $1\leq i<j$.
Given sets $L_{1},\dots,L_{k}\subseteq A$ we write
$\mathit{Rec}(L_{1},\dots,L_{k})[R]$ for the set of all initial vertices
$a_{1}$ of transitive paths $(a_{i})_{i\geq 1}$ that visit each set $L_{j}$
infinitely often. Recurrent reachability with generalized Büchi condition is
the problem of testing $a_{1}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ for a
given (tree-)regular relation $R\subseteq A\times A$, (tree-)regular languages
$L_{1},\dots,L_{k}\subseteq A$, and an initial element $a_{1}\in A$. If $k=1$
this problem is simply called recurrent reachability.

Since the infinite clique problem and recurrent reachability are logspace
equivalent (Proposition 6.1), we obtain:

###### Corollary 2.7.

Recurrent reachability is $\NL$-complete over regular relations. It is
$\EXP$-complete over tree-regular relations given by NTAs or D$\downarrow$TAs,
and $\P$-complete if the tree-regular relations are transitive or given by
D$\uparrow$TAs.

We also apply Theorems 2.2 and 2.4 to obtain tight upper bounds for recurrent
reachability with generalized Büchi condition. The lower bounds result from a
reduction from intersection nonemptiness.

###### Theorem 2.8.

Recurrent reachability with generalized Büchi condition is $\PSPACE$-complete
over regular relations, and $\EXP$-complete over tree-regular relations.

#### Monadic Decomposability

Recall that a relation $R\subseteq A^{k}$ is _monadically decomposable_ if it
is of the form $\bigcup_{i=1}^{n}A_{i,1}\times\dots\times A_{i,k}$ for some
$n\in\mathbb{N}$ and (tree-)regular languages $A_{i,j}$. The traditional
approach to deciding monadic decomposability (Ginsburg and Spanier, 1966;
Libkin, 2003; Carton et al., 2006; Löding and Spinrath, 2019; Barceló et al.,
2019) is to associate with $R$ certain equivalence relations $\sim_{j}$ for
$1\leq j\leq k$ such that $R$ is monadically decomposable if and only if each
$\sim_{j}$ has finite index. An equivalence relation has infinite index if and
only if there exist infinitely many elements that are pairwise in different
equivalence classes which is witnessed by an infinite clique in the complement
relation. Therefore, monadic decomposability amounts to checking that
$\sim_{j}$’s complement $\not\sim_{j}$ does not have an infinite clique for
any $j$. If $R$ is given by a DFA (resp. NFA), then one can construct an NFA
for each $\not\sim_{j}$ in logspace (resp. in $\PSPACE$) and thus Theorem 2.2
yields a tight upper bound:

###### Corollary 2.9.

Given a regular relation $R\subseteq(\Sigma^{*})^{k}$ by a DFA (resp. NFA), it
is $\NL$-complete (resp. $\PSPACE$-complete) to decide whether $R$ is
monadically decomposable.

While this approach yields optimal complexity for words, this is,
unexpectedly, not the case for trees. For a tree-regular relation given as
D$\downarrow$TA or D$\uparrow$TA (resp. NTA), one can also construct an NTA
for each $\not\sim_{j}$ in logspace (resp. $\PSPACE$). Then, applying Theorem
2.4 would yield an $\EXP$ (resp. $\TwoEXP$) algorithm. However, perhaps
surprisingly, monadic decomposability for trees has much lower complexity:

###### Corollary 2.10.

Given a tree-regular relation $R\subseteq\mathcal{T}_{\Sigma}^{k}$ by a
D$\downarrow$TA or D$\uparrow$TA (resp. NTA), it is $\P$-complete (resp.
$\EXP$-complete) to decide whether $R$ is monadically decomposable.

To get the $\P$ (resp. $\EXP$) algorithm, we exploit co-transitivity of each
$\not\sim_{j}$ and apply Theorem 2.6 instead of Theorem 2.4. This shows the
importance of the co-transitivity notion: In the word case, monadic
decomposability requires only the generic clique detection, but the tree case
is more nuanced—we need one algorithm for the general case and a specialized
algorithm for co-transitive relations.

##  3\. Preliminaries

We assume familiarity with the basic models of (non)deterministic and
alternating finite automata on words and trees as well as with standard
complexity classes (e.g., , ¶, , ). We refer the reader to the textbooks
(Kozen, 1997; Comon et al., 1997) for more details. We often abbreviate a
finite or infinite sequence of elements $a_{1},a_{2},\dots$ by a boldface
letter $\bm{a}$.

#### Trees

A tree domain is a nonempty set $D\subseteq\mathbb{N}^{*}$ such that (i) $D$
is prefix closed, i.e., $uv\in D$ implies $u\in D$, (ii) for all
$v\in\mathbb{N}^{*}$ and $j\leq i$ if $vi\in D$, then $vj\in D$, and (iii)
each node $v\in D$ has only finitely many children $vi\in D$ where
$i\in\mathbb{N}$. An unranked tree over an alphabet $\Sigma$ is a function
$t\colon\mathrm{dom}(t)\to\Sigma$ where $\mathrm{dom}(t)$ is a finite tree
domain. A ranked alphabet is a finite alphabet $\Sigma$ where every symbol
$a\in\Sigma$ has a rank $\mathrm{rk}(a)\in\mathbb{N}$. A ranked tree is an
unranked tree $t$ such that every node $v\in\mathrm{dom}(t)$ has
$\mathrm{rk}(t(v))$ many children. We denote the set of all (un)ranked trees
over $\Sigma$ by $\mathcal{T}_{\Sigma}$ and $\mathcal{U}_{\Sigma}$.

Let $x\notin\Sigma$ be a variable. The set $\mathcal{C}_{\Sigma}$ of all
contexts over $\Sigma$ contains all unranked trees over $\Sigma\cup\\{x\\}$
such that every node $u\in\mathrm{dom}(t)$ with $t(u)=x$ is a leaf, called
_hole_. We partition $\mathrm{dom}(t)=\mathrm{nodes}(t)\cup\mathrm{holes}(t)$
into nodes and holes. The size of a context $t$ is $|\mathrm{nodes}(t)|$. For
contexts $s,t_{1},\dots,t_{n}$ with $|\mathrm{holes}(s)|=n$ we denote by
$s[t_{1},\dots,t_{n}]$ the context obtained by replacing the $i$-th hole in
lexicographic order by $t_{i}$. For two contexts
$s_{1},s_{2}\in\mathcal{C}_{\Sigma}$, we call $s_{1}$ a prefix of $s_{2}$,
denoted by $s_{1}\leq_{\mathsf{p}}s_{2}$, if $s_{1}[t_{1},\dots,t_{n}]=s_{2}$
for some contexts $t_{1},\dots,t_{n}$. If $n>0$ and each context $t_{i}$ has
size at least one, then $s_{1}$ is a proper prefix of $s_{2}$, denoted by
$s_{1}<_{\mathsf{p}}s_{2}$.

We define an _infinite unranked tree_ and an _infinite ranked tree_ as in the
finite case but with infinite domains. We denote the set of all finite and
infinite unranked trees over the alphabet $\Sigma$ by
$\mathcal{U}_{\Sigma}^{\infty}$ and the set of all finite and infinite ranked
trees over $\Sigma$ by $\mathcal{T}_{\Sigma}^{\infty}$.

#### Regular and tree-regular languages

A _nondeterministic finite automaton_ (NFA) over the alphabet $\Sigma$ is a
tuple $\mathcal{A}=(Q,\Sigma,\Delta,q_{0},F)$ where $Q$ is a finite set of
states, $\Delta\subseteq Q\times(\Sigma\cup\\{\varepsilon\\})\times Q$ is a
transition relation, $q_{0}\in Q$ is an initial state, and $F\subseteq Q$ is a
set of final states. We denote by $L(\mathcal{A})\subseteq\Sigma^{*}$ the
regular language recognized by $\mathcal{A}$. In our algorithms, the alphabet
$\Sigma$ is _not_ part of the representation of an automaton. Instead, we will
always work with the subalphabet of all symbols occurring in the transitions.
This will be important later when the implicitly given alphabet is
significantly smaller.

A _nondeterministic (top-down) tree automaton_ (NTA) over the ranked alphabet
$\Sigma$ is a tuple $\mathcal{A}=(Q,\Sigma,\Delta,q_{0})$ where $Q$ is a
finite set of states, $q_{0}\in Q$ is an initial state, and
$\Delta\subseteq\bigcup_{a\in\Sigma}Q\times\\{a\\}\times Q^{\mathrm{rk}(a)}$
is a transition relation. A _run_ of $\mathcal{A}$ on a tree
$t\in\mathcal{T}_{\Sigma}$ is a tree $\rho\in\mathcal{T}_{Q}$ with
$\mathrm{dom}(\rho)=\mathrm{dom}(t)$ such that $\rho(\varepsilon)=q_{0}$ and
$(\rho(u),t(u),\rho(u1),\dots,\rho(ur))\in\Delta$ for all nodes
$u\in\mathrm{dom}(\rho)$ with $\mathrm{rk}(t(u))=r$. As before,
$L(\mathcal{A})$ is the set of trees recognized by $\mathcal{A}$, i.e., the
set of all trees $t$ such that there exists a run of $\mathcal{A}$ on $t$. A
set of trees is called _tree-regular_ if there is an NTA that recognizes it.
We will also use the notions of _deterministic finite automata_ (DFA),
_deterministic bottom-up_ (D$\uparrow$TA), and _deterministic top-down tree
automata_ (D$\downarrow$TA). Moreover, _alternating automata_ will be formally
introduced in later sections.

#### Regular and tree-regular relations

Let $\Sigma$ be a finite alphabet and let $\Sigma_{\bot}=\Sigma\cup\\{\bot\\}$
where $\bot\notin\Sigma$ is a fresh symbol. For words
$w_{1},\dots,w_{k}\in\Sigma^{*}$ with $w_{i}=a_{i,1}\dots a_{i,n_{i}}$ and
$n:=\max\\{n_{i}\mid 1\leq i\leq k\\}$ we define their convolution

$w_{1}\otimes\dots\otimes w_{k}:=\begin{bmatrix}w_{1}\\\ \vdots\\\
w_{k}\end{bmatrix}:=\begin{pmatrix}a_{1,1}^{\prime}\\\ \vdots\\\
a_{k,1}^{\prime}\end{pmatrix}\dots\begin{pmatrix}a_{1,n}^{\prime}\\\ \vdots\\\
a_{k,n}^{\prime}\end{pmatrix}\in(\Sigma_{\bot}^{k})^{*}$

where $a_{i,j}^{\prime}=a_{i,j}$ if $j\leq n_{i}$ and $a_{i,j}^{\prime}=\bot$
otherwise. A relation $R\subseteq(\Sigma^{*})^{k}$ is recognized by an NFA
$\mathcal{A}$ if $L(A)=\\{w_{1}\otimes\dots\otimes
w_{k}\mid(w_{1},\dots,w_{k})\in R\\}$. In that case we call $R$ regular.

We extend the definitions to tree-regular relations. For an alphabet $\Sigma$
we set again $\Sigma_{\bot}=\Sigma\cup\\{\bot\\}$ where $\bot\notin\Sigma$ is
a fresh symbol. Let $\varepsilon$ be the _empty tree_ with
$\mathrm{dom}(\varepsilon):=\emptyset$. Given $k$ trees
$t_{1},\dots,t_{k}\in\mathcal{U}_{\Sigma}\cup\\{\varepsilon\\}$ we define
their convolution $t=t_{1}\otimes\dots\otimes
t_{k}\in\mathcal{U}_{\Sigma^{k}_{\bot}}\cup\\{\varepsilon\\}$ with
$\mathrm{dom}(t)=\bigcup_{i=1}^{k}\mathrm{dom}(t_{i})$ and
$t(v)=(t^{\prime}_{1}(v),\dots,t^{\prime}_{k}(v))$ where
$t^{\prime}_{i}(v)=t_{i}(v)$ if $v\in\mathrm{dom}(t_{i})$ and
$t^{\prime}_{i}(v)=\bot$ otherwise. Observe that the degree of a node $v$ in
$t_{1}\otimes\dots\otimes t_{k}$ is the maximum degree of $v$ in a tree
$t_{i}$ such that $v\in\mathrm{dom}(t_{i})$. Similar to the word case, we also
write the convolution of trees as a column vector. If all $t_{i}$ are ranked
trees, then also $t$ is a ranked tree with
$\mathrm{rk}(a_{1},\dots,a_{k}):=\max\\{\mathrm{rk}(a_{i})\mid 1\leq i\leq
k\\}$ for all $(a_{1},\dots,a_{k})\in\Sigma_{\bot}^{k}$ where
$\mathrm{rk}(\bot):=0$. A relation $R\subseteq\mathcal{T}_{\Sigma}^{k}$ is
recognized by an NTA $\mathcal{A}$ if the tree language
$\\{t_{1}\otimes\dots\otimes t_{k}\mid(t_{1},\dots,t_{k})\in R\\}$ is
recognized by $\mathcal{A}$. In that case we call $R$ tree-regular.

Regular and tree-regular relations are effectively closed under first-order
operations (Boolean operations and projections). A relational structure
$\mathfrak{A}$ is automatic (tree-automatic) if its universe and all its
relations are regular (tree-regular).

##  4\. Word-automatic structures

abaaababababbab

$\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}b}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}a}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}}\end{bmatrix}\begin{bmatrix}{\bot}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\\#\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}b}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}b}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\\#\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}a}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}}\end{bmatrix}\begin{bmatrix}\texttt{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}b}}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\begin{bmatrix}{\bot}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}}\end{bmatrix}\begin{bmatrix}{\bot}\\\
\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}}\end{bmatrix}\\#\dots$

Figure 1. An example word comb
$\texttt{ba},\texttt{ababb},\texttt{abaaaab},\dots$ and its encoding as an
infinite word.

We first consider Ramsey quantifiers over word-regular relations. We show that
if $R\subseteq(\Sigma^{*})^{k+2}$ is a regular relation, then an automaton for
$\\{\bm{c}\mid\exists^{\mathrm{ram}}x,y\colon R(x,y,\bm{c})\\}$ can be
constructed in logarithmic space (Theorem 2.2).

#### Word combs

The first step is to observe that, when looking for infinite cliques in $R$,
one can restrict to combs: An infinite sequence $\bm{v}$ of words is called a
comb if there exist infinite sequences $\bm{\alpha}$ and $\bm{\beta}$ of words
with $v_{i}=\beta_{1}\dots\beta_{i-1}\alpha_{i}$ and
$1\leq|\alpha_{i}|\leq|\beta_{i}|$ for all $i\geq 1$. The pair
$(\bm{\alpha},\bm{\beta})$ is called a _generator_ of $\bm{v}$. We remark that
the choice of the generator is not unique. Any infinite subsequence of a comb
is again a comb. In fact, the following lemma is well-known, see (Kuske and
Lohrey, 2010, Lemma 5.1).

###### Lemma 4.1.

Any sequence $\bm{w}$ of pairwise distinct words $w_{i}$ over a finite
alphabet $\Sigma$ contains a comb as a subsequence.

In contrast to arbitrary infinite sequences of words, combs can be encoded
naturally by infinite words. If $(\bm{\alpha},\bm{\beta})$ is a generator we
call the infinite word

$\mathrm{enc}(\bm{\alpha},\bm{\beta})=\begin{bmatrix}\alpha_{1}\\\
\beta_{1}\end{bmatrix}\\#\begin{bmatrix}\alpha_{2}\\\
\beta_{2}\end{bmatrix}\\#\cdots\in((\Sigma_{\bot}\times\Sigma)\cup\\{\\#\\})^{\omega}$

an encoding of $(\bm{\alpha},\bm{\beta})$, or also an encoding of $\bm{v}$.

#### Comb of combs

The next goal would be to construct a Büchi automaton which reads an encoding
of a comb $\bm{v}$ and verifies that $v_{i}\otimes v_{j}$ has an accepting run
$\rho(v_{i},v_{j})$ for all $1\leq i<j$. In general, this is challenging since
it is not clear how a finite automaton can keep track of infinitely many runs
(let alone, an automaton of polynomial size). Instead we will show that every
infinite clique contains an infinite subclique whose accepting runs can be
arranged in a dag of constant width, and can therefore be recognized by a
polynomial-sized Büchi automaton.

Consider a comb $\bm{v}$ with generator $(\bm{\alpha},\bm{\beta})$. First
observe that the convolutions $v_{i}\otimes v_{j}$ can be written as

(1) $\begin{bmatrix}v_{i}\\\ v_{j}\end{bmatrix}=\begin{bmatrix}\beta_{1}\\\
\beta_{1}\end{bmatrix}\dots\begin{bmatrix}\beta_{i-1}\\\
\beta_{i-1}\end{bmatrix}\begin{bmatrix}\alpha_{i}\\\
\beta_{i}\end{bmatrix}\begin{bmatrix}\varepsilon\\\
\beta_{i+1}\end{bmatrix}\dots\begin{bmatrix}\varepsilon\\\
\beta_{j-1}\end{bmatrix}\begin{bmatrix}\varepsilon\\\ \alpha_{j}\end{bmatrix}$

and can hence be arranged in a trie displayed in Figure 2, that we call comb
of combs. The next insight is that we can ensure that the accepting runs
$\rho(v_{i},v_{j})$ on the convolutions $v_{i}\otimes v_{j}$ match this comb
of combs structure, after replacing $\bm{v}$ by an infinite subsequence.
Roughly speaking, the runs look like as if the automaton for $R$ would be
deterministic. For example, all runs $\rho(v_{1},v_{j})$ for $j>1$ share a
common prefix which is a run on $\alpha_{1}\otimes\beta_{1}$, and all runs
$\rho(v_{i},v_{j})$ for $1<i<j$ share a common prefix which is a run on
$\beta_{1}\otimes\beta_{1}$.

A _run_ of an NFA $\mathcal{A}=(Q,\Sigma,\Delta,q_{\mathrm{in}},F)$ on a
nonempty word $a_{1}\dots a_{n}\in\Sigma^{*}$ (runs on the empty word are not
needed here) is a sequence
$(q_{0},a_{1},q_{1})(q_{1},a_{2},q_{2})\dots(q_{n-1},a_{n},q_{n})$ of triples
in $Q\times\Sigma\times Q$ such that there exists a path from $q_{i-1}$ to
$q_{i}$ in $\mathcal{A}$ labeled with $a_{i}$ for all $1\leq i\leq n$. A run
is _accepting_ if $q_{0}=q_{\mathrm{in}}$ and $q_{n}\in F$.

We define a _decomposition_ of a word $w\in\Sigma^{*}$ as $w=u_{1}\dots u_{n}$
where $u_{i}\in\Sigma^{*}$. The decomposition in Equation 1 is called the
$(\bm{\alpha},\bm{\beta})$-decomposition of $v_{i}\otimes v_{j}$. We say that
a decomposition of a run $\rho=\rho_{1}\dots\rho_{n}$ of an NFA is
_compatible_ with a decomposition $w=u_{1}\dots u_{n}$ of a word if $\rho_{i}$
is a run on $u_{i}$ for all $i\in[1,n]$.

We say that a generator $(\bm{\alpha},\bm{\beta})$ of a comb $\bm{v}$ is
_coarser_ than a generator $(\bm{\gamma},\bm{\delta})$ of a comb $\bm{w}$ if
there exist indices $k_{1}<k_{2}<\dots$ such that $v_{i}=w_{k_{i}}$ and
$\beta_{1}\dots\beta_{i}=\delta_{1}\dots\delta_{k_{i}}$ for all $i\geq 1$. In
this case we also say that $(\bm{\alpha},\bm{\beta})$ is the coarsening of
$(\bm{\gamma},\bm{\delta})$ defined by the subsequence $\bm{v}$ of $\bm{w}$.

###### Lemma 4.2.

Let $\bm{w}$ be a comb generated by $(\bm{\gamma},\bm{\delta})$ that forms an
infinite clique in a regular relation $R\subseteq\Sigma^{*}\times\Sigma^{*}$
given as an NFA $\mathcal{A}$. There exist a coarsening
$(\bm{\alpha},\bm{\beta})$ of $(\bm{\gamma},\bm{\delta})$ that generates a
comb $\bm{v}$, accepting runs $\rho(v_{i},v_{j})$ of $\mathcal{A}$ on
$v_{i}\otimes v_{j}$, and runs $\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$
such that

$\rho(v_{i},v_{j})=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,j-1}\nu_{i,j}$

is a decomposition compatible with the
$(\bm{\alpha},\bm{\beta})$-decomposition of $v_{i}\otimes v_{j}$ for all
$i<j$.

###### Proof.

Let $\bm{w}$ be a comb generated by $(\bm{\alpha},\bm{\beta})$ that forms an
infinite clique in $R$ and $\rho(w_{i},w_{j})$ be an accepting run of
$\mathcal{A}$ on $w_{i}\otimes w_{j}$ for all $1\leq i<j$. We establish the
run structure as illustrated in Figure 3 column-wise.

Assume that we already defined $(\kappa_{i})_{i<n}$, $(\lambda_{i})_{i<n}$,
$(\mu_{i,j})_{i<j<n}$, and $(\nu_{i,j})_{i<j<n}$ for some $n\geq 1$ such that

$\displaystyle\rho(w_{i},w_{j})$
$\displaystyle=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,n-1}\tau(w_{i},w_{j})$
$\displaystyle\rho(w_{i^{\prime}},w_{j^{\prime}})$
$\displaystyle=\kappa_{1}\dots\kappa_{n-1}\sigma(w_{i^{\prime}},w_{j^{\prime}})$

for runs $\tau(w_{i},w_{j})$, $\sigma(w_{i^{\prime}},w_{j^{\prime}})$ for all
$1\leq i\leq n-1<j$ and $n-1<i^{\prime}<j^{\prime}$. For all $1\leq i<n$
define $\nu_{i,n}:=\tau(w_{i},w_{n})$.

We now define $\mu_{i,n}$ successively for each $1\leq i<n$. In step $i$ we
apply the pigeonhole principle to get an infinite subsequence $\bm{v}$ of
$\bm{w}$ starting with $w_{1},\dots,w_{n}$ such that all runs
$\tau(v_{i},v_{j})$ for $j>n$ have a common prefix $\mu_{i,n}$ which is a run
on $\varepsilon\otimes\beta_{n}$. At the end of step $i$ we replace $\bm{w}$
by $\bm{v}$ and we replace $(\bm{\alpha},\bm{\beta})$ by the coarsening
defined by $\bm{v}$.

Next we define $\lambda_{n}$. By the pigeonhole principle there exists an
infinite subsequence $\bm{v}$ of $\bm{w}$ starting with $w_{1},\dots,w_{n}$
such that all runs $\sigma(v_{n},v_{j})$ for $j>n$ have a common prefix
$\lambda_{n}$ which is a run on $\alpha_{n}\otimes\beta_{n}$. Again we replace
$\bm{w}$ by $\bm{v}$ and $(\bm{\alpha},\bm{\beta})$ by the coarsening defined
by $\bm{v}$.

Finally, by Ramsey’s theorem there is an infinite subsequence $\bm{v}$ of
$\bm{w}$ starting with $w_{1},\dots,w_{n}$ such that all runs
$\sigma(v_{i},v_{j})$ for $n<i<j$ have a common prefix $\kappa_{n}$ which is a
run on $\beta_{n}\otimes\beta_{n}$. We replace $\bm{w}$ by $\bm{v}$ and
$(\bm{\alpha},\bm{\beta})$ by the coarsening defined by $\bm{v}$.

In the limit we obtain the desired decomposition of $\rho(v_{i},v_{j})$ and
the generator $(\bm{\alpha},\bm{\beta})$ of a comb $\bm{v}$ that is coarser
than the initial generator of $\bm{w}$. ∎

It is not hard to see that such a comb of combs structure can be simulated by
an alternating Büchi automaton, which would only yield a $\PSPACE$-solution
for the infinite clique problem. The following key lemma states that the runs
$\mu_{i,j}$, $\nu_{i,j}$ from Lemma 4.2 can be chosen independently from $i$,
which reduces the width of the run dag of the alternating automaton to a
constant.

$\ddots$$\alpha_{1}\otimes\beta_{1}$$\beta_{1}\otimes\beta_{1}$$\alpha_{2}\otimes\beta_{2}$$\beta_{2}\otimes\beta_{2}$$\alpha_{3}\otimes\beta_{3}$$\varepsilon\otimes\beta_{2}$$\varepsilon\otimes\beta_{3}$$\varepsilon\otimes\beta_{4}$$\varepsilon\otimes\alpha_{2}$$\varepsilon\otimes\alpha_{3}$$\varepsilon\otimes\alpha_{4}$$\varepsilon\otimes\beta_{3}$$\varepsilon\otimes\beta_{4}$$\varepsilon\otimes\alpha_{3}$$\varepsilon\otimes\alpha_{4}$$\varepsilon\otimes\beta_{4}$$\varepsilon\otimes\alpha_{4}$
Figure 2. If $\bm{v}$ is a comb of the form
$v_{i}=\beta_{1}\dots\beta_{i-1}\alpha_{i}$ then the convolutions
$v_{i}\otimes v_{j}$ for all $i<j$ form a comb of combs.

###### Lemma 4.3.

If $\bm{w}$ is an infinite clique in a regular relation
$R\subseteq\Sigma^{*}\times\Sigma^{*}$ given as an NFA $\mathcal{A}$, then
there exist a generator $(\bm{\alpha},\bm{\beta})$ for a subsequence $\bm{v}$
of $\bm{w}$, accepting runs $\rho(v_{i},v_{j})$ of $\mathcal{A}$ on
$v_{i}\otimes v_{j}$, and runs $\kappa_{i},\lambda_{i},\mu_{j},\nu_{j}$ such
that

$\rho(v_{i},v_{j})=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i+1}\dots\mu_{j-1}\nu_{j}$

is a decomposition compatible with the
$(\bm{\alpha},\bm{\beta})$-decomposition of $v_{i}\otimes v_{j}$ for all
$i<j$.

###### Proof.

Suppose that $R$ has an infinite clique. Then there exist an infinite clique
$\bm{w}$ in $R$ generated by $(\bm{\alpha},\bm{\beta})$ and runs
$\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$ for $i<j$ as in Lemma 4.2.

It remains to ensure that $\mu_{i,j}=\mu_{i^{\prime},j}$ and
$\nu_{i,j}=\nu_{i^{\prime},j}$ for all $i<i^{\prime}<j$. To do so, consider
the initial state of the run $\mu_{i,j+1}$. By Ramsey’s theorem there exist
indices $k_{1}<k_{2}<\dots$ such that all runs $\mu_{k_{i},k_{j}+1}$ have the
same initial state. We define $v_{i}=w_{k_{i}}$ for all $i\geq 1$, and

$\displaystyle\tilde{\kappa}_{i}$
$\displaystyle=\kappa_{k_{i-1}+1}\dots\kappa_{k_{i}}$
$\displaystyle\tilde{\lambda}_{i}$
$\displaystyle=\kappa_{k_{i-1}+1}\dots\kappa_{k_{i}-1}\lambda_{k_{i}},$
$\displaystyle\tilde{\mu}_{i+1}$
$\displaystyle=\mu_{k_{1},k_{i}+1}\dots\mu_{k_{1},k_{i+1}}$
$\displaystyle\tilde{\nu}_{i+1}$
$\displaystyle=\mu_{k_{1},k_{i}+1}\dots\mu_{k_{1},k_{i+1}-1}\nu_{k_{1},k_{i+1}},$

for all $i\geq 1$ where $k_{0}:=0$. Observe that the composition
$\tilde{\lambda}_{i}\tilde{\mu}_{i+1}$ forms a valid run since
$\mu_{k_{i},k_{i}+1}$ and $\mu_{k_{1},k_{i}+1}$ have the same initial state.
Then
$\tilde{\kappa}_{1}\dots\tilde{\kappa}_{i-1}\tilde{\lambda}_{i}\tilde{\mu}_{i+1}\dots\tilde{\mu}_{j-1}\tilde{\nu}_{j}$
is an accepting run on $v_{i}\otimes v_{j}$. Furthermore, this run
decomposition is compatible with the $(\bm{\delta},\bm{\gamma})$-decomposition
of $v_{i}\otimes v_{j}$ where the generator $(\bm{\delta},\bm{\gamma})$ is
defined as

$\displaystyle\delta_{i}$ $\displaystyle=\beta_{k_{i-1}+1}\dots\beta_{k_{i}}$
$\displaystyle\gamma_{i}$
$\displaystyle=\beta_{k_{i-1}+1}\dots\beta_{k_{i}-1}\alpha_{k_{i}}$

for all $i\geq 1$ where $k_{0}:=0$. This concludes the proof. ∎

A _nondeterministic Büchi automaton_ (NBA) has the same format as an NFA
$\mathcal{B}=(Q,\Sigma,\Delta,q_{0},F)$. An infinite word
$w\in\Sigma^{\omega}$ is accepted by $\mathcal{B}$ if there exists an
accepting run $(q_{0},a_{1},q_{1})(q_{1},a_{2},q_{2})\dots\in\Delta^{\omega}$
with $w=a_{1}a_{2}\dots$ and $q_{i}\in F$ for infinitely many $i\geq 0$.

###### Proposition 4.4.

Given an NFA $\mathcal{A}$ for a relation $R\subseteq(\Sigma^{*})^{2}$, one
can construct in logarithmic space a Büchi automaton $\mathcal{B}$ over the
alphabet $(\Sigma_{\bot}\times\Sigma)\cup\\{\\#\\}$ such that:

  * •

If $\bm{w}$ is an infinite clique in $R$ then $\mathcal{B}$ accepts an
encoding of a comb $\bm{v}$ which is a subsequence of $\bm{w}$.

  * •

If $\mathcal{B}$ accepts an encoding of a comb $\bm{w}$ then $\bm{w}$ is an
infinite clique in $R$.

For the proof we construct a Büchi automaton $\mathcal{B}$ that simulates the
runs $\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ from Lemma 4.3 in four
components. We refer to Appendix B for the detailed construction.

$\lambda_{1}$$\kappa_{1}$$\lambda_{2}$$\kappa_{2}$$\lambda_{3}$$\kappa_{3}$$\mu_{1,2}$$\mu_{1,3}$$\mu_{1,4}$$\mu_{1,5}$$\nu_{1,2}$$\nu_{1,3}$$\nu_{1,4}$$\nu_{1,5}$$\mu_{2,3}$$\mu_{2,4}$$\mu_{2,5}$$\nu_{2,3}$$\nu_{2,4}$$\nu_{2,5}$$\mu_{3,4}$$\mu_{3,5}$$\nu_{3,4}$$\nu_{3,5}$
Figure 3. One can always find an infinite comb clique $\bm{v}$ with accepting
runs which can be decomposed in the form
$\rho(v_{i},v_{j})=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,j-1}\nu_{i,j}$.

###### Proof of Theorem 2.2.

First observe that we can construct in log-space an NFA $\mathcal{C}$ over
$\Sigma$ such that (i) for every infinite clique $\bm{w}$ of $R$ some element
$w_{i}$ is accepted by $\mathcal{C}$, and (ii) if $w$ is accepted by
$\mathcal{C}$ then $w$ belongs to an infinite clique of $R$. To be more
precise, $\mathcal{C}$ accepts $\alpha_{1}\in\Sigma^{*}$ if and only if some
encoding $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ is accepted by the Büchi
automaton $\mathcal{B}$ from Proposition 4.4. This can be done in log-space as
follows: First we construct a Büchi automaton $\hat{\mathcal{C}}$ over
$\Sigma\cup\\{\\#\\}$ which accepts all words of the form
$\alpha_{1}\\#^{\omega}$ such that an encoding
$\mathrm{enc}(\bm{\alpha},\bm{\beta})$ is accepted by $\mathcal{B}$. Then
$\hat{\mathcal{C}}$ is turned into an NFA $\mathcal{C}$ (which does not read
the suffix $\\#^{\omega}$) by replacing $\\#$-transitions by
$\varepsilon$-transitions. Furthermore $\mathcal{C}$ tracks the number of
final states visited so far and accepts if and only if this number exceeds the
number of states in $\hat{\mathcal{C}}$.

Given an NFA $\mathcal{A}$ for $R\subseteq(\Sigma^{*})^{k+2}$. We first
construct an NFA $\mathcal{A}^{\prime}$ over $\Sigma_{\bot}^{2k+2}$ which
accepts the regular binary relation

$R^{\prime}=\\{(u\otimes c_{1}\otimes\dots\otimes c_{k},v\otimes
c_{1}\otimes\dots\otimes c_{k})\mid(u,v,\bm{c})\in R\\}.$

Note that $\mathcal{A}^{\prime}$ can be constructed in logspace since it is
obtained by taking each transition of $\mathcal{A}$ and duplicating the
$\bm{c}$-coordinates and moving the $v$-coordinate. Let $\mathcal{C}^{\prime}$
be the NFA described above which accepts at least one word from each infinite
$R^{\prime}$-clique and only accepts elements of infinite
$R^{\prime}$-cliques. Projecting away the first component yields the desired
NFA for $\\{\bm{c}\in(\Sigma^{*})^{k}\mid\exists^{\mathrm{ram}}x,y\colon
R(x,y,\bm{c})\\}$. ∎

##  5\. Tree-automatic structures

###  5.1. $\EXP$-hardness

1121223121 22 31 2 3 Figure 4. Left: Illustration of the tree automaton
$\mathcal{T}$, tracking the number of right directions modulo $n$. Right: A
path on which the runs of $\mathcal{T}$ are disjoint.

In this section we prove the exponential lower bound from Theorem 2.3 for the
infinite clique problem over trees. This lower bound is surprising since over
words, the infinite clique problem can be reduced to the emptiness of (word)
Büchi automata, which is $\NL$-complete. This is not the case in the tree case
since emptiness of Büchi tree automata is $\P$-complete.

We start with an intutive explanation of the lower bound. To prove the upper
bound in the word case, we used the fact that we can assume cliques $\bm{v}$
whose runs $\rho(v_{i},v_{j})$ can be merged into a _single_ global run (Lemma
4.3). Over tree regular relations this is not the case anymore. Consider a
deterministic top-down tree automaton $\mathcal{T}$, which behaves as follows
on the convolution $t\otimes t^{\prime}$ of two binary trees $t,t^{\prime}$
with $\mathrm{dom}(t)\subsetneq\mathrm{dom}(t^{\prime})$: Starting from every
node on the fringe of $t$, the automaton tracks the number of times it moves
to a right child, modulo some number $n$; see Figure 4 for a depiction. Now
consider an increasing sequence of binary trees $t_{1},t_{2},\dots$, and the
unique runs $\rho_{i,j}$ of $\mathcal{T}$ on $t_{i}\otimes t_{j}$. Figure 4
illustrates that we can always find a path on which the runs
$\rho_{1,n},\rho_{2,n},\dots,\rho_{n-1,n}$ are disjoint. This behavior
indicates that it is difficult to witness the existence of infinite cliques by
a polynomially-sized Büchi tree automaton.

We extend this idea to a reduction from the intersection non-emptiness problem
for tree automata, which is known to be $\EXP$-complete (Frühwirth et al.,
1991): Given an NTA $\mathcal{A}=(Q,\Sigma,\Delta,q_{0})$ and states
$q_{1},\dots,q_{n}\in Q$, decide whether
$\bigcap_{i=1}^{n}L(\mathcal{A}_{q_{i}})$ is non-empty. Here,
$\mathcal{A}_{q_{i}}$ denotes the NTA $\mathcal{A}$ with initial state
$q_{i}$.

We construct a relation $R$ on decorated trees, which are obtained from a
binary tree by attaching to every inner node $u$ a ranked tree $\delta(u)$
over $\Sigma$. Let $\Gamma:=\Sigma\cup\\{a,c\\}$ be a ranked alphabet with
$\mathrm{rk}(a)=3,~{}\mathrm{rk}(c)=0$. A decorated tree is a tree
$t\in\mathcal{T}_{\Gamma}$ such that $t(\varepsilon)\in\\{a,c\\}$ and for all
$u\in\mathrm{dom}(t)$ we have

  * •

$t(u1)=t(u2)\in\\{a,c\\}$ and $t(u3)\in\Sigma$ if $t(u)=a$ and

  * •

$t(ui)\in\Sigma$ for all $i\in[1,\mathrm{rk}(t(u))]$ if $t(u)\in\Sigma$.

We denote by $a(t):=\\{u\in\mathrm{dom}(t)\mid t(u)=a\\}$ the nodes of $t$
labeled with $a$ and by $ac(t):=\\{u\in\mathrm{dom}(t)\mid
t(u)\in\\{a,c\\}\\}$ the nodes labeled with $a$ or $c$. The _decoration_ of
$t$ is a function $\delta_{t}\colon a(t)\to\mathcal{T}_{\Sigma}$ such that
$\delta_{t}(u)=t_{\downarrow u3}$ where $t_{\downarrow v}$ denotes the subtree
of $t$ rooted in $v\in\mathrm{dom}(t)$.

Let $\mathcal{A}^{\prime}=(Q^{\prime},\Gamma,\Delta^{\prime},p_{1})$ be the
NTA where $Q^{\prime}:=Q\cup\\{p_{1},\dots,p_{n}\\}$ and $\Delta^{\prime}$
contains all transitions from $\Delta$ and the transitions

$\displaystyle p_{i}$ $\displaystyle\xrightarrow{a}(p_{i},p_{i+1},q_{i})\text{
for all }i\in[1,n]\text{ where }p_{n+1}:=p_{1},$ $\displaystyle p_{i}$
$\displaystyle\xrightarrow{c}()\text{ for all }i\in[1,n].$

We define the tree-regular relation
$R\subseteq\mathcal{T}_{\Gamma}\times\mathcal{T}_{\Gamma}$ such that $(s,t)\in
R$ if and only if $s$ and $t$ are decorated trees with $ac(s)\subseteq a(t)$
and $\mathcal{A}^{\prime}$ accepts $t_{\downarrow u}$ for all
$u\in\min(a(t)\setminus a(s))$. Here, the minimum is defined with respect to
prefix ordering. It is easy to construct an NTA that recognizes $R$ in
logspace.

It remains to show that $\bigcap_{i=1}^{n}L(\mathcal{A}_{q_{i}})\neq\emptyset$
if and only if $R$ contains an infinite clique. For the “only if” direction
let $t\in\mathcal{T}_{\Sigma}$ be a tree that is accepted by
$\mathcal{A}_{q_{i}}$ for all $i\in[1,n]$. For all $i\geq 0$ we define the
decorated tree $t_{i}\in\mathcal{T}_{\Gamma}$ such that
$ac(t_{i})=\bigcup_{j=0}^{i}\\{1,2\\}^{j}$ and $\delta_{t_{i}}(u)=t$ for all
$u\in a(t_{i})$. It is easy to verify that $(t_{i},t_{j})\in R$ for all $i<j$.

Conversely, consider a sequence of decorated trees
$t_{i}\in\mathcal{T}_{\Gamma}$ for $i\geq 0$ with $(t_{i},t_{j})\in R$ for all
$i<j$. We define nodes $v_{1},\dots,v_{n}$ with

  * •

$v_{i}\in\min(a(t_{i})\setminus a(t_{i-1}))$ for all $i\in[1,n]$ and

  * •

$v_{i+1}=v_{i}21^{k_{i}}$ for all $i\in[1,n-1]$ and some $k_{i}\geq 0$.

We can choose $v_{1}\in\min(a(t_{1})\setminus a(t_{0}))$ arbitrary which
defines $v_{2},\dots,v_{n}$ uniquely. Since $(t_{i-1},t_{n})\in R$ and
$v_{i}\in\min(a(t_{n})\setminus a(t_{i-1}))$, the subtree ${t_{n}}_{\downarrow
v_{i}}$ is accepted by $\mathcal{A}^{\prime}$ for all $i\in[1,n]$. By
definition of $\mathcal{A}^{\prime}$ there exist accepting runs on
${t_{n}}_{\downarrow v_{n}}$ starting from $p_{1},\dots,p_{n}$. Therefore, the
tree $\delta_{t_{n}}(v_{n})\in\mathcal{T}_{\Sigma}$ is accepted by
$\mathcal{A}$ starting from all states $q_{1},\dots,q_{n}$.

We note that $\EXP$-hardness already holds if $R$ is given by a
D$\downarrow$TA since intersection nonemptiness is $\EXP$-hard already for
D$\downarrow$TAs (Seidl, 1994), and if the automaton $\mathcal{A}$ is a
D$\downarrow$TA, then the constructed relation $R$ from the proof can also be
recognized by a D$\downarrow$TA. Moreover, the reduction can be adapted to
recurrent reachability by setting the target set to $\mathcal{T}_{\Sigma}$,
which proves the exponential lower bound in Corollary 2.7.

###  5.2. Tree combs

To prove the upper bounds for tree-regular relations, we extend the notion of
combs to the tree case. Here a tree $t_{i}$ is decomposed vertically in the
form $t_{i}=\beta_{1}\dots\beta_{i-1}\alpha_{i}$ where $\beta_{1}$ is a
context, $\beta_{2},\dots,\beta_{i-1}$ are forests of contexts, and
$\alpha_{i}$ is a forest of trees, see Figure 5 for an abstract illustration.

A _context forest_ of width $n$ is a finite sequence $\tau=(c_{i})_{1\leq
i\leq n}$ of contexts $c_{i}\in\mathcal{C}_{\Sigma}$. Context forests of width
1 are regarded as contexts. We say that $\tau$ is nontrivial if $n\geq 1$ and
$|c_{i}|\geq 1$ for all $1\leq i\leq n$. If the $c_{i}$ are trees in
$\mathcal{U}_{\Sigma}$, we call $\tau$ just a _forest_. We define the
concatenation of a context $\tau_{1}\in\mathcal{C}_{\Sigma}$ of width $n$ with
a context forest $\tau_{2}=(c_{1},\dots,c_{n})\in\mathcal{F}_{\Sigma}$ by
$\tau_{1}\tau_{2}:=\tau_{1}[c_{1},\dots,c_{n}]$. Assuming left-associativity
we write $\tau_{1}\tau_{2}\dots\tau_{n}$ for a context $\tau_{1}$ and context
forests $\tau_{2},\dots,\tau_{n}$. Here we implicitly assume that the width of
$\tau_{i}$ matches $|\mathrm{holes}(\tau_{1}\dots\tau_{i-1})|$. If $t$ is a
tree and $s$ is a context, we write $t\triangleleft s$ if
$\mathrm{dom}(t)\cap\mathrm{holes}(s)=\emptyset$. For a forest
$\alpha=(t_{i})_{i\leq n}$ and a context forest $\beta=(s_{i})_{i\leq n}$ we
also write $\alpha\triangleleft\beta$ if $t_{i}\triangleleft s_{i}$ for all
$1\leq i\leq n$.

An infinite sequence $\bm{t}=(t_{i})_{i\geq 1}$ of ranked trees is called a
comb if there is a sequence of forests $\bm{\alpha}=(\alpha_{i})_{i\geq 1}$
and a sequence of nontrivial context forests $\bm{\beta}=(\beta_{i})_{i\geq
1}$ such that for all $i\geq 1$ we have
$t_{i}=\beta_{1}\dots\beta_{i-1}\alpha_{i}$ and
$\alpha_{i}\triangleleft\beta_{i}$. The pair $(\bm{\alpha},\bm{\beta})$ is
called _generator_ of the comb. Since the trees $t_{i}$ are ranked, also the
trees in $\alpha_{i}$ and the contexts in $\beta_{i}$ are ranked.

The property $\alpha_{i}\triangleleft\beta_{i}$ should be compared to the
property $|\alpha_{i}|\leq|\beta_{i}|$ in word combs. It ensures that every
forest $\alpha_{i}$ does not touch any context forest $\alpha_{j},\beta_{j}$
for $j\neq i$.

###### Lemma 5.1 (Combs lemma over trees).

Any sequence $\bm{t}$ of pairwise distinct ranked trees
$t_{i}\in\mathcal{T}_{\Sigma}$ over a finite ranked alphabet $\Sigma$ contains
a comb as a subsequence.

###### Proof.

It suffices to show that for any infinite set $T\subseteq\mathcal{T}_{\Sigma}$
there exists a comb over $T$. Consider the following finitely branching
infinite tree whose nodes are contexts from $\mathcal{C}_{\Sigma}$. The root
is the context $x$. The children of a context $s$ are the contexts of the form
$s[t_{1},\dots,t_{n}]$ where each $t_{i}$ is a context of size one. Observe
that all trees in $\mathcal{T}_{\Sigma}$ occur as nodes in the infinite tree.
The set of all ancestors of trees in $T$ form an infinite subtree, which
contains an infinite path
$s_{0}<_{\mathsf{p}}s_{1}<_{\mathsf{p}}s_{2}<_{\mathsf{p}}\dots$ by Kőnig’s
Lemma. For all $i\geq 1$ there exists a tree $t_{i}\in T$ which contains
$s_{i-1}$ as a prefix.

Since the minimal level of a hole in $s_{i}$ is strictly increasing, for every
$i\geq 1$ there exists a $j\geq i$ with $t_{i}\triangleleft s_{j}$. Hence one
can inductively construct indices $1=k_{1}<k_{2}<\dots$ such that
$t_{k_{i}+1}\triangleleft s_{k_{i+1}}$ for all $i\geq 1$. Then
$(t_{k_{i}+1})_{i\geq 1}$ is a comb where the generator
$(\bm{\alpha},\bm{\beta})$ is defined such that
$s_{k_{i+1}}=\beta_{1}\dots\beta_{i}$ and
$t_{k_{i}+1}=\beta_{1}\dots\beta_{i-1}\alpha_{i}$ for $i\geq 1$. The comb
property $\alpha_{i}\triangleleft\beta_{i}$ follows from
$t_{k_{i}+1}\triangleleft s_{k_{i+1}}$. ∎

$t_{1}$$\alpha_{1}$$t_{2}$$\beta_{1}$$\alpha_{2}$$t_{3}$$\dots$$\beta_{1}$$\beta_{2}$$\alpha_{3}$encoding
Figure 5. An example tree comb and its encoding as an infinite tree. In this
example the generator satisfies
$\mathrm{dom}(\alpha_{i})\subseteq\mathrm{dom}(\beta_{i})$ whereas general
generators only satisfy $\alpha_{i}\triangleleft\beta_{i}$.

To define the encoding $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ of a comb
generator we need a few more definitions. For a tree $t$ and context $s$ with
$t\triangleleft s$ we define the convolution $t\otimes s$ as before but every
$(\bot,x)$ is replaced by $x$. That is, $t\otimes s$ is again a context. We
extend the convolution in a natural way to forests and context forests of the
same width. If $\tau=(c_{1},\dots,c_{n})$ is a context forest let $\bar{\tau}$
be obtained from $\tau$ by attaching a new $\\#$-labeled root to each of the
$n$ contexts $c_{i}$. We can now define the _encoding_ of a comb with
generator $(\bm{\alpha},\bm{\beta})$ as the infinite tree

$\mathrm{enc}(\bm{\alpha},\bm{\beta}):=(\alpha_{1}\otimes\beta_{1})(\overline{\alpha_{2}\otimes\beta_{2}})(\overline{\alpha_{3}\otimes\beta_{3}})\dots$

over the ranked alphabet $\Omega:=\Sigma_{\bot}^{2}\cup\\{\\#\\}$. See Figure
5 for an illustration of the encoding. Here, the forests $\alpha_{i}$ are
colored red and the context forests $\beta_{i}$ are colored blue. It is not
hard to see that the set $\mathrm{Enc}_{\Sigma}$ of all comb encodings is a
regular language of infinite trees.

###  5.3. Arbitrary relations

An _alternating tree automaton_ (ATA) over the ranked alphabet $\Sigma$ is a
tuple $\mathcal{A}=(Q,\Sigma,\delta,q_{0})$ where $Q$ is a set of states,
$q_{0}\in Q$ is an initial state, and $\delta\colon
Q\times\Sigma\to\mathcal{B}^{+}(Q\times\mathbb{N})$ is a transition function
$\delta(q,a)\in\mathcal{B}^{+}(Q\times\\{1,\dots,\mathrm{rk}(a)\\})$ for all
$q\in Q,~{}a\in\Sigma$. Here, $\mathcal{B}^{+}(Q\times\mathbb{N})$ denotes the
set of positive propositional formulas over the set of variables
$Q\times\mathbb{N}$. For a set $S$ of variables and formula $\varphi$ we
denote by $S\models\varphi$ that if the variables in $S$ are set to true and
the variables not in $S$ are set to false, then $\varphi$ is satisfied.

We will use a nonstandard definition of runs of ATAs. Firstly, we consider
runs on both trees and contexts. Secondly, each node in the run also carries
the labels of its children, with the purpose of predetermining the states in
the context holes. A _run_ of $\mathcal{A}$ on a nontrivial ranked context
$t\in\mathcal{C}_{\Sigma}$ is a context $\rho$ over the alphabet
$\mathbb{N}^{*}\times Q\times 2^{Q\times\mathbb{N}}$ such that
$\rho(\varepsilon)=(\varepsilon,q_{0},S)$ for some $S\subseteq
Q\times\mathbb{N}$ and for each node $u\in\mathrm{nodes}(\rho)$ with
$\rho(u)=(w,q,S)$ and $S=\\{(q_{1},c_{1}),\dots,(q_{r},c_{r})\\}$ we have that
$S\models\delta(q,t(w))$ and $u$ has $r\geq 0$ children such that
$\rho(ui)=(wc_{i},q_{i},S_{i})$ for some $S_{i}\subseteq Q\times\mathbb{N}$ if
$wc_{i}\in\mathrm{nodes}(t)$, and $\rho(ui)=x$, otherwise. Note that an NTA
can be seen as a special ATA where for all $q\in Q$ and $a\in\Sigma$, the
transition formula $\delta(q,a)$ is a disjunction of conjunctions
$\bigwedge_{i=1}^{\mathrm{rk}(a)}(q_{i},i)$.

We define a _decomposition_ of a context $t$ as $t=\tau_{1}\dots\tau_{n}$
where the $\tau_{i}$ are context forests. For a generator
$(\bm{\alpha},\bm{\beta})$ of a comb $\bm{s}$ we define the
$(\bm{\alpha},\bm{\beta})$-decomposition of $s_{i}\otimes s_{j}$ as in the
word case. We say that a decomposition of a run $\rho=\rho_{1}\dots\rho_{n}$
of an ATA is _compatible_ with a decomposition $t=\tau_{1}\dots\tau_{n}$ of a
context if $\rho_{1}\dots\rho_{i}$ is a run on $\tau_{1}\dots\tau_{i}$ for all
$i\in[1,n]$. Note that the above definition of a run ensures that
$\rho_{1}\dots\rho_{i}$ already determines the first two components of the
root labels of $\rho_{i+1}$ for all $i<n$.

We say that a generator $(\bm{\alpha},\bm{\beta})$ of a comb $\bm{s}$ is
_coarser_ than a generator $(\bm{\gamma},\bm{\delta})$ of a comb $\bm{t}$ if
there exist indices $k_{1}<k_{2}<\dots$ such that $s_{i}=t_{k_{i}}$ and
$\beta_{1}\dots\beta_{i}=\delta_{1}\dots\delta_{k_{i}}$ for all $i\geq 1$. In
this case we also say that $(\bm{\alpha},\bm{\beta})$ is the coarsening of
$(\bm{\gamma},\bm{\delta})$ defined by the subsequence $\bm{s}$ of $\bm{t}$.

###### Lemma 5.2.

Let $\bm{t}$ be a comb generated by $(\bm{\gamma},\bm{\delta})$ that forms an
infinite clique in a tree-regular relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ given as an ATA
$\mathcal{A}$. There exist a coarsening $(\bm{\alpha},\bm{\beta})$ of
$(\bm{\gamma},\bm{\delta})$ that generates a comb $\bm{s}$, runs
$\rho(s_{i},s_{j})$ of $\mathcal{A}$ on $s_{i}\otimes s_{j}$, and context
forests $\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$ such that

$\rho(s_{i},s_{j})=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,j-1}\nu_{i,j}$

is a decomposition compatible with the
$(\bm{\alpha},\bm{\beta})$-decomposition of $s_{i}\otimes s_{j}$ for all
$i<j$.

###### Proof.

The proof is similar to the proof of Lemma 4.2 in the word case. We emphasize
that the pigeonhole principle and Ramsey’s theorem can be applied as in the
word case since the unique prefixes of the runs of the ATA that are runs on a
given context have bounded size. Further note that since a run on a forest is
not defined, instead of considering only the suffixes $\tau(t_{i},t_{j})$ and
$\sigma(t_{i},t_{j})$ in the inductive step, we have to consider the whole run
$\rho(t_{i},t_{j})$ and extend the common prefix that is already fixed. ∎

An _alternating Büchi tree automaton_ (ABTA) over the ranked alphabet $\Sigma$
is a tuple $\mathcal{A}=(Q,\Sigma,\delta,q_{0},F)$ where $Q$, $\Sigma$,
$\delta$, and $q_{0}$ are as in the definition of an ATA and $F\subseteq Q$ is
a set of final states. A _run_ of $\mathcal{A}$ on a finite or infinite tree
$t\in\mathcal{T}_{\Sigma}^{\infty}$ is a tree
$\rho\in\mathcal{U}_{\mathbb{N}^{*}\times Q}^{\infty}$ such that
$\rho(\varepsilon)=(\varepsilon,q_{0})$ and for all $u\in\mathrm{dom}(\rho)$
with $\rho(u)=(w,q)$ and children $u1,\dots,ur$ there is a satisfying
assignment $S=\\{(q_{1},c_{1}),\dots,(q_{r},c_{r})\\}\models\delta(q,t(w))$ of
pairwise distinct $(q_{i},c_{i})$ such that $\rho(ui)=(wc_{i},q_{i})$ for all
$i\in[1,r]$. A run $\rho$ is _accepting_ if every infinite path of $\rho$
contains infinitely many nodes with labels in $\mathbb{N}^{*}\times F$.

###### Proposition 5.3.

Given an ATA $\mathcal{A}$ for a tree-regular relation
$R\subseteq(\mathcal{T}_{\Sigma})^{2}$, one can construct in polynomial time
an ABTA $\mathcal{B}$ over the ranked alphabet
$\Omega=\Sigma_{\bot}^{2}\cup\\{\\#\\}$ such that we have:

  * •

If $\bm{t}$ is an infinite clique in $R$, then $\mathcal{B}$ accepts an
encoding of a comb $\bm{s}$ which is a subsequence of $\bm{t}$.

  * •

If $\mathcal{B}$ accepts $t\in\mathcal{T}_{\Omega}^{\infty}$, then $t$ is an
encoding of a comb $\bm{t}$ that is an infinite clique in $R$.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma_{\bot}^{2},\delta,q_{0})$ be the ATA that
recognizes $R$. We construct an ABTA $\mathcal{B}$ over $\Omega$ which accepts
precisely all comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ with the
properties from Lemma 5.2. The state set of $\mathcal{B}$ is
$Q\times\\{1,2,3,4\\}$, representing four different modes. In the first mode
it simulates $\kappa_{j}$ on $\beta_{j}\otimes\beta_{j}$, in the second mode
it simulates $\lambda_{j}$ on $\alpha_{j}\otimes\beta_{j}$, in the third mode
it simulates $\mu_{i,j}$ on $\varepsilon\otimes\beta_{j}$, and in the fourth
mode it simulates $\nu_{i,j}$ on $\varepsilon\otimes\alpha_{j}$. Figure 3
illustrates the simulation.

For all $q\in Q$ and $\begin{pmatrix}a\\\ b\end{pmatrix}\in\Sigma_{\bot}^{2}$
we set

$\displaystyle\delta_{\mathcal{B}}((q,1),\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle:=\delta_{1}(q,\begin{pmatrix}b\\\ b\end{pmatrix})$
$\displaystyle\delta_{\mathcal{B}}((q,2),\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle:=\delta_{2}(q,\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle\delta_{\mathcal{B}}((q,3),\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle:=\delta_{3}(q,\begin{pmatrix}\bot\\\ b\end{pmatrix})$
$\displaystyle\delta_{\mathcal{B}}((q,4),\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle:=\delta_{4}(q,\begin{pmatrix}\bot\\\ a\end{pmatrix})$

where $\delta_{i}(q,\sigma)$ is the formula $\delta(q,\sigma)$ where each
variable $(p,c)$ is replaced by $((p,i),c)$. At the holes of
$\alpha_{j}\otimes\beta_{j}$ labeled with $\\#$, i.e., the points where
$\alpha_{j+1}\otimes\beta_{j+1}$ starts, the simulations in modes 1,2, and 3
split up. For all $q\in Q$ we define

$\displaystyle\delta_{\mathcal{B}}((q,1),\\#)$
$\displaystyle:=((q,1),1)\wedge((q,2),1)$
$\displaystyle\delta_{\mathcal{B}}((q,2),\\#):=\delta_{\mathcal{B}}((q,3),\\#)$
$\displaystyle:=((q,3),1)\wedge((q,4),1)$

Finally, we add a new initial state $q_{0}^{\mathcal{B}}$ which spawns
simulations of $\mathcal{A}$ in mode 1 and 2, i.e., for all $q\in Q$ and
$\begin{pmatrix}a\\\ b\end{pmatrix}\in\Sigma_{\bot}^{2}$ we define

$\delta_{\mathcal{B}}(q_{0}^{\mathcal{B}},\begin{pmatrix}a\\\
b\end{pmatrix}):=\delta_{1}(q_{0},\begin{pmatrix}b\\\
b\end{pmatrix})\wedge\delta_{2}(q_{0},\begin{pmatrix}a\\\ b\end{pmatrix}).$

Finally, we intersect $L(\mathcal{B})$ with the tree-regular language
$\mathrm{Enc}_{\Sigma}$, which concludes the proof. ∎

If $R$ is given by a D$\uparrow$TA we can even compute in polynomial-time a
nondeterministic Büchi tree automaton (NBTA) for the representation of
infinite cliques. The proof idea is that the runs $\mu_{i,j}$ and $\nu_{i,j}$
in Lemma 5.2 only depend on $j$.

###### Proposition 5.4.

Given a D$\uparrow$TA $\mathcal{A}$ for a tree-regular relation
$R\subseteq(\mathcal{T}_{\Sigma})^{2}$, one can construct in polynomial time
an NBTA $\mathcal{B}$ over the ranked alphabet
$\Omega=\Sigma_{\bot}^{2}\cup\\{\\#\\}$ such that we have:

  * •

If $\bm{t}$ is an infinite clique in $R$, then $\mathcal{B}$ accepts an
encoding of a comb $\bm{s}$ which is a subsequence of $\bm{t}$.

  * •

If $\mathcal{B}$ accepts $t\in\mathcal{T}_{\Omega}^{\infty}$, then $t$ is an
encoding of a comb $\bm{t}$ that is an infinite clique in $R$.

We are ready to prove Theorem 2.4. If $\mathcal{A}$ is an ATA, we use the ABTA
$\mathcal{B}$ from Proposition 5.3 and transform it into an NBTA in
exponential time (Muller and Schupp, 1995, Theorem 1.2). If $\mathcal{A}$ is a
D$\uparrow$TA $\mathcal{A}$ we use the NBTA $\mathcal{B}$ from Proposition
5.4. We then construct an NTA $\mathcal{C}$ over $\Sigma$ which accepts
$t_{1}\in\mathcal{T}_{\Sigma}$ if and only if the encoding of some comb
$(t_{i})_{i\geq 1}$ is accepted by $\mathcal{B}$. The rest of the proof is
analogous to the proof of Theorem 2.2, see Appendix B for details.

###  5.4. Transitive relations

In this section we show that if we assume that $R$ is transitive, then the
Ramsey quantifier can be evaluated in polynomial time (Theorem 2.5).

###### Proposition 5.5.

Given an NTA $\mathcal{A}$ for a transitive tree-regular relation
$R\subseteq(\mathcal{T}_{\Sigma})^{2}$, one can construct in polynomial time
an NBTA $\mathcal{B}$ over the ranked alphabet $\Omega$ such that:

  * •

If $\bm{t}$ is an infinite clique in $R$, then $\mathcal{B}$ accepts an
encoding of a comb $\bm{s}$ which is a subsequence of $\bm{t}$.

  * •

If $\mathcal{B}$ accepts $t\in\mathcal{T}_{\Omega}^{\infty}$, then $t$ is an
encoding of a comb $\bm{t}$ that is an infinite clique in $R$.

For the proof we view $\mathcal{A}$ as an ATA and construct the ABTA
$\mathcal{B}$ as in the proof of Proposition 5.3 which accepts precisely all
comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ with the properties from
Lemma 5.2. By transitivity of $R$ we can omit all states in mode 3. Then any
run contains for each node $v$ of the input tree at most three run nodes
referring to $v$. Thus, we can apply a standard powerset construction to
convert $\mathcal{C}$ into an equivalent NBTA of polynomial size by
restricting to subsets of states of size at most three. We refer to Appendix B
for more details. Using the polynomially-sized NBTA $\mathcal{B}$ we can prove
Theorem 2.5 analogously to Theorem 2.4.

###  5.5. Co-transitive relations

Recall that a binary relation $R\subseteq A\times A$ is co-transitive if its
complement $\bar{R}=(A\times A)\setminus R$ is transitive. Next we show
Theorem 2.6.

A context $\beta$ is called monadic if it has exactly one hole. We will show
that, if a co-transitive relation has an infinite clique, then there exists
one which is a comb generated by a monadic generator
$(\bm{\alpha},\bm{\beta})$ in which all forests $\beta_{i}$ are monadic
contexts. This also implies that all $\alpha_{i}$ are trees.

###### Lemma 5.6.

If a co-transitive tree-regular relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ has an infinite
clique over a tree-regular language $L\subseteq\mathcal{T}_{\Sigma}$, then
there exists an infinite clique $\bm{t}$ of $R$ over $L$ and a nontrivial
monadic context $\beta$ with $t_{1}\triangleleft\beta$ and
$\beta\leq_{\mathsf{p}}t_{i}$ for all $i\geq 2$.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma_{\bot}^{2},\Delta,F)$ and
$\mathcal{B}=(P,\Sigma,\Lambda,G)$ be D$\uparrow$TAs for $R$ and $L$,
respectively. Suppose that $\bm{t}$ is an infinite clique in $R$ over $L$. For
$j\geq 2$ let $c_{j}$ be the unique context with
$\mathrm{nodes}(c_{j})=\mathrm{nodes}(t_{1})\cap\mathrm{nodes}(t_{j})$ and
$c_{j}\leq_{\mathsf{p}}t_{j}$. Notice that $c_{j}$ is nontrivial since $t_{1}$
and $t_{j}$ contain the root. Furthermore we have $t_{1}\triangleleft c_{j}$
since any hole $u\in\mathrm{holes}(c_{j})$ is contained in
$\mathrm{nodes}(t_{j})\setminus\mathrm{nodes}(c_{j})$. Since there are only
finitely many such choices for $c_{j}$, by reducing $\bm{t}$ to a subsequence
which starts with $t_{1}$ we can assume that $c_{j}=c$ for all $j\geq 2$ for
some context $c$. Suppose that $v^{1},\dots,v^{n}$ are the holes of $c$ in
lexicographical order, and $t_{j}=c[t_{j}^{1},\dots,t_{j}^{n}]$ for some trees
$t_{j}^{k}$. For all $i<j$ we have

$t_{i}\otimes t_{j}=\begin{cases}(t_{1}\otimes c)[\varepsilon\otimes
t_{j}^{1},\dots,\varepsilon\otimes t_{j}^{n}],&1=i<j,\\\ (c\otimes
c)[t_{i}^{1}\otimes t_{j}^{1},\dots,t_{i}^{n}\otimes
t_{j}^{n}],&1<i<j,\end{cases}$

where $t_{1}\otimes c$ and $c\otimes c$ are naturally viewed as contexts with
$n$ holes. For $j\geq 2$ consider the accepting run $\rho_{j}$ of
$\mathcal{A}$ on $t_{1}\otimes t_{j}$ and the accepting run $\pi_{j}$ of
$\mathcal{B}$ on $t_{j}$, and color each index $j$ by the tuple
$(\rho_{j}(v^{1}),\dots,\rho_{j}(v^{n}),\pi_{j}(v^{1}),\dots,\pi_{j}(v^{n}))$.
By the pigeonhole principle we can pick numbers $1=\ell_{1}<\ell_{2}<\dots$
such that $\\{\ell_{2},\ell_{3},\dots\\}$ is monochromatic. We then replace
$\bm{t}$ by $(t_{\ell_{i}})_{i\geq 1}$. Hence, the accepting runs of
$\mathcal{A}$ on $t_{1}\otimes t_{j}$ ($j\geq 2$) visit the same states
$r^{1},\dots,r^{n}$ in the nodes $v^{1},\dots,v^{n}$. Similarly, the accepting
runs of $\mathcal{B}$ on the trees $t_{j}$ visit the same states
$p^{1},\dots,p^{n}$ in the nodes $v^{1},\dots,v^{n}$. Therefore

$\displaystyle(t_{1},c[t_{j_{1}}^{1},\dots,t_{j_{n}}^{n}])$ $\displaystyle\in
R$ $\displaystyle\text{for any }j_{1},\dots,j_{n}\geq 2~{}~{}\text{and}$
$\displaystyle c[t_{j_{1}}^{1},\dots,t_{j_{n}}^{n}]$ $\displaystyle\in L$
$\displaystyle\text{for any }j_{1},\dots,j_{n}\geq 2.$

For $1<i<j$ consider an accepting run of $\mathcal{A}$ on $t_{i}\otimes t_{j}$
and let $q_{i,j}^{k}$ be the state reached in node $v^{k}$. By Ramsey’s
theorem we can assume that there exist states $q^{1},\dots,q^{n}\in Q$ such
that $q_{i,j}^{k}=q^{k}$ for all $1<i<j$ (again, after replacing $\bm{t}$ by a
subsequence starting with $t_{1}$). Observe that $\mathcal{A}$ accepts the
context $c\otimes c$ if it starts in nodes $v^{1},\dots,v^{k}$ with the states
$q^{1},\dots,q^{k}$, respectively.

For every $0\leq k\leq n$ define the tree

$s_{k}=c[t_{3}^{1},\dots,t_{3}^{k},t_{2}^{k+1},\dots,t_{2}^{n}].$

We have $(s_{0},s_{n})=(t_{2},t_{3})\in R$. There must be an index $1\leq
k\leq n$ with $(s_{k-1},s_{k})\in R$ since otherwise by transitivity of
$\bar{R}$ we would have $(s_{0},s_{n})\notin R$. Define the context
$\beta=c[t_{3}^{1},\dots,t_{3}^{k-1},x,t_{2}^{k+1},\dots,t_{2}^{n}]$. Then we
have that $(\beta[t_{2}^{k}],\beta[t_{3}^{k}])\in R$. This is witnessed by an
accepting run on their convolution, which reaches state $q^{k}$ at node
$v^{k}$. This implies that $(\beta[t_{i}^{k}],\beta[t_{j}^{k}])\in R$ for all
$i<j$, since the run of $\mathcal{A}$ on $t_{i}^{k}\otimes t_{j}^{k}$ also
reaches $q^{k}$. Hence, the context $\beta$ together with the trees $t_{1}$
and $\beta[t_{i}^{k}]$ for $i\geq 2$ satisfy the claim. Moreover,
$t_{1}\triangleleft c$ and $c\leq_{\mathsf{p}}\beta$ implies
$t_{1}\triangleleft\beta$. ∎

Repeated applications of Lemma 5.6 yields the desired infinite clique:

###### Lemma 5.7.

If a co-transitive tree-regular relation $R$ has an infinite clique then there
exists an infinite clique $\bm{t}$ of $R$ generated by a monadic generator
$(\bm{\alpha},\bm{\beta})$.

###### Proof.

Let $n\in\mathbb{N}$ and suppose we have inductively constructed trees
$\alpha_{1},\dots,\alpha_{n}$, and nontrivial monadic contexts
$\beta_{1},\dots,\beta_{n}$, with $\alpha_{i}\triangleleft\beta_{i}$ for all
$1\leq i\leq n$, such that there exist trees $(t_{i}^{\prime})_{i>n}$ such
that $(t_{i})_{i\geq 1}$ is an infinite clique in $R$ where
$t_{i}=\beta_{1}\beta_{2}\dots\beta_{i-1}\alpha_{i}$ if $i\leq n$, and
$t_{i}=\beta_{1}\beta_{2}\dots\beta_{n}t_{i}^{\prime}$ if $i>n$. Let
$\beta:=\beta_{1}\beta_{2}\dots\beta_{n}$. Then $(t_{i}^{\prime})_{i>n}$ is an
infinite clique in the relation
$R^{\prime}=\\{(s^{\prime},t^{\prime})\mid(\beta[s^{\prime}],\beta[t^{\prime}])\in
R\\}$. It is easy to see that $R^{\prime}$ is again tree-regular and co-
transitive. Furthermore all trees $t_{i}^{\prime}$ for $i>n$ belong to the
tree-regular language $L=\bigcap_{i=1}^{n}\\{t\mid(t_{i},\beta[t])\in R\\}$.
We can apply Lemma 5.6 and obtain a tree $\alpha_{n+1}$, a nontrivial monadic
context $\beta_{n+1}$ with $\alpha_{n+1}\triangleleft\beta_{n+1}$, and trees
$(t_{i}^{\prime\prime})_{i>n+1}$ such that $\alpha_{n+1}$ together with
$\beta_{n+1}[t_{i}^{\prime\prime}]$ for $i>n+1$ form an infinite clique in
$R^{\prime}$. Furthermore all trees $\beta_{n+1}[t_{i}^{\prime\prime}]$ for
$i>n+1$ belong to $L$. Hence $t_{1},\dots,t_{n}$ together with
$\beta[\alpha_{n+1}]$ and $\beta[\beta_{n+1}[t_{i}^{\prime\prime}]]$ for
$i>n+1$ form an infinite clique in $R$. By induction we then obtain the
desired sequences $\bm{\alpha},\bm{\beta}$. ∎

We can now prove Theorem 2.6. Given an NTA $\mathcal{A}$ for a co-transitive
relation $R$. Using Lemmas 5.7 and 5.2, we can prove a statement similar to
Lemma 4.3 for tree combs which are generated by a monadic generator. In
particular, all context forests $\kappa_{i},\lambda_{i},\mu_{j}$ have exactly
one hole, and hence $\kappa_{i},\lambda_{i},\mu_{j},\nu_{j}$ are in fact
contexts.

Now we can construct in polynomial time a Büchi tree automaton $\mathcal{B}$
which accepts all comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ of a
monadic generator $(\bm{\alpha},\bm{\beta})$ for which runs of the form
$\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ as above exist. To this end,
$\mathcal{B}$ consists of four components in which the runs
$\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ are simulated. The detailed
construction can be found in Appendix B.

##  6\. Applications

###  6.1. Recurrent reachability with generalized Büchi condition

The proof of the following Proposition can be found in Appendix C.

###### Proposition 6.1.

The infinite clique problem and recurrent reachability are logspace equivalent
over (tree-)regular relations. Moreover, the logspace reduction from recurrent
reachability to the infinite clique problem preserves transitivity of
relations and determinism of automata.

Using the proposition we obtain tight bounds on the complexity of recurrent
reachability over (transitive) (tree-)regular relations. We can even compute
an automaton for the set $\mathit{Rec}(L)[R]$ of initial elements given
automata for $R$ and $L$.

###### Corollary 6.2.

If $R$ is a binary (tree-)regular relation and $L$ is a (tree-)regular
language given by NFAs (NTAs), then one can construct an NFA (NTA) for
$\mathit{Rec}(L)[R]$ in logspace (exponential time). The construction works in
polynomial time if $R$ and $L$ are given by D$\uparrow$TAs or if $R$ is
transitive.

###### Proof.

We can define $\mathit{Rec}(L)[R]$ by the formula

$\displaystyle\varphi(x)=\exists^{\mathrm{ram}}y,z\colon$ $\displaystyle
R(x,y)\wedge L(y)\wedge R(y,z)$ $\displaystyle\vee\,\exists y\colon$
$\displaystyle R(x,y)\wedge L(y)\wedge R(y,y).$

If $R$ and $L$ are given by NFAs, we can construct in logspace an NFA for
$\mathit{Rec}(L)[R]$ using the closure properties of regular relations and
Theorem 2.2. Over trees, we use Theorems 2.4 and 2.5 to construct an NTA for
$\mathit{Rec}(L)[R]$ in exponential or polynomial time depending on whether
$R$ is transitive and how $R,L$ are given. ∎

For recurrent reachability with generalized Büchi condition we show that over
words the complexity increases from $\NL$ to $\PSPACE$, while over trees it
stays in $\EXP$ (Theorem 2.8).

For both the word and the tree case we reduce the generalized version to the
classical version. First observe that
$a_{0}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ if and only if there is a
sequence $\bm{a}$ such that $(a_{i},a_{j})\in R$ for all $0\leq i<j$ and
$a_{i}\in L_{((i-1)\text{ mod }k)+1}$ for all $i\geq 1$. We define a
(tree-)regular relation $R^{\prime}\subseteq A^{k}\times A^{k}$ that checks if
a tuple $(a_{1},\dots,a_{2k})$ forms a clique of size $2k+1$ in $R$ starting
with $a_{0}$ such that $a_{i}\in L_{i}$ for all $i\in[1,k]$. In the word case
the NFA $\mathcal{A}^{\prime}$ for $R^{\prime}$ can be constructed in
$\PSPACE$ using a product construction. In the tree case we can avoid the
exponential blow-up for the product automaton by using ATAs. To make this
work, we have to reduce the size of the alphabet for the ATA
$\mathcal{A}^{\prime}$. This can be achieved by encoding a tuple
$(\sigma_{1},\dots,\sigma_{k})\in\Sigma_{\bot}^{k}$ of symbols by a path
$\sigma_{1}(\sigma_{2}(\dots\sigma_{k}(\\#_{m})\dots))$ where $\\#_{m}$ is
used as delimiter symbol of rank $m:=\max\\{\mathrm{rk}(\sigma_{i})\mid 1\leq
i\leq k\\}$. Then the ATA $\mathcal{A}^{\prime}$ can be constructed in
polynomial time. Now it holds that
$a_{0}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ if and only if
$\exists^{\mathrm{ram}}x,y\colon R^{\prime}(x,y)\vee\exists x\colon
R^{\prime}(x,x)$ is valid. By Theorem 2.2 (resp. Theorem 2.4) validity of the
first disjunct of $\varphi$ can be checked in nondeterministic logspace (resp.
exponential time) given $\mathcal{A}^{\prime}$. It is easy to see that
validity of the second disjunct of $\varphi$ can also be checked in
nondeterministic logspace (resp. exponential time) given
$\mathcal{A}^{\prime}$. This yields a $\PSPACE$-algorithm in the word case and
an $\EXP$-algorithm in the tree case. Details are in Appendix D.

For the lower bounds we reduce from the intersection non-emptiness problem of
(tree-)regular languages $L_{1},\dots,L_{k}\subseteq A$, which is known to be
$\PSPACE$-complete over words (Kozen, 1977) and $\EXP$-complete over trees
(Comon et al., 1997, Theorem 11). We define the (tree-)regular relation
$R\subseteq A\times A$ such that $(a,b)\in R$ if and only if $a=c$ or $a=b$
where $c\in A$ is some fixed element. Then $L_{1}\cap\dots\cap
L_{k}\neq\emptyset$ if and only if $c\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$.

For $k=1$, the previous construction yields a reduction from nonemptiness for
D$\uparrow$TAs, which is $\P$-complete, to recurrent reachability over
transitive tree-regular relations given by D$\uparrow$TAs, proving the
$\P$-hardness in Theorem 2.3 and Corollary 2.7.

In (Löding, 2006) Löding shows that the reachability relation $\to^{*}$ for
regular ground tree rewrite systems (RGTRS) is tree-regular and an NTA for
$\to^{*}$ can be constructed in polynomial time. Hence, by Theorem 2.8
recurrent reachability with generalized Büchi condition is $\EXP$-complete for
RGTRSs where hardness for GTRSs can be shown by a similar reduction as above
from intersection nonemptiness.

###### Corollary 6.3.

For an RGTRS and tree-regular languages $L_{1},\dots,L_{k}$ given by NTAs, one
can construct in exponential time an NTA recognizing
$\mathit{Rec}(L_{1},\dots,L_{k})[\to^{*}]$.

###  6.2. Monadic Decomposability

In the following we reduce monadic decomposability to the infinite clique
problem over co-transitive relations, proving Corollary 2.9 and Corollary
2.10. A $k$-ary relation $R$ over words or trees is monadically decomposable
if and only if for all $1\leq j\leq k$ the equivalence relations $\sim_{j}$ on
$(\Sigma^{*})^{k}$ (or $\mathcal{T}_{\Sigma}^{k}$) have finite index, where
two tuples $\bm{u}=(u_{1},\dots,u_{j})$, $\bm{v}=(v_{1},\dots,v_{j})$ are
$\sim_{j}$-equivalent if and only if

$\forall\bm{w}=(w_{j+1},\dots,w_{k})\colon[(\bm{u},\bm{w})\in
R\iff(\bm{v},\bm{w})\in R],$

see for example (Carton et al., 2006, Proof of Proposition 3.9). If the given
automaton $\mathcal{A}$ for $R$ is a DFA, D$\uparrow$TA, or D$\downarrow$TA,
then one can compute automata $\mathcal{A}_{\not\sim_{j}}$ for the complements
$\not\sim_{j}$ of $\sim_{j}$ in logspace, using the fact that
$\bm{u}\not\sim_{j}\bm{v}$ is equivalent to

$\displaystyle\exists\bm{w}\colon$ $\displaystyle\big{(}(\bm{u},\bm{w})\in
R\wedge(\bm{v},\bm{w})\notin R\big{)}~{}\vee\big{(}(\bm{u},\bm{w})\notin
R\wedge(\bm{v},\bm{w})\in R\big{)}.$

If $\mathcal{A}$ is an NFA or NTA, then this is possible in polynomial space,
by determinizing $\mathcal{A}$ and using closure properties of regular
relations. Then, apply Theorem 2.2 (Theorem 2.6) to
$\mathcal{A}_{\not\sim_{j}}$ to check in $\NL$ (resp. $\P$) for an infinite
clique in $\not\sim_{j}$.

The lower bounds are shown in Appendix E by a reduction from the universality
problem for DFAs, NFAs, D$\uparrow$TAs, and NTAs, and the emptiness problem
for D$\downarrow$TAs.

##  7\. Unranked tree-automatic structures

In this section we consider the unranked tree analogue of Theorems 2.4 and
2.5. Furthermore, we consider an application of the results to recurrent
reachability in subtree and flat prefix rewriting systems. Unranked tree-
regular languages and relations are recognized by nondeterministic unranked
tree automata (NUTAs), see Appendix F.

###### Theorem 7.1.

Given an unranked tree-regular $R\subseteq(\mathcal{U}_{\Sigma})^{k+2}$ by an
NUTA $\mathcal{A}$, one can construct an NUTA for the relation
$[\\![\exists^{\mathrm{ram}}x,y\colon R(x,y,\bm{z})]\\!]$ in polynomial time
if $R$ is transitive and in exponential time otherwise. Hence, the infinite
clique problem over (transitive) unranked tree-regular relations is in $\EXP$
($\P$).

The proof can be found in Section F.1. It uses the _first-child next-sibling
encoding_ , a standard regularity-preserving transformation from unranked
trees to binary trees (see e.g., (Neven, 2002; Gottlob et al., 2005; Libkin,
2005)). As over ranked trees, Theorem 7.1 implies:

###### Corollary 7.2.

For a binary unranked tree-regular relation $R$ and an unranked tree-regular
language $L$ given by NUTAs, one can construct an NUTA recognizing
$\mathit{Rec}(L)[R]$ in polynomial time if $R$ is transitive and in
exponential time otherwise.

In (Löding and Spelten, 2007) Löding and Spelten introduce tree rewriting
systems over unranked trees called subtree and flat prefix rewriting systems
(SFPRS). We refer to Section F.2 for the definition. In (Löding and Spelten,
2007) it is shown that the reachability relation $\to^{*}$ for (regular)
SFPRSs is an unranked tree-regular relation. Moreover, it can be observed that
the NUTA for $\to^{*}$ can be constructed in polynomial time. Since $\to^{*}$
is transitive, we can apply Corollary 7.2 to obtain that recurrent
reachability for (regular) SFPRSs is decidable in polynomial time:

###### Corollary 7.3.

For a (regular) SFPRS and an unranked tree-regular language $L$ given as NUTA,
one can construct an NUTA recognizing $\mathit{Rec}(L)[\to^{*}]$ in polynomial
time.

Let $\mathrm{FO}(\mathrm{SFPRS})$ be the first-order theory over unranked
trees with the reachability relation $\to^{*}$ and the one-step reachability
relation $\to$ for (regular) SFPRSs. In (Löding and Spelten, 2007) it is shown
that the structure of $\mathrm{FO}(\mathrm{SFPRS})$ is unranked tree-automatic
which means that $\mathrm{FO}(\mathrm{SFPRS})$ is decidable.

Let $\mathrm{FO}(\mathrm{SFPRS}+\mathrm{Rec})$ be the theory
$\mathrm{FO}(\mathrm{SFPRS})$ enriched by the recurrent reachability operator:
For a formula $\varphi$ in $\mathrm{FO}(\mathrm{SFPRS}+\mathrm{Rec})$ with one
free variable we define the recurrent reachability operator
$\mathit{Rec}(\varphi)$ as formula with one free variable such that
$\mathit{Rec}(\varphi)(t)$ is true if and only if
$t\in\mathit{Rec}(L)[\to^{*}]$ for any $t\in\mathcal{U}_{\Sigma}$ where $L$ is
the unranked tree-regular language defined by $\varphi$.

###### Corollary 7.4.

The theory $\mathrm{FO}(\mathrm{SFPRS}+\mathrm{Rec})$ is decidable.

##  8\. Conclusion and Future Works

We have identified directed Ramsey quantifiers as a fundamental notion that
underlies the standard notion of Ramsey quantifiers, recurrent reachability,
and monadic decomposability. We have also shown that the notion of _comb of
combs_ can be used to obtain substantially simpler proofs in case of word-
automatic relations, and can be generalized to tree-automatic relations,
allowing us to derive new results for Ramsey quantifiers, recurrent
reachability and monadic decomposability (with applications to generalized
Büchi conditions and unranked tree-automatic relations). There are many
natural research directions. In particular, we pinpoint that Ramsey
quantifiers over $\omega$-automatic relations, as well as recurrent
reachability over transitive $\omega$-automatic relations, is still a major
open problem (Kuske, 2010), although monadic decomposability is known to be
decidable (Löding and Spinrath, 2019). One possible approach is to consider
the subclass of $\omega$-automatic relations that are definable over the
theory of mixed integer-real linear arithmetic
$\langle\mathbb{R};\mathbb{Z},1,0,<,+\rangle$, for which the problem of Ramsey
quantifiers and recurrent reachability, to be the best our knowledge, is still
an open problem.

###### Acknowledgements.

Pascal Bergsträßer and Anthony Lin are supported by the Sponsor ERC
https://erc.europa.eu Starting Grant Grant #759969 (AV-SMP).

pages main.pgpages pages0 pages

## References

  * (1)
  * Abdulla et al. (2002) Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d’Orso. 2002.  Regular Tree Model Checking. In _Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings_ _(Lecture Notes in Computer Science, Vol. 2404)_ , Ed Brinksma and Kim Guldstrand Larsen (Eds.). Springer, 555–568.  https://doi.org/10.1007/3-540-45657-0_47
  * Abdulla et al. (2004) Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. 2004.  A Survey of Regular Model Checking. In _CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings_ _(Lecture Notes in Computer Science, Vol. 3170)_ , Philippa Gardner and Nobuko Yoshida (Eds.). Springer, 35–48.  https://doi.org/10.1007/978-3-540-28644-8_3
  * Barceló et al. (2019) Pablo Barceló, Chih-Duo Hong, Xuan Bach Le, Anthony W. Lin, and Reino Niskanen. 2019\.  Monadic Decomposability of Regular Relations. In _46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece_ _(LIPIcs, Vol. 132)_ , Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 103:1–103:14.  https://doi.org/10.4230/LIPIcs.ICALP.2019.103
  * Blumensath and Grädel (2000) Achim Blumensath and Erich Grädel. 2000.  Automatic Structures. In _15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000_. IEEE Computer Society, 51–62.  https://doi.org/10.1109/LICS.2000.855755
  * Blumensath and Grädel (2004) Achim Blumensath and Erich Grädel. 2004.  Finite Presentations of Infinite Structures: Automata and Interpretations.  _Theory Comput. Syst._ 37, 6 (2004), 641–674.  https://doi.org/10.1007/s00224-004-1133-y
  * Carton et al. (2006) Olivier Carton, Christian Choffrut, and Serge Grigorieff. 2006\.  Decision problems among the main subfamilies of rational relations.  _RAIRO Theor. Informatics Appl._ 40, 2 (2006), 255–275.  https://doi.org/10.1051/ita:2006005
  * Comon et al. (1997) Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. 1997.  Tree Automata Techniques and Applications.  (1997).
  * Frühwirth et al. (1991) Thom W. Frühwirth, Ehud Shapiro, Moshe Y. Vardi, and Eyal Yardeni. 1991.  Logic Programs as Types for Logic Programs. In _Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18, 1991_. IEEE Computer Society, 300–309.  https://doi.org/10.1109/LICS.1991.151654
  * Ginsburg and Spanier (1966) Seymour Ginsburg and Edwin H Spanier. 1966.  Bounded regular sets.  _Proc. Amer. Math. Soc._ 17, 5 (1966), 1043–1049.  https://doi.org/10.1090/S0002-9939-1966-0201310-3
  * Gottlob et al. (2005) Georg Gottlob, Christoph Koch, Reinhard Pichler, and Luc Segoufin. 2005.  The complexity of XPath query evaluation and XML typing.  _J. ACM_ 52, 2 (2005), 284–335.  https://doi.org/10.1145/1059513.1059520
  * Grädel (2020) Erich Grädel. 2020\.  Automatic Structures: Twenty Years Later. In _LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020_ , Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 21–34.  https://doi.org/10.1145/3373718.3394734
  * Kozen (1977) Dexter Kozen. 1977\.  Lower Bounds for Natural Proof Systems. In _18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977_. IEEE Computer Society, 254–266.  https://doi.org/10.1109/SFCS.1977.16
  * Kozen (1997) Dexter Kozen. 1997\.  _Automata and computability_.  Springer.
  * Kuske (2010) Dietrich Kuske. 2010\.  Is Ramsey’s Theorem omega-automatic?. In _27th International Symposium on Theoretical Aspects of Computer Science, STACS 2010, March 4-6, 2010, Nancy, France_ _(LIPIcs, Vol. 5)_ , Jean-Yves Marion and Thomas Schwentick (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 537–548.  https://doi.org/10.4230/LIPIcs.STACS.2010.2483
  * Kuske and Lohrey (2010) Dietrich Kuske and Markus Lohrey. 2010.  Some natural decision problems in automatic graphs.  _J. Symb. Log._ 75, 2 (2010), 678–710.  https://doi.org/10.2178/jsl/1268917499
  * Leroux and Sutre (2006) Jérôme Leroux and Grégoire Sutre. 2006.  Flat counter automata almost everywhere!. In _Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006_ _(Dagstuhl Seminar Proceedings, Vol. 06081)_ , Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm (Eds.). Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.  http://drops.dagstuhl.de/opus/volltexte/2006/729
  * Libkin (2003) Leonid Libkin. 2003\.  Variable independence for first-order definable constraints.  _ACM Trans. Comput. Log._ 4, 4 (2003), 431–451.  https://doi.org/10.1145/937555.937557
  * Libkin (2005) Leonid Libkin. 2005\.  Logics for Unranked Trees: An Overview. In _Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings_ _(Lecture Notes in Computer Science, Vol. 3580)_ , Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung (Eds.). Springer, 35–50.  https://doi.org/10.1007/11523468_4
  * Lin (2012) Anthony Widjaja Lin. 2012\.  Accelerating tree-automatic relations. In _IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India_. 313–324.  https://doi.org/10.4230/LIPIcs.FSTTCS.2012.313
  * Lin and Rümmer (2021) Anthony W. Lin and Philipp Rümmer. 2021.  Regular Model Checking Revisited. In _Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday_. 97–114.  https://doi.org/10.1007/978-3-030-91384-7_6
  * Löding (2006) Christof Löding. 2006\.  Reachability Problems on Regular Ground Tree Rewriting Graphs.  _Theory Comput. Syst._ 39, 2 (2006), 347–383.  https://doi.org/10.1007/s00224-004-1170-6
  * Löding and Spelten (2007) Christof Löding and Alex Spelten. 2007.  Transition Graphs of Rewriting Systems over Unranked Trees. In _Mathematical Foundations of Computer Science 2007, 32nd International Symposium, MFCS 2007, Ceský Krumlov, Czech Republic, August 26-31, 2007, Proceedings_ _(Lecture Notes in Computer Science, Vol. 4708)_ , Ludek Kucera and Antonín Kucera (Eds.). Springer, 67–77.  https://doi.org/10.1007/978-3-540-74456-6_8
  * Löding and Spinrath (2019) Christof Löding and Christopher Spinrath. 2019.  Decision Problems for Subclasses of Rational Relations over Finite and Infinite Words.  _Discret. Math. Theor. Comput. Sci._ 21, 3 (2019).  http://dmtcs.episciences.org/5141
  * Muller and Schupp (1995) David E. Muller and Paul E. Schupp. 1995.  Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra.  _Theor. Comput. Sci._ 141, 1&2 (1995), 69–107.  https://doi.org/10.1016/0304-3975(94)00214-4
  * Neven (2002) Frank Neven. 2002\.  Automata, Logic, and XML. In _Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings_ _(Lecture Notes in Computer Science, Vol. 2471)_ , Julian C. Bradfield (Ed.). Springer, 2–26.  https://doi.org/10.1007/3-540-45793-3_2
  * Rubin (2008) Sasha Rubin. 2008\.  Automata Presenting Structures: A Survey of the Finite String Case.  _Bull. Symb. Log._ 14, 2 (2008), 169–209.  https://doi.org/10.2178/bsl/1208442827
  * Seidl (1994) Helmut Seidl. 1994\.  Haskell Overloading is DEXPTIME-Complete.  _Inf. Process. Lett._ 52, 2 (1994), 57–60.  https://doi.org/10.1016/0020-0190(94)00130-8
  * Stearns (1967) Richard Edwin Stearns. 1967\.  A Regularity Test for Pushdown Machines.  _Inf. Control._ 11, 3 (1967), 323–340.  https://doi.org/10.1016/S0019-9958(67)90591-8
  * To and Libkin (2008) Anthony Widjaja To and Leonid Libkin. 2008.  Recurrent Reachability Analysis in Regular Model Checking. In _Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings_. 198–213.  https://doi.org/10.1007/978-3-540-89439-1_15
  * To and Libkin (2010) Anthony Widjaja To and Leonid Libkin. 2010.  Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems. In _Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings_. 221–236.  https://doi.org/10.1007/978-3-642-12032-9_16
  * Valiant (1975) Leslie G. Valiant. 1975\.  Regularity and Related Problems for Deterministic Pushdown Automata.  _J. ACM_ 22, 1 (1975), 1–10.  https://doi.org/10.1145/321864.321865
  * Veanes (1997) Margus Veanes. 1997\.  _On computational complexity of basic decision problems of finite tree automata_.  Technical Report. UPMAIL Technical Report 133, Uppsala University, Computing Science Department.
  * Veanes et al. (2017) Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, and Sergey Bereg. 2017.  Monadic Decomposition.  _J. ACM_ 64, 2 (2017), 14:1–14:28.  https://doi.org/10.1145/3040488

##  Appendix A Directed vs undirected cliques

Theorem 2.2 and Theorem 2.4 also hold if we alternatively define the Ramsey
quantifier $\exists^{\mathrm{ram}}x,y\colon\varphi(x,y,\bm{z})$ using infinite
undirected cliques, i.e., there exists an infinite set $X$ such that
$\varphi(a,b,\bm{z})$ holds for all $a,b\in X$ with $a\neq b$, since we can
replace $\varphi(x,y,\bm{z})$ by
$\varphi(x,y,\bm{z})\wedge\varphi(y,x,\bm{z})$.

Furthermore, the -lower bound in the word case (Corollary 2.9) and the -lower
bound in the tree case (Theorem 2.3) also hold for undirected cliques:

###### Proposition A.1.

The infinite clique problems for directed and undirected cliques are logspace
equivalent over (tree-)regular relations.

###### Proof.

We first reduce the undirected version to the directed version. Let
$R\subseteq A\times A$ be given by an NFA (resp. NTA) $\mathcal{A}$. Then we
define the relation $R^{\prime}:=\\{(a,b)\in A\times A\mid(a,b)\in
R\wedge(b,a)\in R\\}$. Clearly, $R^{\prime}$ is a (tree-)regular relation and
an NFA (resp. NTA) recognizing $R^{\prime}$ can be constructed in logspace
from $\mathcal{A}$. Moreover, we have that $R$ has an infinite undirected
clique if and only if $R^{\prime}$ has an infinite directed clique.

For the reverse reduction, let $R\subseteq A\times A$ be given by an NFA
(resp. NTA) $\mathcal{A}$. We define the relation

$R^{\prime}:=\\{((a,i),(b,j))\in(A\times\mathbb{N})^{2}\mid a\neq b\\\
\wedge((a,b)\in R\wedge i<j\vee(b,a)\in R\wedge j<i)\\}.$

It is easy to see that $R^{\prime}$ can be encoded as a (tree-)regular
relation and an NFA (resp. NTA) recognizing this relation can be constructed
in logspace from $\mathcal{A}$. It holds that $R$ has an infinite directed
clique if and only if $R^{\prime}$ has an infinite undirected clique. Indeed,
if $R$ has an infinite directed clique $(a_{i})_{i\geq 1}$, then we can number
the elements and get an infinite undirected clique $((a_{i},i))_{i\geq 1}$ in
$R^{\prime}$. Conversely, if $R^{\prime}$ has an infinite undirected clique
$((a_{i},n_{i}))_{i\geq 1}$, then $(a_{i_{j}})_{j\geq 1}$ with
$n_{i_{j}}<n_{i_{j^{\prime}}}$ for $j<j^{\prime}$ is an infinite directed
clique in $R$. ∎

##  Appendix B Constructions of Büchi automata

See 4.4

###### Proof.

Given an NFA $\mathcal{A}=(Q,\Sigma_{\bot}^{2},q_{\mathrm{in}},\Delta,F)$, we
add to $\mathcal{A}$ a state $\bot$ and transitions $\bot\xrightarrow{(a,b)}q$
for all $(a,b)\in\Sigma_{\bot}^{2}$ and $q\in Q_{\bot}$.

The Büchi automaton
$\mathcal{B}=(Q_{\bot}^{4},\Sigma_{\bot}^{2},q_{\mathrm{in}}^{\mathcal{B}},\Delta^{\mathcal{B}},Q_{\bot}^{4})$
simulates the runs $\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ from Lemma 4.3 in
the four components. Its initial state is
$q_{\mathrm{in}}^{\mathcal{B}}=(q_{\mathrm{in}},q_{\mathrm{in}},\bot,\bot)$
and it contains the following transtions:

  * •

$(p,s,q,t)\xrightarrow{(a,b)}_{\mathcal{B}}(p^{\prime},s^{\prime},q^{\prime},t^{\prime})$
for all $p\xrightarrow{(b,b)}_{\mathcal{A}}p^{\prime}$,
$s\xrightarrow{(a,b)}_{\mathcal{A}}s^{\prime}$,
$q\xrightarrow{(\bot,b)}_{\mathcal{A}}q^{\prime}$,
$t\xrightarrow{(\bot,a)}_{\mathcal{A}}t^{\prime}$,

  * •

$(p,q,q,t)\xrightarrow{\\#}_{\mathcal{B}}(p,p,q,q)$ for all $p,q\in Q$, $t\in
F$,

  * •

$(p_{1},p_{2},p_{3},p_{4})\xrightarrow{\varepsilon}_{\mathcal{B}}(q_{1},q_{2},q_{3},q_{4})$
whenever $p_{i}=q_{i}$ or $p_{i}\xrightarrow{\varepsilon}_{\mathcal{A}}q_{i}$
for all $i$.

The desired Büchi automaton is a product automaton of $\mathcal{B}$ and a
Büchi automaton which verifies that the input word is a valid comb encoding
$\mathrm{enc}(\bm{\alpha},\bm{\beta})$. ∎

See 5.4

###### Proof.

Let $\mathcal{A}^{\prime}=(Q,\Sigma_{\bot}^{2},\Delta,q_{\mathrm{in}})$ be the
NTA that is obtained by reverting the transitions of the D$\uparrow$TA
$\mathcal{A}$. Clearly, $\mathcal{A}^{\prime}$ has the same runs as
$\mathcal{A}$ on trees. Let $\bm{t}$ be a comb that forms an infinite clique
in $R$. Since any NTA is a special ATA, we can apply Lemma 5.2 on
$\mathcal{A}^{\prime}$ and $\bm{t}$ to get a subcomb $\bm{s}$ of $\bm{t}$
generated by $(\bm{\alpha},\bm{\beta})$, runs $\rho(s_{i},s_{j})$ of
$\mathcal{A}^{\prime}$ on $s_{i}\otimes s_{j}$, and context forests
$\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$ such that

$\rho(s_{i},s_{j})=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,j-1}\nu_{i,j}$

is a decomposition compatible with the
$(\bm{\alpha},\bm{\beta})$-decomposition of $s_{i}\otimes s_{j}$ for all
$i<j$. Moreover, we have that $\mu_{i,j}$ and $\nu_{i,j}$ only depend on $j$
since there are unique runs of $\mathcal{A}$ on
$(\varepsilon\otimes\beta_{j})(\varepsilon\otimes\alpha_{j+1})$ and
$\varepsilon\otimes\alpha_{j}$. Thus, we can just write $\mu_{j}$ and
$\nu_{j}$ for all $j>1$.

We now construct an NBTA $\mathcal{B}$ over the alphabet $\Omega$ which
accepts precisely all comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ of
a generator $(\bm{\alpha},\bm{\beta})$ with the above properties. Since the
set of all comb encodings is regular, we can assume that the input tree is
already a valid comb encoding. A state in $\mathcal{B}$ consists of four
components in which $\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ are simulated. To
handle the special case where only $\kappa_{0}$, $\lambda_{0}$ are simulated,
we add a state $\bot$ to $\mathcal{A}^{\prime}$ with transitions
$\bot\xrightarrow{(a,b)}\bm{q}$ for all symbols $(a,b)\in\Sigma_{\bot}^{2}$ of
rank $r$, and $\bm{q}\in Q_{\bot}^{r}$. The NBTA $\mathcal{B}$ has the state
set $Q_{\bot}^{4}$, initial state
$(q_{\mathrm{in}},q_{\mathrm{in}},\bot,\bot)$, and the transitions

  * •

$(p,s,q,t)\xrightarrow{(a,b)}\bm{p}\otimes\bm{s}\otimes\bm{q}\otimes\bm{t}$ if
$\mathcal{A}^{\prime}$ contains the transitions $p\xrightarrow{(b,b)}\bm{p}$,
$s\xrightarrow{(a,b)}\bm{s}$, $q\xrightarrow{(\bot,b)}\bm{q}$,
$t\xrightarrow{(\bot,a)}\bm{t}$,

  * •

$(p,q,q,\bot)\xrightarrow{\\#}(p,p,q,q)$ for all $p,q\in Q$.

Correctness follows from the previous observations. ∎

See 2.4

###### Proof.

First observe that from the ABTA $\mathcal{B}$ in Proposition 5.3 we can
construct in exponential time an NTA $\mathcal{C}$ over $\Sigma$ which accepts
$t_{1}\in\mathcal{T}_{\Sigma}$ if and only if the encoding of some comb
$(t_{i})_{i\geq 1}$ is accepted by $\mathcal{B}$. Indeed, we first transform
$\mathcal{B}$ into an NBTA
$\mathcal{D}=(Q_{\mathcal{D}},\Omega,\Delta_{D},q_{0}^{\mathcal{D}},F_{\mathcal{D}})$
which can be done in exponential time (Muller and Schupp, 1995, Theorem 1.2).
From $\mathcal{D}$ we construct
$\mathcal{C}=(Q_{\mathcal{D}},\Sigma,\Delta_{\mathcal{C}},q_{0}^{\mathcal{D}})$
such that for all $q\in Q_{\mathcal{D}}$, $a\in\Sigma$, and $p_{i}\in
Q_{\mathcal{D}}$ for $1\leq i\leq\mathrm{rk}(a)$ we let
$(q,a,(p_{i})_{i\leq\mathrm{rk}(a)})\in\Delta_{\mathcal{C}}$ if and only if
there exist $b\in\Sigma_{\bot}$ and $p_{i}\in Q_{\mathcal{D}}$ for
$\mathrm{rk}(a)<i\leq\mathrm{rk}\begin{pmatrix}a\\\ b\end{pmatrix}$ such that

$(q,\begin{pmatrix}a\\\
b\end{pmatrix},(p_{i})_{i\leq\mathrm{rk}\begin{pmatrix}a\\\
b\end{pmatrix}})\in\Delta_{\mathcal{D}}$

and $\mathcal{D}$ accepts some tree from state $p_{i}$ for all
$i>\mathrm{rk}(a)$. Note that $\mathcal{C}$ can be constructed in polynomial
time given $\mathcal{D}$ since we need to perform a polynomial number of non-
emptiness checks on $\mathcal{D}$, each of which takes quadratic time. The NTA
$\mathcal{C}$ satisfies that (i) for every infinite clique $\bm{t}$ of $R$
some element $t_{i}$ is accepted by $\mathcal{C}$ and (ii) if $t$ is accepted
by $\mathcal{C}$, then $t$ belongs to an infinite clique of $R$.

Given an NTA $\mathcal{A}$ for $R\subseteq(\mathcal{T}_{\Sigma})^{k+2}$. We
first construct an NTA $\mathcal{A}^{\prime}$ over $\Sigma_{\bot}^{2k+2}$
accepting the binary relation

$R^{\prime}=\\{(s\otimes c_{1}\otimes\dots\otimes c_{k},t\otimes
c_{1}\otimes\dots\otimes c_{k})\mid(s,t,\bm{c})\in R\\}.$

Let $\mathcal{C}^{\prime}$ be the NTA described above that accepts at least
one tree from each infinite $R^{\prime}$-clique and only accepts elements of
infinite $R^{\prime}$-cliques. Projecting away the first component yields the
desired NTA for
$\\{\bm{c}\in(\mathcal{T}_{\Sigma})^{k}\mid\exists^{\mathrm{ram}}x,y\colon
R(x,y,\bm{c})\\}$.

If $R$ is given as D$\uparrow$TA, then one can construct an NBTA in polynomial
time instead of an ABTA using Proposition 5.4. Then $\mathcal{C}^{\prime}$ can
be constructed in polynomial time. ∎

See 5.5

###### Proof.

We view the NTA $\mathcal{A}$ for $R$ as an ATA and construct the ABTA
$\mathcal{B}$ as in the proof of Proposition 5.3 which accepts precisely all
comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ with the properties from
Lemma 5.2. Then, we omit all states in mode 3. More formally, let
$\mathcal{C}=(Q_{\mathcal{C}},\Omega,\delta_{\mathcal{C}},q_{0}^{\mathcal{C}},Q_{\mathcal{C}})$
be the ABTA with state set
$Q_{\mathcal{C}}=\\{q_{0}^{\mathcal{C}}\\}\cup(Q\times\\{1,2,4\\})$, and the
same transitions as $\mathcal{B}$ except for
$\delta_{\mathcal{C}}((q,2),\\#):=((q,4),1)$ for all $q\in Q$. Clearly, all
comb encodings with the properties from Lemma 5.2 are still accepted by
$\mathcal{C}$. Conversely, if the encoding
$\mathrm{enc}(\bm{\alpha},\bm{\beta})$ of a comb $\bm{t}$ is accepted by
$\mathcal{C}$ then for all $i\geq 1$, $\mathcal{C}$ simulates a run of
$\mathcal{A}$ on $t_{i}\otimes t_{i+1}$ as argued in Proposition 5.3. By
transitivity we obtain $(t_{i},t_{j})\in R$ for all $i<j$.

It remains to convert $\mathcal{C}$ into an NBTA of polynomial size. Observe
that $\mathcal{C}$ only universally branches in the root and at $\\#$-nodes
into a state of mode 1 and 2. Furthermore, states of mode 2 transition to mode
4 when reading $\\#$. Hence, any run contains for each node $v$ of the input
tree at most three run nodes referring to $v$. Thus, we apply a standard
powerset construction to convert $\mathcal{C}$ into an equivalent NBTA
$\mathcal{D}$, where we restrict to subsets of $Q_{\mathcal{C}}$ of size at
most three. We make all states in $\mathcal{D}$ final, since $\mathcal{C}$
accepts any tree with a run. Finally, we take the product construction of
$\mathcal{D}$ with an NBTA for $\mathrm{Enc}_{\Sigma}$, to obtain the desired
NBTA in polynomial time. ∎

See 2.6

###### Proof.

Given an NTA $\mathcal{A}=(Q,\Sigma_{\bot}^{2},\Delta,q_{\mathrm{in}})$ for a
co-transitive relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$. We can prove a
statement similar to Lemma 4.3 for tree combs which are generated by a monadic
generator.

Suppose that $R$ has an infinite clique. By Lemma 5.7 and Lemma 5.2 there
exist an infinite clique $\bm{t}$ in $R$ with a monadic generator
$(\bm{\alpha},\bm{\beta})$, and context forests
$\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$ for $i<j$ such that
$\rho_{i,j}=\kappa_{1}\dots\kappa_{i-1}\lambda_{i}\mu_{i,i+1}\dots\mu_{i,j-1}\nu_{i,j}$
is a decomposition compatible with the
$(\bm{\alpha},\bm{\beta})$-decomposition of $t_{i}\otimes t_{j}$. In
particular, all context forests $\kappa_{i},\lambda_{i},\mu_{i,j}$ have
exactly one hole, and hence $\kappa_{i},\lambda_{i},\mu_{i,j},\nu_{i,j}$ are
in fact contexts.

Moreover, we can ensure that $\mu_{i,j}=\mu_{i^{\prime},j}$ and
$\nu_{i,j}=\nu_{i^{\prime},j}$ for all $i<i^{\prime}<j$ and can therefore just
write $\mu_{j}$ and $\nu_{j}$ for all $j>1$, respectively. For the proof we
can reason similarly as in Lemma 4.3 by applying Ramsey’s theorem to ensure
that all contexts $\mu_{i,j}$ carry the same state in the root. This allows us
to verify the runs using a polynomially sized NBTA on the comb encoding.

Finally, we can construct in polynomial time a Büchi tree automaton
$\mathcal{B}$ over the alphabet $\Omega=\Sigma_{\bot}^{2}\cup\\{\\#\\}$ which
accepts all comb encodings $\mathrm{enc}(\bm{\alpha},\bm{\beta})$ of a monadic
generator $(\bm{\alpha},\bm{\beta})$ for which runs of the form
$\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ as above exist. Since the set of all
monadic comb encodings is regular, we can assume that the input tree is
already a valid monadic comb encoding. A state in $\mathcal{B}$ consists of
four components in which the runs $\kappa_{j},\lambda_{j},\mu_{j},\nu_{j}$ are
simulated. To handle the special case where only $\kappa_{0}$, $\lambda_{0}$
are simulated, we add a state $\bot$ to $\mathcal{A}$ with transitions
$\bot\xrightarrow{(a,b)}\bm{q}$ for all symbols $(a,b)\in\Sigma_{\bot}^{2}$ of
rank $r$, and $\bm{q}\in Q_{\bot}^{r}$. The Büchi tree automaton $\mathcal{B}$
has the state set $Q_{\bot}^{4}$, initial state
$(q_{\mathrm{in}},q_{\mathrm{in}},\bot,\bot)$, and the transitions

  * •

$(p,s,q,t)\xrightarrow{(a,b)}\bm{p}\otimes\bm{s}\otimes\bm{q}\otimes\bm{t}$ if
$\mathcal{A}$ contains the transitions $p\xrightarrow{(b,b)}\bm{p}$,
$s\xrightarrow{(a,b)}\bm{s}$, $q\xrightarrow{(\bot,b)}\bm{q}$,
$t\xrightarrow{(\bot,a)}\bm{t}$,

  * •

$(p,q,q,\bot)\xrightarrow{\\#}(p,p,q,q)$ for all $p,q\in Q$.

Correctness follows from the previous observations. ∎

##  Appendix C Proof of Proposition 6.1

###### Lemma C.1.

The infinite clique problem is logspace reducible to recurrent reachability
over (tree-)regular relations.

###### Proof.

The word case is easy. Let $R\subseteq\Sigma^{*}\times\Sigma^{*}$ be given by
an NFA $\mathcal{A}$. We have that $R$ has an infinite clique if and only if
there exists a sequence $(w_{i})_{i\geq 1}$ of words such that
$(w_{i},w_{j})\in R$ and $|w_{i}|<|w_{j}|$ for all $1\leq i<j$. We define the
relation $R^{\prime}\subseteq\Sigma^{*}\times\Sigma^{*}$ such that

  * •

$(\varepsilon,w)\in R^{\prime}$ for all $w\in\Sigma^{+}$ and

  * •

$(v,w)\in R^{\prime}$ iff $(v,w)\in R$ and $|v|<|w|$ for all
$v,w\in\Sigma^{+}$.

Clearly, the relation $R^{\prime}$ is regular and an NFA that accepts
$R^{\prime}$ is implicitly logspace computable. Since a path in $R^{\prime}$
cannot visit a word more than once, it holds that $R$ has an infinite clique
if and only if $\varepsilon\in\mathit{Rec}(\Sigma^{*})[R^{\prime}]$.

In the tree case we use a similar idea as in the word case for one path of the
trees. Let $R\subseteq T_{\Sigma}\times T_{\Sigma}$ be given by an NTA
$\mathcal{A}$. We have that $R$ has an infinite clique if and only if there
exists a sequence $(t_{i})_{i\geq 1}$ of trees such that $(t_{i},t_{j})\in R$
for all $1\leq i<j$ and the domain of one path strictly grows indefinitely in
the sequence. Such a sequence exists since the union of the domains of all
$t_{i}$ is an infinite ranked tree domain which by König’s lemma has an
infinite path. Let $t_{0}\colon\\{\varepsilon\\}\to\Sigma$ with
$t_{0}(\varepsilon):=a$ for some $a\in\Sigma$. We define the relation
$R^{\prime}\subseteq T_{\Sigma^{\prime}}\times T_{\Sigma^{\prime}}$ with
$\Sigma^{\prime}=\Sigma\cup\\{a^{\prime}\mid a\in\Sigma\\}$ such that for all
$s,t\in T_{\Sigma^{\prime}}\setminus\\{t_{0}\\}$ we have

  * •

$(t_{0},t)\in R^{\prime}$ and

  * •

$(s,t)\in R^{\prime}$ iff the non-primed versions of $s$ and $t$ are in
relation in $R$ and there exists exactly one path $p$ from the root to a leaf
in $s$ labeled with primed symbols, exactly one path $q$ from the root to a
leaf in $t$ labeled with primed symbols, and the domain of $p$ is a strict
subpath of the domain of $q$.

The relation $R^{\prime}$ is tree-regular and an NTA for $R^{\prime}$ is
implicitly logspace computable. Indeed, the NTA for $R^{\prime}$
nondeterministically guesses the path of primed labels in the convolution and
verifies that all other paths have non-primed labels. Moreover, it can check
if the path in $s$ is padded and therefore a strict subpath of the path in
$t$. Finally, it can simulate the automaton $\mathcal{A}$ for $R$ on the non-
primed versions of $s$ and $t$ by just treating a symbol $a^{\prime}$ as $a$.

We claim that $R$ has an infinite clique if and only if
$t_{0}\in\mathit{Rec}(T_{\Sigma^{\prime}})[R^{\prime}]$. We already argued the
“only if” direction. For the “if” direction note that the path property
prevents the witnessing sequence from visiting the non-primed version of a
tree more than once. ∎

###### Lemma C.2.

Recurrent reachability is logspace reducible to the infinite clique problem
over (tree-)regular relations.

###### Proof.

We use the same idea for both the word and tree case. Let $R\subseteq A\times
A$ be a (tree-)regular relation given by an NFA (resp. NTA) $\mathcal{A}$ and
$L\subseteq A$ be a (tree-)regular language given by an NFA (resp. NTA)
$\mathcal{B}$. Furthermore, let $a_{0}\in A$ be the initial word (resp. tree).
We define the relation
$R^{\prime}\subseteq(A\times\mathbb{N})\times(A\times\mathbb{N})$ such that
$((a,m),(b,n))\in R^{\prime}$ if and only if

  * •

$(a_{0},a)\in R$,

  * •

$(a,b)\in R$, and

  * •

$a\in L$.

Intuitively, we create infinitely many copies of every word (resp. tree) by
taking the direct product with the integers. This allows the witnessing
sequence of the infinite clique to visit a word (resp. tree) several times.
Furthermore, in $R^{\prime}$ we only consider the words (resp. trees) that are
in relation with $a_{0}$ to ensure that $a_{0}$ fulfills the conditions of the
initial word (resp. tree). With the third condition we ensure that every word
(resp. tree) of the infinite clique is contained in $L$. Thus,
$a_{0}\in\mathit{Rec}(L)[R]$ if and only if $R^{\prime}$ has an infinite
clique.

Note that $R^{\prime}$ is (tree-)regular and an NFA (resp. NTA) for it is
implicitly logspace computable. To this end, we represent the integers in
unary as words (resp. paths) and take the convolution with the corresponding
word (resp. tree). The first condition can be checked by hardwiring $a_{0}$
into the automaton. The second and third conditions can be ensured by
simulating $\mathcal{A}$ and $\mathcal{B}$, respectively.

Note that if $R$ is transitive, then so is $R^{\prime}$. Moreover, if
$\mathcal{A}$ and $\mathcal{B}$ are deterministic, then so is the automaton
for $R^{\prime}$. ∎

##  Appendix D Recurrent reachability with generalized Büchi condition

###### Proposition D.1.

Recurrent reachability with generalized Büchi condition is decidable in
polynomial space over words.

###### Proof.

We give a $\PSPACE$-reduction from the generalized version to the classical
version. Let the relation $R\subseteq\Sigma^{*}\times\Sigma^{*}$ be given by
an NFA $\mathcal{A}$, the languages $L_{1},\dots,L_{k}\subseteq\Sigma^{*}$ be
given by NFAs $\mathcal{A}_{1},\dots,\mathcal{A}_{k}$, and
$s_{0}\in\Sigma^{*}$ be the initial word. First observe that
$s_{0}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ if and only if there is a
sequence of words $(s_{i})_{i\geq 1}$ such that $(s_{i},s_{j})\in R$ for all
$0\leq i<j$ and $s_{i}\in L_{((i-1)\text{ mod }k)+1}$ for all $i\geq 1$. We
define the relation

$R_{i}:=\\{(w_{1},\dots,w_{2k})\in(\Sigma^{*})^{2k}\mid w_{i}\in L_{i}\\}$

for all $i\in[1,k]$. Moreover, for all $1\leq i<j\leq 2k$ let

$R_{i,j}:=\\{(w_{1},\dots,w_{2k})\in(\Sigma^{*})^{2k}\mid(w_{i},w_{j})\in
R\\}.$

Finally, we define the relation

$R_{s_{0},i}:=\\{(w_{1},\dots,w_{2k})\in(\Sigma^{*})^{2k}\mid(s_{0},w_{i})\in
R\\}$

for all $i\in[1,k]$. Then $s_{0}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ if and
only if

$\varphi:=\exists^{\mathrm{ram}}x,y\colon R^{\prime}(x,y)\vee\exists x\colon
R^{\prime}(x,x)$

is valid where

$R^{\prime}:=\bigcap_{i=1}^{k}R_{i}\cap\bigcap_{1\leq i<j\leq
2k}R_{i,j}\cap\bigcap_{i=1}^{k}R_{s_{0},i}\subseteq(\Sigma^{*})^{k}\times(\Sigma^{*})^{k}.$

Note that the NFAs for $R_{i}$, $R_{i,j}$, and $R_{s_{0},i}$ can be easily
constructed in polynomial time. Hence, the product automaton
$\mathcal{A}^{\prime}$ that recognizes $R^{\prime}$ can be constructed in
$\PSPACE$. By Theorem 2.2 validity of the first disjunct of $\varphi$ can be
checked in nondeterministic logspace given $\mathcal{A}^{\prime}$. It is easy
to see that validity of the second disjunct of $\varphi$ can also be checked
in nondeterministic logspace given $\mathcal{A}^{\prime}$. This yields a
$\PSPACE$-algorithm in total. ∎

###### Proposition D.2.

Recurrent reachability with generalized Büchi condition is decidable in
exponential time over trees.

###### Proof.

We proceed similarly to the word case but we use ATAs to avoid the exponential
blow-up for the product automaton. Let the relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ be given by an ATA
$\mathcal{A}=(Q,\Sigma_{\bot}^{2},\delta,q_{0})$, the languages
$L_{1},\dots,L_{k}\subseteq\mathcal{T}_{\Sigma}$ be given by ATAs
$\mathcal{A}_{i}=(Q_{i},\Sigma,\delta_{i},q_{0}^{i})$ for all $i\in[1,k]$, and
$s_{0}\in\mathcal{T}_{\Sigma}$ be the initial tree. Note that we may assume
that the relation and the languages are given by alternating automata since an
NTA can be easily converted into an ATA in polynomial time. Let
$r:=\max\\{\mathrm{rk}(a)\mid a\in\Sigma\\}$ and
$\Omega:=\Sigma_{\bot}\cup\\{\\#_{i}\mid 0\leq i\leq r\\}$ be a new ranked
alphabet with $\mathrm{rk}(a):=1$ for all $a\in\Sigma_{\bot}$ and
$\mathrm{rk}(\\#_{i}):=i$ for all $i\in[1,r]$. For trees
$t_{1},\dots,t_{n}\in\mathcal{T}_{\Sigma}$ we define
$p(t_{1},\dots,t_{n})\in\mathcal{T}_{\Omega}$ to be the tree
$t_{1}\otimes\dots\otimes t_{n}$ where each node labeled with
$(a_{1},\dots,a_{n})\in\Sigma_{\bot}^{n}$ is replaced by a path
$a_{1}(a_{2}(\dots a_{n}(\\#_{m})\dots))$ where
$m:=\max\\{\mathrm{rk}(a_{i})\mid 1\leq i\leq n\\}$.

Let

$R_{p}:=\\{(s,t)\in\mathcal{T}_{\Omega}^{2}\mid s=p(t_{1},\dots,t_{k})\wedge
t=p(t_{k+1},\dots,t_{2k})\\}$

be the binary relation that checks if the trees are images under $p$. Note
that an ATA for $R_{p}$ can easily be constructed. We define ATAs recognizing
relations $R_{i}$ for all $i\in[1,k]$ and $R_{i,j}$ for all $1\leq i<j\leq 2k$
with a similar meaning as in the word case. We start with the construction of
the ATA

$\mathcal{B}_{i}=(Q_{i}^{\mathcal{B}},\Omega^{2},\delta_{i}^{\mathcal{B}},(q_{0},0))$

for $R_{i}$. Intuitively, $\mathcal{B}_{i}$ checks if in
$p(t_{1},\dots,t_{k})\otimes p(t_{k+1},\dots,t_{2k})$ we have that $t_{i}\in
L_{i}$ for all $i\in[1,k]$. The set of states of $\mathcal{B}_{i}$ is defined
as

$Q_{i}^{\mathcal{B}}:=Q_{i}\times\\{0,\dots,i-1\\}\cup
Q_{i}\times\Sigma\times\\{i,\dots,k\\}.$

For all $q\in Q_{i}$, $j\in[0,k]$, $a,b\in\Sigma_{\bot}$, and $c\in\Sigma$ we
let

$\displaystyle\delta_{i}^{\mathcal{B}}((q,j),\begin{pmatrix}a\\\
b\end{pmatrix})$ $\displaystyle:=((q,j+1),1),\text{ if }j\leq i-2$
$\displaystyle\delta_{i}^{\mathcal{B}}((q,i-1),\begin{pmatrix}c\\\
b\end{pmatrix})$ $\displaystyle:=((q,c,i),1)$
$\displaystyle\delta_{i}^{\mathcal{B}}((q,c,j),\begin{pmatrix}a\\\
b\end{pmatrix})$ $\displaystyle:=((q,c,j+1),1),\text{ if }i\leq j<k$

and for all $r_{1},r_{2}\in[0,r]$ with
$\mathrm{rk}(c)\leq\max\\{r_{1},r_{2}\\}$ let

$\delta_{i}^{\mathcal{B}}((q,c,k),\begin{pmatrix}\\#_{r_{1}}\\\
\\#_{r_{2}}\end{pmatrix}):=\delta^{\prime}_{i}(q,c)$

where $\delta^{\prime}_{i}(q,c)$ is the formula $\delta_{i}(q,c)$ in which
each variable $(p,\ell)$ is replaced by $((p,0),\ell)$.

We now construct the ATA

$\mathcal{A}_{k_{1},k_{2}}=(Q_{k_{1},k_{2}},\Omega^{2},\delta_{k_{1},k_{2}},(q_{0},0))$

for $R_{k_{1},k_{2}}$. Intuitively, $\mathcal{A}_{k_{1},k_{2}}$ checks if
$(t_{k_{1}},t_{k_{2}})\in R$ holds in $p(t_{1},\dots,t_{k})\otimes
p(t_{k+1},\dots,t_{2k})$. We only show the construction for the case $1\leq
k_{1}\leq k<k_{2}\leq 2k$ and $k_{1}<k_{2}-k$ and note that the other cases
work analogously. The set of states of $\mathcal{A}_{k_{1},k_{2}}$ is defined
as

$\displaystyle Q_{k_{1},k_{2}}:=\ $ $\displaystyle
Q\times\\{0,\dots,k_{1}-1\\}\ \cup$ $\displaystyle
Q\times\Sigma_{\bot}\times\\{k_{1},\dots,k_{2}-k-1\\}\ \cup$ $\displaystyle
Q\times\Sigma_{\bot}^{2}\times\\{k_{2}-k,\dots,k\\}.$

We now define the transition function. For all $q\in Q$, $j\in[0,k]$, and
$a,b,c,d\in\Sigma_{\bot}$ we let

$\delta_{k_{1},k_{2}}((q,j),\begin{pmatrix}a\\\ b\end{pmatrix}):=((q,j+1),1)$

if $j\leq k_{1}-2$,

$\displaystyle\delta_{k_{1},k_{2}}((q,k_{1}-1),\begin{pmatrix}a\\\
b\end{pmatrix})$ $\displaystyle:=((q,a,k_{1}),1)$
$\displaystyle\delta_{k_{1},k_{2}}((q,c,j),\begin{pmatrix}a\\\
b\end{pmatrix})$ $\displaystyle:=((q,c,j+1),1)$

if $k_{1}\leq j\leq k_{2}-k-2$,

$\displaystyle\delta_{k_{1},k_{2}}((q,c,k_{2}-k-1),\begin{pmatrix}a\\\
b\end{pmatrix})$ $\displaystyle:=((q,\begin{pmatrix}c\\\
b\end{pmatrix},k_{2}-k),1)$
$\displaystyle\delta_{k_{1},k_{2}}((q,\begin{pmatrix}c\\\
d\end{pmatrix},j),\begin{pmatrix}a\\\ b\end{pmatrix})$
$\displaystyle:=((q,\begin{pmatrix}c\\\ d\end{pmatrix},j+1),1)$

if $k_{2}-k\leq j\leq k-1$, and for all $r_{1},r_{2}\in[0,r]$ with
$\mathrm{rk}(c),\mathrm{rk}(d)\leq\max\\{r_{1},r_{2}\\}$ let

$\delta_{k_{1},k_{2}}((q,\begin{pmatrix}c\\\
d\end{pmatrix},k),\begin{pmatrix}\\#_{r_{1}}\\\
\\#_{r_{2}}\end{pmatrix}):=\delta^{\prime}(q,\begin{pmatrix}c\\\
d\end{pmatrix})$

where $\delta^{\prime}(q,\begin{pmatrix}c\\\ d\end{pmatrix})$ is the formula
$\delta(q,\begin{pmatrix}c\\\ d\end{pmatrix})$ in which each variable
$(p,\ell)$ is replaced by $((p,0),\ell)$.

The ATA for the relation $R_{s_{0},i}$ with $i\in[1,k]$ that checks if in
$p(t_{1},\dots,t_{k})\otimes p(t_{k+1},\dots,t_{2k})$ we have that
$(s_{0},t_{i})\in R$ can be constructed similarly to $\mathcal{A}_{i,j}$. Note
that all the constructions above can be done in polynomial time.

It now holds that $s_{0}\in\mathit{Rec}(L_{1},\dots,L_{k})[R]$ if and only if
$\varphi:=\exists^{\mathrm{ram}}x,y\colon R^{\prime}(x,y)\vee\exists x\colon
R^{\prime}(x,x)$ is valid where

$R^{\prime}:=R_{p}\cap\bigcap_{i=1}^{k}R_{i}\cap\bigcap_{1\leq i<j\leq
2k}R_{i,j}\cap\bigcap_{i=1}^{k}R_{s_{0},i}.$

Since an ATA for the intersection of two ATAs can be constructed in linear
time, we can construct an ATA $\mathcal{A}^{\prime}$ for $R^{\prime}$ in time
polynomial in the size of the ATAs
$\mathcal{A},\mathcal{A}_{1},\dots,\mathcal{A}_{k}$ and $s_{0}$. By Theorem
2.4 validity of the first disjunct of $\varphi$ can be checked in time
exponential in the size of $\mathcal{A}^{\prime}$. It is easy to see that
validity of the second disjunct of $\varphi$ can also be checked in time
exponential in $\mathcal{A}^{\prime}$. This yields an exponential time
algorithm in total. ∎

##  Appendix E Lower bounds for monadic decomposability

###### Lemma E.1.

Given a binary regular relation $R\subseteq\Sigma^{*}\times\Sigma^{*}$ by an
NFA (resp. DFA), it is $\PSPACE$-hard (resp. $\NL$-hard) to decide whether $R$
is monadically decomposable. Given a binary tree-regular relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ by an NTA (resp.
D$\uparrow$TA), it is $\EXP$-hard (resp. $\P$-hard) to decide whether $R$ is
monadically decomposable.

###### Proof.

We give a logspace reduction from the universality problem which is known to
be $\PSPACE$-complete for NFAs, $\NL$-complete for DFAs, $\P$-complete for
D$\uparrow$TAs, and $\EXP$-complete for NTAs. In the following we only
consider the word case. Recall that the universality problem asks whether for
a given regular language $L\subseteq\Sigma^{*}$ it holds that $L=\Sigma^{*}$.
Let $L\subseteq\Sigma^{*}$ be a regular language given by an NFA (resp. DFA)
$\mathcal{A}$. We define the regular relation

$R_{L}:=\\{(u\otimes v,w)\mid u\in L\text{ or }v=w\in\Sigma^{*}\\}.$

It is easy to construct an NFA (resp. DFA) that recognizes $R_{L}$ in
logarithmic space from $\mathcal{A}$. Note that for DFAs the disjunction can
be realized with a product construction. It remains to show that $R_{L}$ is
monadically decomposable if and only if $L=\Sigma^{*}$.

If $L=\Sigma^{*}$, it holds that $R_{L}=\\{(u\otimes v,w)\mid
u,v,w\in\Sigma^{*}\\}$ which is clearly monadically decomposable.

For the converse assume that there exists $u_{0}\in\Sigma^{*}\setminus L$.
Then the intersection of $R_{L}$ with the monadically decomposable relation
$\\{(u_{0}\otimes v,w)\mid v,w\in\Sigma^{*}\\}$ is the relation
$\\{(u_{0}\otimes v,w)\mid v=w\in\Sigma^{*}\\}$, which is not monadically
decomposable. Since monadically decomposable relations are closed under
intersection, it follows that $R_{L}$ is not monadically decomposable. ∎

###### Lemma E.2.

Given a binary tree-regular relation
$R\subseteq\mathcal{T}_{\Sigma}\times\mathcal{T}_{\Sigma}$ by a
D$\downarrow$TA, it is $\P$-hard to decide whether $R$ is monadically
decomposable.

###### Proof.

We give a logspace reduction from the emptiness problem for D$\downarrow$TAs
which is known to be $\P$-complete (Veanes, 1997). Let
$\mathcal{A}=(Q,\Sigma,\Delta,q_{0})$ be a D$\downarrow$TA. We construct a
D$\downarrow$TA
$\mathcal{A}^{\prime}=(Q,\Gamma_{\bot}^{2},\Delta^{\prime},q_{0})$ recognizing
a binary tree-regular relation $R^{\prime}$ over $\Gamma:=\Sigma\cup\\{\\#\\}$
where $\\#\notin\Sigma$ is a symbol of rank 1 as follows. We define the
transition relation $\Delta^{\prime}$ such that

  * •

$q\xrightarrow{(a,a)}_{\mathcal{A}^{\prime}}(q_{1},\dots,q_{r})$ for all
$q\xrightarrow{a}_{\mathcal{A}}(q_{1},\dots,q_{r})$,

  * •

$q_{0}\xrightarrow{(\\#,\\#)}_{\mathcal{A}^{\prime}}q_{0}$

Clearly, $\mathcal{A}^{\prime}$ can be constructed in logspace from
$\mathcal{A}$.

It is easy to see that $R^{\prime}\subseteq\\{(t,t)\mid
t\in\mathcal{T}_{\Gamma}\\}$. Moreover, it holds that $R^{\prime}$ is finite
if and only if $L(\mathcal{A})=\emptyset$. Indeed, if there exists $t\in
L(\mathcal{A})$, then $(t_{n},t_{n})\in R^{\prime}$ for all $n\geq 0$ where
$t_{n}$ is the resulting tree when padding a chain of $\\#$-symbols of length
$n$ to the root of $t$. Since every finite relation is recognizable and every
infinite subrelation of $\\{(t,t)\mid t\in\mathcal{T}_{\Gamma}\\}$ is clearly
not recognizable, it holds that $R^{\prime}$ is recognizable if and only if
$L(\mathcal{A})=\emptyset$. ∎

##  Appendix F Proofs of Section 7

A _nondeterministic unranked tree automaton_ (NUTA) over the unranked alphabet
$\Sigma$ is a tuple $\mathcal{A}=(Q,\Sigma,\Delta,q_{0})$ where $Q$ and
$q_{0}$ are as in the definition of an NTA and $\Delta\subseteq
Q\times\Sigma\times\mathit{REG}(Q)$ is a finite set of transitions. Here,
$\mathit{REG}(Q)$ denotes the set of regular word languages over $Q$ and we
assume that the regular language for each transition is given by an NFA. A
_run_ of $\mathcal{A}$ on an unranked tree $t\in\mathcal{U}_{\Sigma}$ is an
unranked tree $\rho\in\mathcal{U}_{Q}$ with
$\mathrm{dom}(\rho)=\mathrm{dom}(t)$ such that $\rho(\varepsilon)=q_{0}$ and
for each inner node $u\in\mathrm{dom}(\rho)$ with children
$u1,\dots,ur\in\mathrm{dom}(\rho)$ there is a transition
$(\rho(u),t(u),L)\in\Delta$ such that $\rho(u1)\cdots\rho(ur)\in L$. A run
$\rho$ is _accepting_ if for each leaf $u\in\mathrm{dom}(\rho)$ there is a
transition $(\rho(u),t(u),L)\in\Delta$ such that $\varepsilon\in L$. We define
_unranked tree-regular relations_ in the same way as in the ranked case by
using NUTAs instead of NTAs.

###  F.1. Proof of Theorem 7.1

###### Definition F.1.

For an unranked tree $t\in\mathcal{U}_{\Sigma}$ we define the _first-child
next-sibling encoding_ $\mathrm{fcns}:\mathbb{N}^{*}\to\\{1,2\\}^{*}$ such
that $\mathrm{fcns}(\varepsilon)=\varepsilon$ and for all $u\in\mathbb{N}^{*}$
we have $\mathrm{fcns}(u1)=\mathrm{fcns}(u)1$ and
$\mathrm{fcns}(u(i+1))=\mathrm{fcns}(ui)2$ for all $i\geq 1$. We let
$\mathrm{fcns}(\mathrm{dom}(t)):=\bigcup_{u\in\mathrm{dom}(t)}\\{\mathrm{fcns}(u),\mathrm{fcns}(u)1,\mathrm{fcns}(u)2\\}$.