# On the Width of Regular Classes of Finite Structures111A preliminary version
of this work was published in the proceedings of the 27th International
Conference on Automated Deduction [1]

Alexsander Andrade de Melo1 Mateus de Oliveira Oliveira2

1Federal University of Rio de Janeiro, Rio de Janeiro, Brazil
<EMAIL_ADDRESS>
2University of Bergen, Bergen, Norway
<EMAIL_ADDRESS>
###### Abstract

In this work, we introduce the notion of decisional width of a finite
relational structure and the notion of decisional width of a regular class of
finite structures. Our main result states that given a first-order formula
$\psi$ over a vocabulary $\tau$, and a finite automaton $\mathcal{F}$ over a
suitable alphabet $\mathcal{B}(\Sigma,0pt,\tau)$ representing a width-$0pt$
regular-decisional class of $\tau$-structures $\mathcal{C}$, one can decide in
time $f(\tau,\Sigma,\psi,0pt)\cdot|\mathcal{F}|$ whether some $\tau$-structure
in $\mathcal{C}$ satisfies $\psi$. Here, $f$ is a function that depends on the
parameters $\tau,\Sigma,\psi,0pt$, but not on the size of the automaton
$\mathcal{F}$ representing the class. Therefore, besides implying that the
first-order theory of any given regular-decisional class of finite structures
is decidable, it also implies that when the parameters $\tau$, $\psi$,
$\Sigma$ and $0pt$ are fixed, decidability can be achieved in linear time on
the size of the input automaton $\mathcal{F}$. Building on the proof of our
main result, we show that the problem of counting satisfying assignments for a
first-order logic formula in a given structure $\mathfrak{A}$ of width $0pt$
is fixed-parameter tractable with respect to $0pt$, and can be solved in
quadratic time on the length of the input representation of $\mathfrak{A}$.

Keywords. Automatic Structures, Width Measures, First Order Logic

##  1 Introduction

Relational structures can be used to formalize a wide variety of mathematical
constructions, such as graphs, hypergraphs, groups, rings, databases, etc. Not
surprisingly, relational structures are a central object of study in several
subfields of computer science, such as database theory, learning theory [16],
constraint satisfaction theory [8, 23], and automated theorem proving [26, 29,
10, 11, 31].

Given a class $\mathcal{C}$ of finite relational structures and a logic
$\mathcal{L}$, such as first-order logic (FO) or monadic second-order logic
(MSO), the $\mathcal{L}$ theory of $\mathcal{C}$ is the set
$\mathcal{T}(\mathcal{L},\mathcal{C})$ of all logical sentences from
$\mathcal{L}$ that are satisfied by at least one structure in $\mathcal{C}$.
The theory $\mathcal{T}(\mathcal{L},\mathcal{C})$ is said to be decidable if
the problem of determining whether a given sentence $\varphi$ belongs to
$\mathcal{T}(\mathcal{L},\mathcal{C})$ is decidable. Showing that the
$\mathcal{L}$ theory of a particular class of structures $\mathcal{C}$ is
decidable is an endeavour of fundamental importance because many interesting
mathematical statements can be formulated as the problem of determining
whether some/every/no structure in a given class $\mathcal{C}$ of finite
structures satisfies a given logical sentence $\varphi$.

The problem of deciding logical properties of relational structures has been
studied extensively in the field of automatic structure theory. Intuitively, a
relational structure is automatic if its domain and each of its relations can
be defined by finite automata. Although the idea of representing certain types
of relational structures using automata dates back to seminal work of Büchi
and Rabin, and it has been extensively applied in the field of automatic group
theory [15], Khoussainov and Nerode were the first to define and investigate a
general notion of automatic structure [22]. One early use of the notion of
automatic structure is in providing a simplified proof of a celebrated theorem
of Presburger stating that the first-order theory of $(\mathbb{N},+)$ is
decidable. In [25] Kruckman et al. introduced the notion of structure with
advice and used it to show that the first-order theory of $(\mathbb{Q},+)$ is
decidable. The theory of automatic structures with advice was extended by
Zaid, Grädel and Reinhardt and used to define classes of relational
structures. They showed that an automatic class of structures with advice has
decidable first-order logic theory if and only if the set of used advices has
a decidable monadic second-order logic theory [31].

Interesting classes of structures with decidable MSO theory can be obtained by
combining automata theoretic techniques with techniques from parameterized
complexity theory. In particular, for each fixed $k\in\mathbb{N}$, if
$\mathcal{C}$ is the class of graphs of treewidth at most $k$, and
$\mathcal{L}$ is the monadic second order logic of graphs with vertex-set and
edge-set quantifications (MSO2 logic), then the
$\mathcal{T}(\mathcal{L},\mathcal{C})$ is decidable [10, 31]. Given the
expressive power of MSO2 logic, this decidability result implies that for each
fixed $k\in\mathbb{N}$, the validity of several long-standing conjectures,
such as Hadwiger’s conjecture for $K_{r}$-free graphs (for each fixed $r\geq
7$) can be decided automatically when restricted to the class of graphs of
treewidth at most $k$. Similar decidability results can be obtained when
$\mathcal{C}$ is the class of graphs of cliquewidth at most $k$, for fixed
$k\in\mathbb{N}$, and $\mathcal{L}$ is the monadic second-order logic of
graphs with vertex-set quantifications (MSO1 logic) [11, 31]. On the other
hand, it is known that the MSO1 theory of any class of graphs that contain
arbitrarily large grids is undecidable. Additionally, a celebrated long-
standing conjecture due to Seese states that the MSO1 theory of any class of
graphs of unbounded cliquewidth is undecidable [28].

###  1.1 Our Contributions

In this work, we introduce a new width measure for finite relational
structures that builds on the notion of ordered decision diagrams (ODDs). An
ODD over an alphabet $\Sigma$ is essentially an acyclic finite automaton over
$\Sigma$ where states are split into a sequence of frontiers, and transitions
are split into a sequence of layers in such a way that transitions in layer
$i$ send states in frontier $i-1$ to states in frontier $i$. We note that ODDs
over a binary alphabet have been extensively studied in the literature and are
usually called OBDDs (ordered binary decision diagrams). This formalism has
been widely used in the field of symbolic computation due to its ability to
concisely represent certain classes of combinatorial structures with
exponentially many elements in the domain [5, 4, 19, 30, 27].

An important complexity measure when dealing with ODDs is the notion of width.
This is simply the maximum number of states in a frontier of the ODD. In this
work, we will be concerned with relational structures that can be represented
using ODDs whose width is bounded by a constant $0pt$. More precisely, we say
that a relational structure
$\mathfrak{A}=(\mathsf{R}_{0}(\mathfrak{A}),\mathsf{R}_{1}(\mathfrak{A}),\ldots,\mathsf{R}_{l}(\mathfrak{A}))$
over a relational vocabulary $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ is
$(\Sigma,0pt)$-decisional if its domain $\mathsf{R}_{0}(\mathfrak{A})$ can be
represented by an ODD of width at most $0pt$ over the alphabet $\Sigma$, and
each of its relations
$\mathsf{R}_{i}(\mathfrak{A})\subseteq\mathsf{R}_{0}(\mathfrak{A})^{\mathfrak{a}_{i}}$
can be represented by an ODD of width at most $0pt$ over the alphabet
$\Sigma^{\otimes\mathfrak{a}_{i}}$, i.e. the $\mathfrak{a}_{i}$-fold Cartesian
product of $\Sigma$. If we let $\mathcal{B}(\Sigma,0pt)$ denote the set of all
layers whose frontiers have size at most $0pt$, then an ODD over $\Sigma$ can
be represented as a word over the alphabet $\mathcal{B}(\Sigma,0pt)$.
Similarly, an ODD over $\Sigma^{\otimes\mathfrak{a}_{i}}$ of width at most
$0pt$ can be represented as a word over the alphabet
$\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt)$. Therefore, a
$(\Sigma,0pt)$-relational structure can be represented as a word over the
alphabet
$\mathcal{B}(\Sigma,0pt,\tau)\doteq\mathcal{B}(\Sigma,0pt)\otimes\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{1}},0pt)\otimes\cdots\otimes\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{l}},0pt)$.
Following this point of view, one can define classes of finite
$(\Sigma,0pt)$-structures over a vocabulary $\tau$ using languages over the
alphabet $\mathcal{B}(\Sigma,0pt,\tau)$. In particular, we will be concerned
with classes of structures that can be defined using regular languages over
$\mathcal{B}(\Sigma,0pt,\tau)$. We say that that a class $\mathcal{C}$ of
finite relational structures is $(\Sigma,0pt)$-regular-decisional if there is
a finite automaton $\mathcal{F}$ over $\mathcal{B}(\Sigma,0pt,\tau)$ whose
words represent precisely those structures in $\mathcal{C}$.

In this work, we show that given a first order sentence $\psi$ over a
vocabulary $\tau$, an alphabet $\Sigma$ and a constant $0pt$, the class of
$(\Sigma,0pt)$-decisional structures satisfying $\psi$ is
$(\Sigma,0pt)$-regular-decisional. Building on this result we show that given
a finite automaton $\mathcal{F}$ over the alphabet
$\mathcal{B}(\Sigma,0pt,\tau)$ representing a class $\mathcal{C}$ of
structures, one can decide in time $f(\tau,\Sigma,\psi,0pt)\cdot|\mathcal{F}|$
whether some structure defined by a word in $L(\mathcal{F})$ satisfies
$\varphi$. Finally, we show that given a formula $\psi$ over $\tau$ with $t$
variables $x_{1},\dots,x_{t}$, and a presentation of a $\tau$-structure
$\mathfrak{A}$ as a tuple of ODDs of length $k$ and width $0pt$, one can count
in time $f(\tau,\Sigma,\psi,t,0pt)\cdot k$ the number of assignments for
$x_{1},\dots,x_{t}$ that satisfy $\psi$ on $\mathfrak{A}$. As a
straightforward application of this result, we have that several counting
problems that are $\\#W[1]$-complete or $\\#W[2]$-complete on general graphs,
such as counting the number of independent sets of size $r$ or the number of
dominating sets of size $r$ (for fixed $r$), can be solved in FPT time on
$(\Sigma,0pt)$-decisional graphs, provided a presentation is given at the
input.

An interesting feature of our width measure for classes of structures is that
it behaves very differently from usual complexity measures for graphs studied
in structural complexity theory. As an example of this fact, we note that the
family of hypercube graphs has regular-decisional width $2$, while it has
unbounded width in many of the studied measures, such as treewidth and
cliquewidth. This class of graphs has also unbounded degeneracy, and therefore
it is not no-where dense. As a consequence, we have that most algorithmic
meta-theorems proved so far dealing with the interplay between first-order
logic and structural graph theory [17, 24, 18] fail on graphs of constant
decisional-width. In this regard, it is interesting to note that our first-
order decidability result cannot be generalized to MSO1 logic, since the class
of grid graphs has constant decisional width, while the MSO1 theory of grids
is known to be undecidable [28, 20].

##  2 Preliminaries

We denote by $\mathbb{N}\doteq\\{0,1,\ldots\\}$ the set of natural numbers
(including zero), and by $\mathbb{N}_{+}\doteq\mathbb{N}\setminus\\{0\\}$ the
set of positive natural numbers. For each $c\in\mathbb{N}_{+}$, we let
$[c]\doteq\\{1,2,\ldots,c\\}$ and $\llbracket
c\rrbracket\doteq\\{0,1,\ldots,c-1\\}$. Given a set $S$ and a number
$a\in\mathbb{N}_{+}$, we let $S^{\times a}$ be the set of all $a$-tuples of
elements from $S$.

##### Relational Structures.

A _relational vocabulary_ is a tuple
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ of _relation symbols_ where for
each $i\in[l]$, the relation symbol $\mathsf{R}_{i}$ is associated with an
arity $\mathfrak{a}_{i}\in\mathbb{N}_{+}$. Let
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary. A
finite _$\tau$ -structure_ is a tuple
$\mathfrak{A}=(\mathsf{R}_{0}(\mathfrak{A}),R_{1}(\mathfrak{A}),\ldots,R_{l}(\mathfrak{A}))$
such that

  1. 1.

$\mathsf{R}_{0}(\mathfrak{A})$ is a non-empty finite set, called the _domain_
of $\mathfrak{A}$;

  2. 2.

for each $i\in[l]$,
$R_{i}(\mathfrak{A})\subseteq\mathsf{R}_{0}(\mathfrak{A})^{\times\mathfrak{a}_{i}}$
is an $\mathfrak{a}_{i}$-ary relation.

Let $\mathfrak{A}$ and $\mathfrak{A}^{\prime}$ be $\tau$-structures. An
_isomorphism from $\mathfrak{A}$ to $\mathfrak{A}^{\prime}$_ is a bijection
$\pi\colon\mathsf{R}_{0}(\mathfrak{A})\rightarrow\mathsf{R}_{0}(\mathfrak{A}^{\prime})$
such that, for each $i\in[l]$,
$(u_{1},\ldots,u_{\mathfrak{a}_{i}})\in\mathsf{R}_{i}(\mathfrak{A})$ if and
only if
$(\pi(u_{1}),\dots,\pi(u_{\mathfrak{a}_{i}}))\in\mathsf{R}_{i}(\mathfrak{A}^{\prime})$.
If there exists an isomorphism from $\mathfrak{A}$ to $\mathfrak{A}^{\prime}$,
then we say that $\mathfrak{A}$ is _isomorphic_ to $\mathfrak{A}^{\prime}$,
and we denote this fact by $\mathfrak{A}\simeq\mathfrak{A}^{\prime}$.

##### First-Order Logic.

Now, we briefly recall some basic concepts from first-order logic. Extensive
treatments of this subject can be found in [12, 13].

Let $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary.
We denote by $\mathrm{FO}\\{\tau\\}$ the set of all _first-order logic
formulas over $\tau$_, i.e. the logic formulas comprising: variables to be
used as placeholders for elements from the domain of a $\tau$-structure; the
Boolean connectives $\vee$, $\wedge$, $\neg$, $\rightarrow$ and
$\leftrightarrow$; the quantifiers $\exists$ and $\forall$ that can be applied
to the variables; and the atomic logic formulas $x=y$, where $x$ and $y$ are
variables, and $R_{i}(x_{1},\ldots,x_{\mathfrak{a}_{i}})$ for some $i\in[l]$,
where $x_{1},\ldots,x_{\mathfrak{a}_{i}}$ are variables.

A variable $x$ is said to be free in a formula $\mathrm{FO}\\{\tau\\}$ if some
of its occurrences is outside the scope of any quantifier. We let
$\mathrm{freevar}(\psi)$ denote the set of variables that are free in $\psi$.
We write $\psi(x_{1},\ldots,x_{t})$ to indicate that
$\mathrm{freevar}(\psi)\subseteq\\{x_{1},\ldots,x_{t}\\}$. A _sentence_ is a
formula without free variables.

Let
$\mathfrak{A}=(\mathsf{R}_{0}(\mathfrak{A}),\mathsf{R}_{1}(\mathfrak{A}),\ldots,\mathsf{R}_{l}(\mathfrak{A}))$
be a finite $\tau$-structure,
$\psi(x_{1},\ldots,x_{t})\in\mathrm{FO}\\{\tau\\}$ and
$u_{1},\ldots,u_{t}\in\mathsf{R}_{0}(\mathfrak{A})$. We write
$\mathfrak{A}\models\psi[u_{1},\ldots,u_{t}]$ to mean that $\mathfrak{A}$
satisfies $\psi$ when all the free occurrences of the variables
$x_{1},\ldots,x_{t}$ are interpreted by the values $u_{1},\ldots,u_{t}$,
respectively. In particular, if $\psi$ is a sentence, then we may write
$\mathfrak{A}\models\psi$ to mean that $\mathfrak{A}$ satisfies $\psi$. In
this case, we also say that $\mathfrak{A}$ is a _model_ of $\psi$. If
$\psi(x_{1},\ldots,x_{t})\equiv\mathsf{R}_{i}(x_{\beta(1)},\ldots,x_{\beta(\mathfrak{a}_{i})})$
for some mapping $\beta\colon[\mathfrak{a}_{i}]\rightarrow[t]$ and some
$i\in[l]$, then $\mathfrak{A}\models\psi[u_{1},\ldots,u_{t}]$ if and only if
$(u_{\beta(1)},\ldots,u_{\beta(\mathfrak{a}_{i})})\in\mathsf{R}_{i}(\mathfrak{A})$.
The semantics of the equality symbol, of the quantifiers $\exists$ and
$\forall$, and of the Boolean connectives $\vee$, $\wedge$, $\neg$,
$\rightarrow$ and $\leftrightarrow$ are the usual ones.

##### Languages.

An _alphabet_ is any finite, non-empty set of symbols $\Sigma$. A _string_
over $\Sigma$ is any finite sequence of symbols from $\Sigma$. We denote by
$\Sigma^{*}$ the set of all strings over $\Sigma$, including the empty string
$\varepsilon$, and by $\Sigma^{+}$ the set of all (non-empty) strings over
$\Sigma$. A _language_ over $\Sigma$ is any subset $L$ of $\Sigma^{*}$. In
particular, for each $k\in\mathbb{N}_{+}$, we let $\Sigma^{k}$ be the language
of all strings of length $k$ over $\Sigma$, and we let $\Sigma^{\leq
k}\doteq\Sigma^{1}\cup\cdots\cup\Sigma^{k}$ be the language of all (non-empty)
strings of length at most $k$ over $\Sigma$.

For each alphabet $\Sigma$, we let $\square$ be a special symbol, called the
padding symbol, such that $\square\not\in\Sigma$, and we write
$\Sigma\uplus\\{\square\\}$ to denote the disjoint union between $\Sigma$ and
$\\{\square\\}$. For each $\sigma\in\Sigma\uplus\\{\square\\}$ and each
$c\in\mathbb{N}_{+}$, we let $\sigma^{\times c}$ denote the tuple
$(\sigma,\ldots,\sigma)$ composed by $c$ copies of the symbol $\sigma$.

##### Tensor Product.

Let $\Sigma_{1},\ldots,\Sigma_{c}$ be $c$ alphabets, where
$c\in\mathbb{N}_{+}$. The _tensor product_ of $\Sigma_{1},\ldots,\Sigma_{c}$
is defined as the alphabet

$\Sigma_{1}\otimes\cdots\otimes\Sigma_{c}\doteq\\{(\sigma_{1},\ldots,\sigma_{c})\colon\sigma_{i}\in\Sigma_{i},\;i\in[c]\\}\text{.}$

In particular, for each $c\in\mathbb{N}_{+}$ and each alphabet $\Sigma$, we
define the _$c$ -th tensor power_ of $\Sigma$ as the alphabet $\Sigma^{\otimes
c}\doteq\overbrace{\Sigma\otimes\cdots\otimes\Sigma}^{c\;\mathit{times}}\text{.}$
Note that the tensor product of $\Sigma_{1},\ldots,\Sigma_{c}$ (the $c$-th
tensor power of $\Sigma$) may be simply regarded as the Cartesian product of
$\Sigma_{1},\ldots,\Sigma_{c}$ (the $c$-ary Cartesian power of $\Sigma$,
respectively). Also, note that $\Sigma^{\otimes 1}=\Sigma$.

For each $i\in[c]$, let $s_{i}=\sigma_{i,1}\cdots\sigma_{i,k_{i}}$ be a string
of length $k_{i}$, where $k_{i}\in\mathbb{N}_{+}$, over the alphabet
$\Sigma_{i}$. The _tensor product_ of $s_{1},\ldots,s_{c}$ is defined as the
string

$s_{1}\otimes\cdots\otimes
s_{c}\doteq(\widetilde{\sigma}_{1,1},\ldots,\widetilde{\sigma}_{c,1})\cdots(\widetilde{\sigma}_{1,k},\ldots,\widetilde{\sigma}_{c,k})\text{}$

of length $k=\max\\{k_{1},\ldots,k_{c}\\}$ over the alphabet
$(\Sigma_{1}\uplus\\{\square\\})\otimes\cdots\otimes(\Sigma_{c}\uplus\\{\square\\})$
such that, for each $i\in[c]$ and each $j\in[k]$,

$\widetilde{\sigma}_{i,j}\doteq\left\\{\begin{array}[]{lr}\sigma_{i,j}&\text{
if }j\leq k_{i}\\\ \square&\text{ otherwise.}\end{array}\right.$

For instance, the tensor product of the strings $aabab$ and $abb$ over the
alphabet $\\{a,b\\}$ is the string $(a,a)(a,b)(b,b)(a,\square)(b,\square)$
over the alphabet $(\\{a,b\\}\uplus\\{\square\\})^{\otimes 2}$.

For each $i\in[c]$, let $L_{i}\subseteq\Sigma_{i}^{+}$ be a language over the
alphabet $\Sigma_{i}$. The _tensor product_ of $L_{1},\ldots,L_{c}$ is defined
as the language

$L_{1}\otimes\cdots\otimes L_{c}\doteq\\{s_{1}\otimes\cdots\otimes s_{c}\colon
s_{i}\in L_{i},i\in[c]\\}\text{.}$

We remark that in the literature [2, 3, 21, 31] the tensor product of strings
(as well as the tensor product of languages) is also commonly called of
_convolution_.

##### Finite Automata.

A _finite automaton_ is a tuple $\mathcal{F}=(\Sigma,Q,T,I,F)$, where $\Sigma$
is an alphabet, $Q$ is a finite set of _states_ , ${T\subseteq
Q\times\Sigma\times Q}$ is a set of _transitions_ , $I\subseteq Q$ is a set of
_initial states_ and $F\subseteq Q$ is a set of _final states_. The size of a
finite automaton $\mathcal{F}$ is defined as
$\lvert\mathcal{F}\rvert\doteq\lvert Q\rvert+\lvert T\rvert\log|\Sigma|$.

Let $k\in\mathbb{N}_{+}$ and $s=\sigma_{1}\cdots\sigma_{k}\in\Sigma^{k}$. We
say that $\mathcal{F}$ _accepts_ $s$ if there exists a sequence of transitions
$\langle(q_{0},\sigma_{1},q_{1}),(q_{1},\sigma_{2},q_{2}),\ldots,(q_{k-1},\sigma_{k},q_{k})\rangle$,
called an _accepting sequence_ for $s$ in $\mathcal{F}$, such that $q_{0}\in
I$, $q_{k}\in F$ and, for each $i\in[k]$, ${(q_{i-1},\sigma_{i},q_{i})\in T}$.
The language of $\mathcal{F}$, denoted by $\bm{\mathcal{L}}(\mathcal{F})$, is
defined as the set of all strings accepted by $\mathcal{F}$, i.e.
$\bm{\mathcal{L}}(\mathcal{F})\doteq\left\\{s\in\Sigma^{+}\colon s\text{ is
accepted by }\mathcal{F}\right\\}\text{.}$

##### Regular Relations.

Let $\Sigma$ be an alphabet. A language $L\subseteq\Sigma^{+}$ is called
_regular_ if there exists a finite automaton $\mathcal{F}$ over $\Sigma$ such
that $\bm{\mathcal{L}}(\mathcal{F})=L$.

For each $\mathfrak{a}\in\mathbb{N}_{+}$ and each language
$L\subseteq(\Sigma^{\otimes\mathfrak{a}})^{+}$ over the alphabet
$\Sigma^{\otimes\mathfrak{a}}$, we let
$\mathsf{rel}(L)\doteq\\{(s_{1},\ldots,s_{\mathfrak{a}})\colon
s_{1}\otimes\cdots\otimes s_{\mathfrak{a}}\in L\\}$ be the _relation
associated with $L$_. On the other hand, for each
$\mathfrak{a}\in\mathbb{N}_{+}$ and each $\mathfrak{a}$-ary relation
$R\subseteq(\Sigma^{+})^{\times\mathfrak{a}}$, we let
$\mathsf{lang}(R)\doteq\\{s_{1}\otimes\cdots\otimes
s_{\mathfrak{a}}\colon(s_{1},\ldots,s_{\mathfrak{a}})\in R\\}$ be the
_language associated with $R$_. We say that such a relation $R$ is _regular_
if its associated language $\mathsf{lang}(R)$ is a regular subset of
$(\Sigma^{\otimes\mathfrak{a}})^{+}$.

##  3 Ordered Decision Diagrams

Let $\Sigma$ be an alphabet and $0pt\in\mathbb{N}_{+}$. A _$(\Sigma,0pt)$
-layer_ is a tuple $B\doteq(\ell,r,T,I,F,\iota,\phi)$, where
$\ell\subseteq\llbracket 0pt\rrbracket$ is a set of _left states_ ,
$r\subseteq\llbracket 0pt\rrbracket$ is a set of _right states_ ,
$T\subseteq\ell\times(\Sigma\uplus\\{\square\\})\times r$ is a set of
_transitions_ , $I\subseteq\ell$ is a set of _initial states_ , $F\subseteq r$
is a set of _final states_ and $\iota,\phi\in\\{0,1\\}$ are Boolean flags
satisfying the following conditions:  i) $I=\emptyset$if $\iota=0$, and  ii)
$F=\emptyset$if $\phi=0$.  We remark that it is possible that $\iota=1$ and
$I=\emptyset$. Similarly, it might be the case in which $\phi=1$ and
$F=\emptyset$.

In what follows, we may write $\ell(B)$, $r(B)$, $T(B)$, $I(B)$, $F(B)$,
$\iota(B)$ and $\phi(B)$ to refer to the sets $\ell$, $r$, $T$, $I$ and $F$
and to the Boolean flags $\iota$ and $\phi$, respectively.

We let $\mathcal{B}(\Sigma,0pt)$ denote the set of all $(\Sigma,0pt)$-layers.
Note that, $\mathcal{B}(\Sigma,0pt)$ is non-empty and has at most
$2^{\mathcal{O}(\lvert\Sigma\rvert\cdot 0pt^{2})}$ elements. Therefore,
$\mathcal{B}(\Sigma,0pt)$ may be regarded as an alphabet.

Let $k\in\mathbb{N}_{+}$. A _$(\Sigma,0pt)$ -ordered decision diagram_ (or
simply, $(\Sigma,0pt)$-_ODD_) of _length_ $k$ is a string $D\doteq B_{1}\cdots
B_{k}\in\mathcal{B}(\Sigma,0pt)^{k}$ of length $k$ over the alphabet
$\mathcal{B}(\Sigma,0pt)$ satisfying the following conditions:

  1. 1.

for each $i\in[k-1]$, $\ell(B_{i+1})=r(B_{i})$;

  2. 2.

$\iota(B_{1})=1$ and, for each $i\in\\{2,\ldots,k\\}$, $\iota(B_{i})=0$;

  3. 3.

$\phi(B_{k})=1$ and, for each $i\in[k-1]$, $\phi(B_{i})=0$.

The _width_ of $D$ is defined as
$\omega(D)\doteq\max\left\\{\lvert\ell(B_{1})\rvert,\ldots,\lvert\ell(B_{k})\rvert,\lvert
r(B_{k})\rvert\right\\}\text{.}$ We remark that $\omega(D)\leq 0pt$.

For each $k\in\mathbb{N}_{+}$, we denote by
$\mathcal{B}(\Sigma,0pt)^{\circ{k}}$ the set of all $(\Sigma,0pt)$-ODDs of
length $k$. And, more generally, we let
$\mathcal{B}(\Sigma,0pt)^{\circledast}$ be the set of all $(\Sigma,0pt)$-ODDs,
i.e.
$\mathcal{B}(\Sigma,0pt)^{\circledast}\doteq\bigcup_{k\in\mathbb{N}_{+}}\mathcal{B}(\Sigma,0pt)^{\circ{k}}$.

Let $D=B_{1}\cdots B_{k}\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}$ and
$s=\sigma_{1}\cdots\sigma_{k^{\prime}}\in\Sigma^{\leq k}$. A _valid sequence_
for $s$ in $D$ is a sequence of transitions
$\langle(\mathfrak{p}_{1},\widetilde{\sigma}_{1},\mathfrak{q}_{1}),\ldots,(\mathfrak{p}_{k},\widetilde{\sigma}_{k},\mathfrak{q}_{k})\rangle$
satisfying the following conditions:

  1. 1.

for each $i\in[k]$, $\widetilde{\sigma}_{i}=\sigma_{i}$ if $i\leq k^{\prime}$,
and $\widetilde{\sigma}_{i}=\square$ otherwise;

  2. 2.

for each $i\in[k]$,
$(\mathfrak{p}_{i},\widetilde{\sigma}_{i},\mathfrak{q}_{i})\in T(B_{i})$;

  3. 3.

for each $i\in[k-1]$, $\mathfrak{p}_{i+1}=\mathfrak{q}_{i}$.

Such a sequence is called _accepting_ for $s$ if, in addition to the above
conditions, $\mathfrak{p}_{1}\in I(B_{1})$ and $\mathfrak{q}_{k}\in F(B_{k})$.
We say that $D$ _accepts_ $s$ if there exists an accepting sequence for $s$ in
$D$. The language of $D$, denoted by $\mathcal{L}(D)$, is defined as the set
of all strings accepted by $D$, i.e.
$\mathcal{L}(D)\doteq\left\\{s\in\Sigma^{\leq k}\colon s\text{ is accepted by
}D\right\\}\text{.}$

######  Proposition 1.

Let $\Sigma$ be an alphabet, $0pt,k\in\mathbb{N}_{+}$ and
$D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}$. For each natural number
$k^{\prime}\geq k$, there exists an ODD
$D^{\prime}\in\mathcal{B}(\Sigma,0pt)^{\circ{k^{\prime}}}$ such that
$\mathcal{L}(D^{\prime})=\mathcal{L}(D)$.

###### Proof.

Assume that $D=B_{1}\cdots B_{k}\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}$. If
$k^{\prime}=k$, then simply define $D^{\prime}=D$. Thus, assume that
$k^{\prime}>k$, and let $D^{\prime}=B^{\prime}_{1}\cdots
B^{\prime}_{k}B^{\prime}_{k+1}\cdots B^{\prime}_{k^{\prime}}$ be the ODD in
$\mathcal{B}(\Sigma,0pt)^{\circ{k^{\prime}}}$ defined as follows.

  * •

For each $i\in[k-1]$, we let $B^{\prime}_{i}=B_{i}$.

  * •

We let $B^{\prime}_{k}$ be the layer in $\mathcal{B}(\Sigma,0pt)$ obtained
from $B_{k}$ by setting $F(B^{\prime}_{k})=\emptyset$ and
$\phi(B^{\prime}_{k})=0$.

  * •

We let $B^{\prime}_{k+1}$ be the layer in $\mathcal{B}(\Sigma,0pt)$ defined as
follows: $\ell(B^{\prime}_{k+1})=F(B_{k})$; $r(B^{\prime}_{k+1})=\\{0\\}$;
$T(B^{\prime}_{k+1})=\\{(\mathfrak{p},\square,0)\colon\mathfrak{p}\in
F(B_{k})\\}$; $I(B^{\prime}_{k+1})=\emptyset$; $F(B^{\prime}_{k+1})=\emptyset$
if $k^{\prime}>k+1$, and $F(B^{\prime}_{k+1})=\\{0\\}$ otherwise;
$\iota(B^{\prime}_{k+1})=0$; and $\phi(B^{\prime}_{k+1})=0$ if
$k^{\prime}>k+1$, and $\phi(B^{\prime}_{k+1})=1$ otherwise.

  * •

Finally, for each $i\in\\{k+2,\ldots,k^{\prime}\\}$, we let $B^{\prime}_{i}$
be the layer in $\mathcal{B}(\Sigma,0pt)$ defined as follows:
$\ell(B^{\prime}_{i})=r(B^{\prime}_{i})=\\{0\\}$;
$T(B^{\prime}_{i})=\\{(0,\square,0)\\}$; $I(B^{\prime}_{i})=\emptyset$;
$F(B^{\prime}_{i})=\emptyset$ if $i<k^{\prime}$, and
$F(B^{\prime}_{i})=\\{0\\}$ otherwise; $\iota(B^{\prime}_{i})=0$; and
$\phi(B^{\prime}_{i})=0$ if $i<k^{\prime}$, and $\phi(B^{\prime}_{i})=1$
otherwise.

One can verify that $D^{\prime}$ is in fact an ODD in
$\mathcal{B}(\Sigma,0pt)^{\circ{k^{\prime}}}$ and
$\mathcal{L}(D^{\prime})=\mathcal{L}(D)$. ∎

##  4 Regular-Decisional Classes of Finite Relational Structures

In this section we combine ODDs with finite automata in order to define
infinite classes of finite structures. We start by defining the notion of
$(\Sigma,0pt,\tau)$-structural tuples of ODDs as a way to encode single finite
$\tau$-structures. Subsequently, we use finite automata over a suitable
alphabet in order to uniformly define infinite families of finite
$\tau$-structures.

###  4.1 Decisional Relations and Decisional Relational Structures

Let $\Sigma$ be an alphabet and $\mathfrak{a},0pt\in\mathbb{N}_{+}$. A
_finite_ $\mathfrak{a}$-ary relation
$R\subseteq(\Sigma^{+})^{\times\mathfrak{a}}$ is said to be strongly
$(\Sigma,0pt)$-decisional if there exists an ODD $D$ in
$\mathcal{B}(\Sigma^{\otimes\mathfrak{a}},0pt)^{\circledast}$ such that
$\mathsf{rel}(\mathcal{L}(D))=R$. Given a set $S$, we say that a relation
$R\subseteq S^{\times\mathfrak{a}}$ is $(\Sigma,0pt)$-decisional if $R$ is
isomorphic to some strongly $(\Sigma,0pt)$-decisional structure.

Let $\tau=(\mathsf{R}_{1},\dots,\mathsf{R}_{l})$ be a relational vocabulary,
$\Sigma$ be an alphabet and $0pt\in\mathbb{N}_{+}$. We say that a tuple
$\mathcal{D}=(D_{0},D_{1},\dots,D_{l})$ of ODDs is _$(\Sigma,0pt,\tau)$
-structural_ if there exists a positive natural number $k\in\mathbb{N}_{+}$,
called the _length of $\mathcal{D}$_, such that the following conditions are
satisfied:

  1. 1.

$D_{0}$ is an ODD in $\mathcal{B}(\Sigma,0pt)^{\circ{k}}$;

  2. 2.

for each $i\in[l]$, $D_{i}$ is an ODD in
$\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt)^{\circ{k}}$;

  3. 3.

for each $i\in[l]$,
$\mathcal{L}(D_{i})\subseteq\mathcal{L}(D_{0})^{\otimes\mathfrak{a}_{i}}$.

Let $\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$ be a
$(\Sigma,0pt,\tau)$-structural tuple. The _$\tau$ -structure derived from
$\mathcal{D}$_ is defined as the finite $\tau$-structure

$\mathfrak{s}(\mathcal{D})\doteq(\mathsf{R}_{0}(\mathfrak{s}(\mathcal{D})),\mathsf{R}_{1}(\mathfrak{s}(\mathcal{D})),\ldots,\mathsf{R}_{l}(\mathfrak{s}(\mathcal{D})))\text{,}$

with domain $\mathsf{R}_{0}(\mathfrak{s}(\mathcal{D}))=\mathcal{L}(D_{0})$,
such that
$\mathsf{R}_{i}(\mathfrak{s}(\mathcal{D}))=\mathsf{rel}(\mathcal{L}(D_{i}))$
for each $i\in[l]$.

We say that a finite $\tau$-structure $\mathfrak{A}$ is _strongly
$(\Sigma,0pt)$-decisional_ if there exists some $(\Sigma,0pt,\tau)$-structural
tuple $\mathcal{D}$ such that $\mathfrak{A}=\mathfrak{s}(\mathcal{D})$. We say
that a finite $\tau$-structure $\mathfrak{A}$, whose domain is not necessarily
a subset of $\Sigma^{+}$, is $(\Sigma,0pt)$-decisional if $\mathfrak{A}$ is
isomorphic to some strongly $(\Sigma,0pt)$-decisional structure.

The _$\Sigma$ -decisional width_ of a finite $\tau$-structure $\mathfrak{A}$,
denoted by $\omega(\Sigma,\mathfrak{A})$, is defined as the minimum
$0pt\in\mathbb{N}_{+}$ such that $\mathfrak{A}$ is $(\Sigma,0pt)$-decisional.
The following proposition states that if a relation is
$(\Sigma,0pt)$-decisional, then it is also
$(\\{0,1\\},0pt^{\prime})$-decisional for a suitable
$0pt^{\prime}\in\mathbb{N}_{+}$.

######  Proposition 2.

Let $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary,
$\Sigma$ be an alphabet and $0pt\in\mathbb{N}_{+}$. If $\mathfrak{A}$ is a
finite $\tau$-structure with $\omega(\Sigma,\mathfrak{A})\leq 0pt$ for some
$0pt\in\mathbb{N}_{+}$, then $\omega(\\{0,1\\},\mathfrak{A})\leq
0pt^{2}\cdot\lvert\Sigma\rvert^{\max\\{1,\mathfrak{a}_{1},\ldots,\mathfrak{a}_{l}\\}}$.

###### Proof.

Since by hypothesis $\omega(\Sigma,\mathfrak{A})\leq 0pt$, there exists a
strongly $(\Sigma,0pt)$-decisional $\tau$-structure that is isomorphic to
$\mathfrak{A}$. Thus, for simplicity, assume without loss of generality that
$\mathfrak{A}$ is strongly $(\Sigma,0pt)$-decisional. For each $i\in\llbracket
l+1\rrbracket$, let
$D_{i}\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt)^{\circledast}$ such
that $\mathsf{rel}(\mathcal{L}(D_{i}))=\mathsf{R}_{i}(\mathfrak{A})$, where
$\mathfrak{a}_{0}=1$. Based on Proposition 1, we can assume without loss of
generality that the ODDs $D_{0},D_{1},\ldots,D_{l}$ have the same length, say
$k\in\mathbb{N}_{+}$. Thus, assume that $D_{i}=B_{i,1}\cdots B_{i,k}$ for each
$i\in\llbracket l+1\rrbracket$.

Let $c=\lceil\log_{2}\lvert\Sigma\rvert\rceil$ and
$\alpha\colon(\Sigma\uplus\\{\square\\})\rightarrow(\\{0,1\\}\uplus\\{\square\\})^{c}$
be an injection, which sends each symbol in $\Sigma\uplus\\{\square\\}$ to a
string of length $c$ over $\\{0,1\\}\uplus\\{\square\\}$, such that
$\alpha(\square)\in\\{\square\\}^{c}$ and, for each $\sigma\in\Sigma$,
$\alpha(\sigma)\in\\{0,1\\}^{c}$. Note that, each symbol in $\Sigma$ can be
associated with an exclusive number in
$\llbracket\lvert\Sigma\rvert\rrbracket$. Thus, we might, for instance,
consider $\alpha$ as the encoding which sends each symbol in $\Sigma$ to the
usual binary representation, with $c$ bits, of its associated number in
$\llbracket\lvert\Sigma\rvert\rrbracket$.

For each symbol $\widetilde{\sigma}\in\Sigma\uplus\\{\square\\}$ and each
$h\in[c]$, we let $\alpha(\widetilde{\sigma},h)$ denote the $h$-th symbol of
$\alpha(\widetilde{\sigma})$, i.e., if
$\alpha(\widetilde{\sigma})=\widetilde{\nu}_{1}\cdots\widetilde{\nu}_{c}$,
then
$\alpha(\widetilde{\sigma},h)=\widetilde{\nu}_{h}\in\\{0,1\\}\uplus\\{\square\\}$.

Let $k^{\prime}=k\cdot c$, and let $j=g\cdot c+h$, where $g\in\llbracket
k\rrbracket$ and $h\in[c]$. For each $i\in\llbracket l+1\rrbracket$, consider
the layer
$B^{\prime}_{i,j}\in\mathcal{B}(\\{0,1\\}^{\otimes\mathfrak{a}_{i}},0pt^{2}\cdot\lvert\Sigma\rvert^{\mathfrak{a}_{i}})$
with left state set: $\ell(B^{\prime}_{i,j})=\ell(B_{i,g+1})$ if $h=1$, and
$\ell(B^{\prime}_{i,j})=\llbracket\lvert T(B_{i,g+1})\rvert\rrbracket$
otherwise; right state set: $r(B^{\prime}_{i,j})=r(B_{i,g+1})$ if $h=c$, and
$r(B^{\prime}_{i,j})=\llbracket\lvert T(B_{i,g+1})\rvert\rrbracket$ otherwise;
transition set

$T(B^{\prime}_{i,j})=\begin{cases}\begin{multlined}\big{\\{}\left(\mathfrak{p},\left(\alpha(\widetilde{\sigma}_{1}),\ldots,\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}})\right),\mathfrak{q}\right)\colon\\\\[-10.76385pt]
\hfil(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}\end{multlined}\big{\\{}\left(\mathfrak{p},\left(\alpha(\widetilde{\sigma}_{1}),\ldots,\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}})\right),\mathfrak{q}\right)\colon\\\\[-10.76385pt]
\hfil(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}&\text{ if }c=1\text{}\\\\[10.76385pt]
\begin{multlined}\big{\\{}\left(\mathfrak{p},\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},1)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},1)}\right),\beta(\delta)\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}\end{multlined}\big{\\{}\left(\mathfrak{p},\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},1)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},1)}\right),\beta(\delta)\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}&\text{ if }c\neq 1\text{ and }h=1\text{}\\\\[10.76385pt]
\begin{multlined}\big{\\{}\left(\beta(\delta),\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},c)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},c)}\right),\mathfrak{q}\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}\end{multlined}\big{\\{}\left(\beta(\delta),\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},c)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},c)}\right),\mathfrak{q}\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}&\text{ if }c\neq 1\text{ and }h=c\text{}\\\\[10.76385pt]
\begin{multlined}\big{\\{}\left(\beta(\delta),\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},h)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},h)}\right),\beta(\delta)\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}\end{multlined}\big{\\{}\left(\beta(\delta),\left({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{1},h)},\ldots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\alpha(\widetilde{\sigma}_{\mathfrak{a}_{i}},h)}\right),\beta(\delta)\right)\colon\\\\[-10.76385pt]
\hfil\exists\,\delta=(\mathfrak{p},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{i}}),\mathfrak{q})\in
T(B_{i,g+1})\big{)}&\text{ otherwise, }\\\\[10.76385pt] \end{cases}$

where $\beta\colon T(B_{i,g+1})\rightarrow\llbracket\lvert
T(B_{i,g+1})\rvert\rrbracket$ denotes an arbitrary bijection that sends each
transition in $T(B_{i,g+1})$ to an exclusive number in $\llbracket\lvert
T(B_{i,g+1})\rvert\rrbracket$; initial state set:
$I(B^{\prime}_{i,j})=I(B_{i,g+1})$ if $j=1$, and
$I(B^{\prime}_{i,j})=\emptyset$ otherwise; final state set:
$F(B^{\prime}_{i,j})=F(B_{i,g+1})$ if $j=k^{\prime}$, and
$F(B^{\prime}_{i,j})=\emptyset$ otherwise; initial Boolean flag:
$\iota(B^{\prime}_{i,j})=1$ if $j=1$, and $\iota(B^{\prime}_{i,j})=0$
otherwise; and final Boolean flag: $\phi(B^{\prime}_{i,j})=1$ if
$j=k^{\prime}$, and $\phi(B^{\prime}_{i,j})=0$ otherwise.

One can verify that, for each $i\in\llbracket l+1\rrbracket$,
$D^{\prime}_{i}=B^{\prime}_{i,1}\cdots B^{\prime}_{i,k^{\prime}}$ is an ODD in
$\mathcal{B}(\\{0,1\\}^{\otimes\mathfrak{a}_{i}},0pt^{2}\cdot\lvert\Sigma\rvert^{\mathfrak{a}_{i}})^{\circ{k^{\prime}}}$
with language

$\begin{multlined}\mathcal{L}(D^{\prime}_{i})=\Big{\\{}\big{(}\alpha(\widetilde{\sigma}_{1,1},1),\ldots,\alpha(\widetilde{\sigma}_{1,\mathfrak{a}_{i}},1)\big{)}\cdots\left(\alpha(\widetilde{\sigma}_{1,1},c),\ldots,\alpha(\widetilde{\sigma}_{1,\mathfrak{a}_{i}},c)\right)\cdots\\\
\hfill\big{(}\alpha(\widetilde{\sigma}_{k,1},1),\ldots,\alpha(\widetilde{\sigma}_{k,\mathfrak{a}_{i}},1)\big{)}\cdots\big{(}\alpha(\widetilde{\sigma}_{k,1},c),\ldots,\alpha(\widetilde{\sigma}_{k,\mathfrak{a}_{i}},c)\big{)}\colon\hskip
17.22217pt\\\
\hfill\big{(}\widetilde{\sigma}_{1,1},\ldots,\widetilde{\sigma}_{1,\mathfrak{a}_{i}}\big{)}\cdots\big{(}\widetilde{\sigma}_{k,1},\ldots,\widetilde{\sigma}_{k,\mathfrak{a}_{i}}\big{)}\in\mathcal{L}(D^{\prime}_{i})\Big{\\}}\text{.}\end{multlined}\mathcal{L}(D^{\prime}_{i})=\Big{\\{}\big{(}\alpha(\widetilde{\sigma}_{1,1},1),\ldots,\alpha(\widetilde{\sigma}_{1,\mathfrak{a}_{i}},1)\big{)}\cdots\left(\alpha(\widetilde{\sigma}_{1,1},c),\ldots,\alpha(\widetilde{\sigma}_{1,\mathfrak{a}_{i}},c)\right)\cdots\\\
\hfill\big{(}\alpha(\widetilde{\sigma}_{k,1},1),\ldots,\alpha(\widetilde{\sigma}_{k,\mathfrak{a}_{i}},1)\big{)}\cdots\big{(}\alpha(\widetilde{\sigma}_{k,1},c),\ldots,\alpha(\widetilde{\sigma}_{k,\mathfrak{a}_{i}},c)\big{)}\colon\hskip
17.22217pt\\\
\hfill\big{(}\widetilde{\sigma}_{1,1},\ldots,\widetilde{\sigma}_{1,\mathfrak{a}_{i}}\big{)}\cdots\big{(}\widetilde{\sigma}_{k,1},\ldots,\widetilde{\sigma}_{k,\mathfrak{a}_{i}}\big{)}\in\mathcal{L}(D^{\prime}_{i})\Big{\\}}\text{.}$

Let $\mathfrak{A}^{\prime}$ be the $\tau$-structure, with domain
$\mathsf{R}_{0}(\mathfrak{A}^{\prime})=\mathsf{rel}(\mathcal{L}(D^{\prime}_{0}))$,
such that
$\mathsf{R}_{i}(\mathfrak{A}^{\prime})=\mathsf{rel}(\mathcal{L}(D^{\prime}_{i}))$
for each $i\in[l]$. By construction, $\mathfrak{A}^{\prime}$ is
$(\\{0,1\\},0pt^{2}\cdot\lvert\Sigma\rvert^{\max\\{1,\mathfrak{a}_{1},\ldots,\mathfrak{a}_{l}\\}})$-decisional.
Moreover, $\mathfrak{A}^{\prime}$ is isomorphic to $\mathfrak{A}$. Indeed,
note that the permutation
$\pi\colon\mathsf{R}_{0}(\mathfrak{A}^{\prime})\rightarrow\mathsf{R}_{0}(\mathfrak{A})$,
where $\pi(u)=\widetilde{\sigma}_{1}\cdots\widetilde{\sigma}_{k}$ for each
$u=\alpha(\widetilde{\sigma}_{1})\cdots\widetilde{\sigma}(\sigma_{k})\in\mathsf{R}_{0}(\mathfrak{A}^{\prime})$,
is an isomorphism from $\mathfrak{A}^{\prime}$ to $\mathfrak{A}$. ∎

##### The hypercube graph $\mathcal{H}_{k}$.

Let $k\in\mathbb{N}_{+}$. The _$k$ -dimensional hypercube graph_ is the graph
$\mathcal{H}_{k}=(\mathsf{R}_{0}(\mathcal{H}_{k}),\mathsf{R}_{1}(\mathcal{H}_{k}))$
whose vertex set $\mathsf{R}_{0}(\mathcal{H}_{k})=\\{0,1\\}^{k}$ is the set of
all $k$-bit binary strings, and whose edge set
$\mathsf{R}_{1}(\mathcal{H}_{k})$ is the set of all pairs of $k$-bit strings
that differ in exactly one position.

$\mathsf{R}_{1}(\mathcal{H}_{k})=\\{(b_{1}b_{2}\cdots
b_{k},b_{1}^{\prime}b_{2}^{\prime}\cdots b_{k}^{\prime})\;:\;\mbox{There is a
unique $i\in[k]$ such that $b_{i}\neq b^{\prime}_{i}$}\\}.$

Therefore, the $k$-dimensional hypercube is equal to the structure derived
from the structural pair $\mathcal{D}_{k}=(D_{0},D_{1})$, where the ODD
$D_{0}\in\mathcal{B}(\\{0,1\\},2)^{\circ{k}}$ accepts all $k$-bit strings of
length $k$, and $D_{1}\in\mathcal{B}(\\{0,1\\}^{\otimes 2},2)^{\circ{k}}$ is
the ODD that accepts all strings of the form $b_{1}\cdots b_{k}\otimes
b_{1}^{\prime}\cdots b_{k}^{\prime}$ such that $b_{1}\cdots b_{k}$ and
$b_{1}^{\prime}\cdots b_{k}^{\prime}$ differ in exactly one entry. In other
words, we have $\mathcal{H}_{k}=\mathfrak{s}(\mathcal{D}_{k})$. This
structural pair is depicted in Figure 1.

Figure 1: An example of a $(\\{0,1\\},2,\tau)$-structural pair
$\mathcal{D}_{5}=(D_{0},D_{1})$, where $\tau$ is the relational vocabulary of
directed graphs. The ODD $D_{0}$ accepts all binary strings of length $5$. The
odd $D_{1}$ accepts all strings of the form $b_{1}\cdots b_{5}\otimes
b_{1}^{\prime}\cdots
b_{5}^{\prime}=(b_{1},b_{1}^{\prime})\cdots(b_{5},b_{5}^{\prime})$ such that
$b_{1}\cdots b_{5}$ and $b_{1}^{\prime}\cdots b_{5}^{\prime}$ differ in
exactly one bit. The structure derived from $\mathcal{D}_{5}$ is the
$5$-dimensional directed hypercube
$\mathcal{H}_{5}=\mathfrak{s}(\mathcal{D}_{5})$.

###  4.2 Regular-Decisional Classes

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$ and
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary. We
let $\mathcal{R}(\Sigma,0pt,\tau)$ denote the relation constituted by all
$(\Sigma,0pt,\tau)$-structural tuples. Note that the relation
$\mathcal{R}(\Sigma,0pt,\tau)$ is a subset of the following set of tuples of
ODDs

$\bigcup_{k\in\mathbb{N}_{+}}\mathcal{B}(\Sigma,0pt)^{\circ{k}}\times\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{1}},0pt)^{\circ{k}}\times\cdots\times\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{l}},0pt)^{\circ{k}}.$

Since each $(\Sigma,0pt,\tau)$-structural tuple
$\mathcal{D}\in\mathcal{R}(\Sigma,0pt,\tau)$ corresponds to a
$(\Sigma,0pt)$-decisional structure $\mathfrak{s}(\mathcal{D})$, we can
associate with each sub-relation $R\subseteq\mathcal{R}(\Sigma,0pt,\tau)$ a
class $\mathfrak{s}(R)=\left\\{\mathfrak{A}\colon\mathcal{D}\in
R,\mathfrak{s}(\mathcal{D})\simeq\mathfrak{A}\right\\}$ of
$(\Sigma,0pt)$-decisional $\tau$-structures.

######  Definition 3.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$, and $\tau$ be a
relational vocabulary. We say that a class $\mathcal{C}$ of _finite_
$\tau$-structures is _$(\Sigma,0pt)$ -regular-decisional_ if there exists a
regular sub-relation $R\subseteq\mathcal{R}(\Sigma,0pt,\tau)$ such that
$\mathcal{C}=\mathfrak{s}(R)$.

The _$\Sigma$ -regular-decisional width_ of a class $\mathcal{C}$ of finite
$\tau$-structures, denoted by $\omega(\Sigma,\mathcal{C})$, is defined as the
minimum $0pt\in\mathbb{N}_{+}$ such that $\mathcal{C}$ is
$(\Sigma,0pt)$-regular-decisional. We note that this minimum $w$ may not
exist. In this case, we set $\omega(\Sigma,\mathcal{C})=\infty$.

Now, consider the alphabet

$\mathcal{B}(\Sigma,0pt,\tau)\doteq\mathcal{B}(\Sigma,0pt)\otimes\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{1}},0pt)\otimes\cdots\otimes\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{l}},0pt).$
(1)

inline](Up to now it is not known that the set
$\mathcal{B}(\Sigma,0pt,\tau)^{\circledast}$ is regular). We let
$\mathcal{B}(\Sigma,0pt,\tau)^{\circledast}$ be the set of strings
$D_{0}\otimes D_{1}\otimes\ldots\otimes D_{l}$ over
$\mathcal{B}(\Sigma,0pt,\tau)$ such that $(D_{0},D_{1},\ldots,D_{l})$ is a
$(\Sigma,0pt,\tau)$-structural tuple.

Then a class $\mathcal{C}$ of finite $\tau$-structures is
$(\Sigma,0pt)$-regular-decisional if and only if there exists a finite
automaton $\mathcal{F}$ over $\mathcal{B}(\Sigma,0pt,\tau)$ such that
$\mathsf{rel}(\bm{\mathcal{L}}(\mathcal{F}))\subseteq\mathcal{R}(\Sigma,0pt,\tau)$,
and $\mathcal{C}=\mathfrak{s}(\mathsf{rel}(\bm{\mathcal{L}}(\mathcal{F})))$.

######  Definition 4.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\dots,\mathsf{R}_{l})$ be a relational vocabulary and
$\mathcal{C}$ be a $(\Sigma,0pt,\tau)$-regular-decisional class of finite
structures. We say that a finite automaton $\mathcal{F}$ over
$\mathcal{B}(\Sigma,0pt,\tau)$ represents $\mathcal{C}$ if
$\mathsf{rel}(\bm{\mathcal{L}}(\mathcal{F}))\subseteq\mathcal{R}(\Sigma,0pt,\tau)$
and $\mathcal{C}=\mathfrak{s}(\mathsf{rel}(\bm{\mathcal{L}}(\mathcal{F})))$.

###  4.3 The Hypercube Language.

inline]Revisit this paragraph. It is not clear whether we are talking about
equality or isomorphism here. Same thing with definition above.

In order to show that a class $\mathcal{C}$ of finite $\tau$-structures is
$(\Sigma,0pt)$-decisional, it is enough to construct a finite automaton
$\mathcal{F}$ over $\mathcal{B}(\Sigma,0pt,\tau)$ representing $\mathcal{C}$.
More precisely, we need to define such an automaton $\mathcal{F}$ such that
for each $k\in\mathbb{N}$, and each string $D_{0}\otimes
D_{1}\otimes\ldots\otimes D_{l}\in\mathcal{B}(\Sigma,0pt,\tau)^{k}$,
$D_{0}\otimes D_{1}\otimes\ldots\otimes D_{l}$ belongs to
$\bm{\mathcal{L}}(\mathcal{F})$ if and only if
$\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$ is a $(\Sigma,0pt,\tau)$-structural
tuple and $\mathfrak{s}(\mathcal{D})\in\mathcal{C}$.

To illustrate this type of construction, we show in Proposition 5 that the
class $\mathscr{H}$ of hypercubes is $(\\{0,1\\},2)$-regular-decisional. Since
it can be easily shown that this class is not $(\\{0,1\\},1)$-regular-
decisional, we have that the $\\{0,1\\}$-regular-decisional width of
$\mathscr{H}$ is $2$.

######  Proposition 5.

Let $\mathscr{H}\doteq\left\\{\mathcal{H}_{k}\colon
k\in\mathbb{N}_{+}\right\\}$ be the class of all hypercube graphs. The class
$\mathscr{H}$ is $(\\{0,1\\},2)$-regular-decisional.

###### Proof.

In Figure 2 we depict an automaton $\mathcal{F}$ which accepts a string
$D_{0}\otimes D_{1}$ of length $k$ if and only if the pair
$\mathcal{D}_{k}=(D_{0},D_{1})$ is a structural pair whose derived structure
$\mathfrak{s}(\mathcal{D}_{k})$ is the hypercube graph $\mathcal{H}_{k}$. ∎

Figure 2: An automaton $\mathcal{F}$ over the alphabet
$\mathcal{B}(\\{0,1\\},2,\tau)$, where $\tau$ is the vocabulary of directed
graphs. This automaton accepts exactly one string of length $k$ for each
$k\in\mathbb{N}_{+}$. For each such $k$, if $D_{0}\otimes D_{1}$ is the unique
string of length $k$ accepted by $\mathcal{F}$, then the pair
$\mathcal{D}_{k}=(D_{0},D_{1})$ is structural, and
$\mathfrak{s}(\mathcal{D}_{k})$ is the hypercube graph $\mathcal{H}_{k}$. In
particular, the string $D_{0}\otimes D_{1}$ represented in Figure 1 is
accepted by $\mathcal{F}$ upon following the sequence of states
$q_{0}q_{1}q_{1}q_{1}q_{1}q_{2}$.

An interesting aspect of Proposition 5 is that it states that the class
$\mathscr{H}$ of hypercube graphs has regular-decisional width $2$, while this
class has unbounded width with respect to most traditional width measures
studied in structural graph theory. For instance, it can be shown that the
hypercube graph $\mathcal{H}_{k}$ has treewidth $\Theta(2^{k}/\sqrt{k})$ [9]
and cliquewidth $\Omega(2^{k}/\sqrt{k})$ [6]. Therefore, $\mathcal{H}_{k}$ has
also exponential bandwidth, carving width, pathwidth, treedepth and rank-
width. Additionally, since all vertices of $\mathcal{H}_{k}$ have degree $k$,
the degeneracy of the family $\mathscr{H}$ is $\Theta(k)$. Therefore,
$\mathscr{H}$ is not a nowhere dense class of graphs. This also implies that
the graphs in $\mathscr{H}$ have unbounded genus, unbounded local treewidth,
etc.

##  5 First-Order Definable Classes of Structures of Constant Width

For each $\mathrm{FO}\\{\tau\\}$-sentence $\psi$, we let
$\mathcal{R}(\Sigma,0pt,\tau,\psi)$ denote the subset of
$\mathcal{R}(\Sigma,0pt,\tau)$ consisting of all tuples
$\mathcal{D}\in\mathcal{R}(\Sigma,0pt,\tau)$ whose associated structure
$\mathfrak{s}(\mathcal{D})$ satisfies $\psi$.

$\mathcal{R}(\Sigma,0pt,\tau,\psi)\doteq\\{\mathcal{D}\in\mathcal{R}(\Sigma,0pt,\tau)\colon\mathfrak{s}(\mathcal{D})\models\psi\\}\text{.}$

The next theorem (Theorem 6), states that the relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi)$ is regular.

######  Theorem 6.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$, and
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary. For
each $\mathrm{FO}\\{\tau\\}$-sentence $\psi$, the relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi)$ is regular.

A constructive proof of Theorem 6 will be given in Section 6. As a consequence
of Theorem 6, we have that the problem of determining whether a given
$\mathrm{FO}\\{\tau\\}$-sentence $\psi$ is satisfied by some structure
$\mathfrak{A}$ in the class of structures specified by a given finite
automaton $\mathcal{F}$ over the alphabet $\mathcal{B}(\Sigma,0pt,\tau)$ is
fixed-parameter linear in the size of $\mathcal{F}$ when parameterized by
$\tau$, $\psi$, $\Sigma$ and $0pt$ (Theorem 7).

We note that in natural applications, the parameter $\tau$ is often fixed. For
instance, if our goal is to decide properties about classes of directed
graphs, then $\tau$ is simply the vocabulary of directed graphs. Additionally,
often the sentence $\psi$ is fixed, as in the case where the goal is to
determine whether all graphs in a given class of graphs, specified by a finite
automaton $\mathcal{F}$ over the alphabet $\mathcal{B}(\Sigma,0pt,\tau)$, are
triangle-free. Finally, by Proposition 2, the alphabet $\Sigma$ can be assumed
to be the binary alphabet $\\{0,1\\}$, with only a moderate increase in width.
Therefore, in applications where $\tau$, $\psi$ and $\Sigma$ are fixed, the
only relevant parameter is the width parameter $0pt$. This parameter
intuitively is a measure of the complexity of each individual structure in the
class specified by $\mathcal{F}$, while the size of $\mathcal{F}$ is a measure
of the complexity of the class itself.

######  Theorem 7.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\dots,\mathsf{R}_{l})$ be a relational vocabulary, and
$\psi$ be a $\mathrm{FO}\\{\tau\\}$-sentence. Given a finite automaton
$\mathcal{F}$ over the alphabet $\mathcal{B}(\Sigma,0pt,\tau)$ representing a
$(\Sigma,0pt)$-regular-decisional class of $\tau$-structures, one can
determine in time $f(\Sigma,0pt,\tau,\psi)\cdot|\mathcal{F}|$ whether some
$\tau$-structure $\mathfrak{A}\in\mathcal{C}$ satisfies $\psi$, for some
computable function $f$.

###### Proof.

The proof of Theorem 6 shows how to construct an automaton
$\mathcal{F}(\Sigma,0pt,\tau,\psi)$ over the alphabet
$\mathcal{B}(\Sigma,0pt,\tau)$ such that
$\bm{\mathcal{L}}(\mathcal{F}(\Sigma,0pt,\tau,\psi))=\mathsf{lang}(\mathcal{R}(\Sigma,0pt,\tau,\psi))$.
Therefore, there is some $\tau$-structure $\mathfrak{A}\in\mathcal{C}$ that
satisfies $\psi$, if and only if the language
$\bm{\mathcal{L}}(\mathcal{F})\cap\bm{\mathcal{L}}(\mathcal{F}(\Sigma,0pt,\tau,\psi))$
is non-empty. Since this non-emptiness of intersection test can be performed
in time $O(|\mathcal{F}(\Sigma,0pt,\tau,\psi)|\cdot|\mathcal{F}|)$, the
theorem follows by setting
$f(\Sigma,0pt,\tau,\psi)=c\cdot|\mathcal{F}(\Sigma,0pt,\tau,\psi)|+d$ for some
sufficiently large constants $c,d\in\mathbb{N}$. ∎

Let $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary.
We denote by $\mathrm{MSO}\\{\tau\\}$ the set of all monadic second-order
logic formulas over $\tau$, i.e. the extension of $\mathrm{FO}\\{\tau\\}$
that, additionally, allows variables to be used as placeholders for sets of
elements from the domain of a finite $\tau$-structure and allows
quantification over such variables. We note that neither Theorem 6 nor Theorem
7 can be generalized to the logic $\mathrm{MSO}\\{\tau\\}$ for an arbitrary
relational vocabulary $\tau$. Indeed, it is well known that the MSO theory of
unlabeled grids is already undecidable [28, 20] 222Note that the well known
fact that the first-order theory of unlabeled grids is decidable is a special
case of Theorem 7, since unlabeled grids have constant decisional-width. On
the other hand, it is also well known that the first-order theory of labeled
grids is undecidable. Note that labeled grids may have arbitrarily large
decidisonal-width, due to the fact that the ODDs representing the vertices in
each label class may have arbitrarily large width.

Nevertheless, instead of using MSO logic to reason about properties of classes
of $\tau$-structures, we can use MSO logic over the vocabulary of
$\mathcal{B}(\Sigma,0pt,\tau)$-strings to define $(\Sigma,0pt)$-regular-
decisional classes of $\tau$-structures. More precisely, for a given alphabet
$\Gamma$, let $\varrho(\Gamma)$ be the vocabulary of strings over $\Gamma$.
From Büchi-Elgot’s theorem [7, 14], a language $L\subseteq\Gamma^{*}$ is
regular if and only if $L$ can be defined by an
$\mathrm{MSO}\\{\varrho(\Gamma)\\}$-sentence. In particular, a class
$\mathcal{C}$ of finite $\tau$-structures is $(\Sigma,0pt)$-regular decisional
if and only if there is an
$\mathrm{MSO}\\{\varrho(\mathcal{B}(\Sigma,0pt,\tau))\\}$-sentence $\varphi$
such that for each $k\in\mathbb{N}_{+}$, and each string
$\mathbb{S}=D_{0}\otimes D_{1}\otimes\ldots\otimes D_{l}$ in
$\mathcal{B}(\Sigma,0pt,\tau)^{k}$, $\mathbb{S}$ satisfies $\varphi$ if and
only if $\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$ is a
$(\Sigma,0pt,\tau)$-structural tuple and $\mathfrak{s}(\mathcal{D})$ belongs
to $\mathcal{C}$.

######  Theorem 8.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$ and
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary.
Given an $\mathrm{MSO}\\{\varrho(\mathcal{B}(\Sigma,0pt,\tau))\\}$-sentence
$\varphi$ and an $\mathrm{FO}\\{\tau\\}$-sentence $\psi$, one can decide
whether there exists some string $\mathbb{S}=D_{0}\otimes
D_{1}\otimes\ldots\otimes D_{l}\in\mathcal{B}(\Sigma,0pt,\tau)^{\circledast}$
such that $\mathbb{S}\models\varphi$ and
$\mathfrak{s}(\mathcal{D})\models\psi$, where
$\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$.

###### Proof.

By using Büchi-Elgot’s Theorem, one can construct a finite automaton
$\mathcal{F}_{1}$ over $\mathcal{B}(\Sigma,0pt,\tau)$ that accepts a string
$\mathbb{S}\in\mathcal{B}(\Sigma,0pt,\tau)^{+}$ if and only if
$\mathbb{S}\models\varphi$. Now, from Theorem 6, we can construct a finite
automaton $\mathcal{F}_{2}$ over $\mathcal{B}(\Sigma,0pt,\tau)$ which accepts
a string $D_{0}\otimes D_{1}\otimes\ldots\otimes
D_{l}\in\mathcal{B}(\Sigma,0pt,\tau)^{+}$ if and only if
$\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$ is a $(\Sigma,0pt,\tau)$-structural
tuple and $\mathfrak{s}(\mathcal{D})\models\psi$. Let $\mathcal{F}_{\cap}$ be
a finite automaton that accepts the language
$\bm{\mathcal{L}}(\mathcal{F}_{1})\cap\bm{\mathcal{L}}(\mathcal{F}_{2})$.
Then, we have that $\bm{\mathcal{L}}(\mathcal{F}_{\cap})$ is non-empty if and
only if there exists some string $\mathbb{S}=D_{0}\otimes
D_{1}\otimes\ldots\otimes D_{l}\in\mathcal{B}(\Sigma,0pt,\tau)^{\circledast}$
such that $\mathbb{S}\models\varphi$ and
$\mathfrak{s}(\mathcal{D})\models\psi$, where
$\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$. Since emptiness is decidable for
finite automata, the theorem follows. ∎

##  6 Proof of Theorem 6

We dedicate this section to the proof of Theorem 6. The proof follows a
traditional strategy combined with new machinery for the implicit manipulation
of ODDs. More precisely, given an alphabet $\Sigma$, $0pt\in\mathbb{N}_{+}$, a
relational vocabulary $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ and an
$\mathrm{FO}\\{\tau\\}$-formula $\psi(x_{1},\ldots,x_{t})$ with free variables
$\mathrm{freevar}(\psi)\subseteq\,X_{t}=\\{x_{1},\ldots,x_{t}\\}$, we define
$\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t})$ as the relation containing precisely
the tuples of the form $(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})$ such
that $\mathcal{D}=(D_{0},D_{1},\ldots,D_{l})$ is
$(\Sigma,0pt,\tau)$-structural and
$\mathfrak{s}(\mathcal{D})\models\psi[u_{1},\ldots,u_{t}]$. The Boolean
connectives $\wedge,\vee$ and $\neg$ and the existential quantification
$\exists$ are handled using closure properties from regular languages.

The technically involved part of the proof however will be the construction of
an initial automaton which accepts precisely those strings

$D_{0}\otimes D_{1}\otimes\ldots\otimes D_{l}\otimes u_{1}\ldots u_{t}$

such that $(D_{0},D_{1},\ldots,D_{l})$ is a $(\Sigma,0pt,\tau)$-structural
tuple, and $u_{1},\ldots,u_{t}$ belong to the domain $\mathcal{L}(D_{0})$. In
particular, we need to guaranteed that for each $i\in[l]$, the language
$\mathcal{L}(D_{i})$ is contained in the tensored language
$\mathcal{L}(D_{0})^{\otimes\mathfrak{a}_{i}}$.

###  6.1 Basic General Operations

In this section, we introduce some basic low-level operations that will be
used repeatedly in the proof of Theorem 6. More precisely, we consider the
following operations: _projection_ , _identification_ , _permutation of
coordinates_ , _fold_ , _unfold_ , _direct sum_ , _union_ , _intersection_ and
_complementation_.

Let $\Sigma$ be an alphabet, $\mathfrak{a}\in\mathbb{N}_{+}$ and
$R\subseteq(\Sigma^{+})^{{\times}\mathfrak{a}}$ be an $\mathfrak{a}$-ary
relation.

For each permutation $\pi\colon[\mathfrak{a}]\rightarrow[\mathfrak{a}]$, we
let $\mathsf{perm}(R,\pi)$ be the relation obtained from $R$ by permuting the
coordinates of each tuple in $R$ according to $\pi$. In other words,
$\mathsf{perm}(R,\pi)\doteq\left\\{\left(s_{\pi(1)},\ldots,s_{\pi(\mathfrak{a})}\right)\colon\left(s_{1},\ldots,s_{\mathfrak{a}}\right)\in
R\right\\}$.

For each $i\in[\mathfrak{a}]$, the _projection of the $i$-th coordinate of
$R$_ is defined as the $(\mathfrak{a}-1)$-ary relation
$\mathsf{proj}(R,i)\doteq\left\\{\left(s_{1},\dots,s_{i-1},s_{i+1},\dots,s_{\mathfrak{a}}\right)\colon\left(s_{1},\ldots,s_{\mathfrak{a}}\right)\in
R\right\\}\text{}$ obtained from $R$ by removing the $i$-th coordinate of each
tuple in $R$. More generally, for each $J\subseteq[\mathfrak{a}]$, we let
$\mathsf{proj}(R,J)$ denote the relation obtained from $R$ by removing all the
$i$-th coordinates of each tuple in $R$, where $i\in J$.

For each $i,j\in[\mathfrak{a}]$, the _identification of the $i$-th and $j$-th
coordinates of $R$_ is defined as the relation
$\mathsf{ident}(R,i,j)\doteq\\{(s_{1},\ldots,s_{\mathfrak{a}})\in R\colon
s_{i}=s_{j}\\}\text{}$ obtained from $R$ by removing each tuple
$(s_{1},\ldots,s_{\mathfrak{a}})\in R$ such that $s_{i}\neq s_{j}$. More
generally, for each $J\subseteq[\mathfrak{a}]\times[\mathfrak{a}]$, we let
$\mathsf{ident}(R,J)\doteq\\{(s_{1},\ldots,s_{\mathfrak{a}})\in R\colon
s_{i}=s_{j},(i,j)\in J\\}$.

For each $i,j\in[\mathfrak{a}]$, with $i\leq j$, we let

$\mathsf{fold}(R,i,j)\doteq\left\\{\left(s_{1},\ldots,s_{i-1},s_{i}\otimes\cdots\otimes
s_{j},s_{j+1},\ldots,s_{\mathfrak{a}}\right)\colon\left(s_{1},\ldots,s_{\mathfrak{a}}\right)\in
R\right\\}\text{.}$

On the other hand, if $R=\mathsf{fold}(R^{\prime},i,j)$ for some relation
$R^{\prime}$ and some $i,j\in[\mathfrak{a}]$, with $i\leq j$, then we let
$\mathsf{unfold}(R,i)=R^{\prime}$, i.e. the inverse operation of
$\mathsf{fold}$.

Let $\Sigma_{1}$ and $\Sigma_{2}$ be two alphabets,
$\mathfrak{a}_{1},\mathfrak{a}_{2}\in\mathbb{N}_{+}$,
$R_{1}\subseteq(\Sigma_{1}^{+})^{\times\mathfrak{a}_{1}}$ be an
$\mathfrak{a}_{1}$-ary relation and
$R_{2}\subseteq(\Sigma_{2}^{+})^{{\times}\mathfrak{a}_{2}}$ be an
$\mathfrak{a}_{2}$-ary relation. If $R_{1}$ and $R_{2}$ are non-empty, then we
define the _direct sum_ of $R_{1}$ with $R_{2}$ as the
$(\mathfrak{a}_{1}+\mathfrak{a}_{2})$-ary relation

$R_{1}\oplus
R_{2}\doteq\left\\{\left(s_{1},\ldots,s_{\mathfrak{a}_{1}},s^{\prime}_{1},\ldots,s^{\prime}_{\mathfrak{a}_{2}}\right)\colon\left(s_{1},\ldots,s_{\mathfrak{a}_{1}}\right)\in
R_{1},\left(s^{\prime}_{1},\ldots,s^{\prime}_{\mathfrak{a}_{2}}\right)\in
R_{2}\right\\}\text{.}$

Otherwise, we let $R_{1}\oplus\emptyset\doteq R_{1}$ and $\emptyset\oplus
R_{2}\doteq R_{2}$.

######  Proposition 9.

Let $\Sigma_{1}$ and $\Sigma_{2}$ be two alphabets,
$\mathfrak{a}_{1},\mathfrak{a}_{2}\in\mathbb{N}_{+}$,
$R_{1}\subseteq(\Sigma_{1}^{+})^{{\times}\mathfrak{a}_{1}}$ be a regular
$\mathfrak{a}_{1}$-ary relation and
$R_{2}\subseteq(\Sigma_{2}^{+})^{{\times}\mathfrak{a}_{2}}$ be a regular
$\mathfrak{a}_{2}$-ary relation. The following closure properties are held:

  1. 1.

for each permutation
$\pi\colon[\mathfrak{a}_{1}]\rightarrow[\mathfrak{a}_{1}]$,
$\mathsf{perm}(R_{1},\pi)$ is regular;

  2. 2.

for each $J\subseteq[\mathfrak{a}_{1}]$, $\mathsf{proj}(R_{1},J)$ is regular;

  3. 3.

for each $J\subseteq[\mathfrak{a}_{1}]\times[\mathfrak{a}_{1}]$,
$\mathsf{ident}(R_{1},J)$ is regular;

  4. 4.

for each $i,j\in[\mathfrak{a}_{1}]$, with $i\leq j$,
$\mathsf{fold}(R_{1},i,j)$ is regular;

  5. 5.

if $R_{1}=\mathsf{fold}(R^{\prime}_{1},i,j)$ for some relation
$R^{\prime}_{1}$ and some $i,j\in[\mathfrak{a}_{1}]$, with $i\leq j$, then
$\mathsf{unfold}(R_{1},i)=R^{\prime}_{1}$ is regular;

  6. 6.

$R_{1}\oplus R_{2}$ is regular.

###### Proof.

Since $R_{1}$ is a regular relation, there exists a finite automaton
$\mathcal{F}_{1}$ over the alphabet $\Sigma_{1}^{\otimes\mathfrak{a}_{1}}$
such that $\bm{\mathcal{L}}(\mathcal{F}_{1})=\mathsf{lang}(R_{1})$.
Analogously, there exists a finite automaton $\mathcal{F}_{2}$ over the
alphabet $\Sigma_{2}^{\otimes\mathfrak{a}_{2}}$ such that
$\bm{\mathcal{L}}(\mathcal{F}_{2})=\mathsf{lang}(R^{\prime})$.

1. Let $\mathcal{F}_{1}^{\prime}$ be the finite automaton with state set $Q(\mathcal{F}_{1}^{\prime})=Q(\mathcal{F}_{1})$, transition set $T(\mathcal{F}_{1}^{\prime})=\left\\{(q^{\prime},(\widetilde{\sigma}_{\pi(1)},\ldots,\widetilde{\sigma}_{\pi(\mathfrak{a}_{1})}),q)\colon(q^{\prime},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}}),q)\in T(\mathcal{F}_{1})\right\\}\text{,}$ initial state set $I(\mathcal{F}_{1}^{\prime})=I(\mathcal{F}_{1})$, and final state set $F(\mathcal{F}_{1}^{\prime})=F(\mathcal{F}_{1})$. One can verify that $\bm{\mathcal{L}}(\mathcal{F}_{1}^{\prime})=\mathsf{lang}(\mathsf{perm}(R_{1},\pi))$. Therefore, $\mathsf{perm}(R_{1},\pi)$ is regular.

2. For each symbol $(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}})\in(\Sigma_{1}\uplus\\{\square\\})^{\otimes\mathfrak{a}_{1}}$, we let $\mathsf{proj}(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},J)$ denote the symbol in $(\Sigma_{1}\uplus\\{\square\\})^{\otimes(\mathfrak{a}_{1}-\lvert J\rvert)}$ obtained from $(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}})$ by removing each $i$-th coordinate, where $i\in J$. Thus, let $\mathcal{F}_{1}^{\prime}$ be the finite automaton with state set $Q(\mathcal{F}_{1}^{\prime})=Q(\mathcal{F}_{1})$, transition set

$T(\mathcal{F}_{1}^{\prime})=\left\\{(q^{\prime},\mathsf{proj}(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},J),q)\in
T(\mathcal{F}_{1})\colon(q^{\prime},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}}),q)\in
T(\mathcal{F}_{1})\right\\}\text{,}$

initial state set $I(\mathcal{F}_{1}^{\prime})=I(\mathcal{F}_{1})$, and final
state set $F(\mathcal{F}_{1}^{\prime})=F(\mathcal{F}_{1})$. One can verify
that
$\bm{\mathcal{L}}(\mathcal{F}_{1}^{\prime})=\mathsf{lang}(\mathsf{proj}(R_{1},J))$.
Therefore, $\mathsf{proj}(R_{1},J)$ is regular.

3. Let $\mathcal{F}_{1}^{\prime}$ be the finite automaton with state set $Q(\mathcal{F}_{1}^{\prime})=Q(\mathcal{F}_{1})$, transition set $T(\mathcal{F}_{1}^{\prime})=T(\mathcal{F}_{1})\setminus\left\\{(q^{\prime},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}}),q)\in T(\mathcal{F}_{1})\colon\widetilde{\sigma}_{i}\neq\widetilde{\sigma}_{j},(i,j)\in J\right\\}\text{,}$ initial state set $I(\mathcal{F}_{1}^{\prime})=I(\mathcal{F}_{1})$, and final state set $F(\mathcal{F}_{1}^{\prime})=F(\mathcal{F}_{1})$. One can verify that $\bm{\mathcal{L}}(\mathcal{F}_{1}^{\prime})=\mathsf{lang}(\mathsf{ident}(R_{1},J))$. Therefore, $\mathsf{ident}(R_{1},J)$ is regular.

4. Let $\alpha$ be the map that sends each tuple of symbols $(\sigma_{1},...,\sigma_{\mathfrak{a}_{1}})\in\Sigma_{1}^{\mathfrak{a}_{1}}$ to the tuple $(\sigma_{1},...,\sigma_{i-1},(\sigma_{i},...,\sigma_{j}),\sigma_{j+1},...,\sigma_{\mathfrak{a}_{1}})$. For a language $L\subseteq(\Sigma_{1}^{\otimes\mathfrak{a}_{1}})^{+}$, let $\alpha(L)$ be the homomorphic image of $L$ under $\alpha$. Since regular languages are closed under homomorphism, and $\mathsf{fold}(R_{1},i,j)=\mathsf{rel}(\alpha(\mathsf{lang}(R_{1})))$ we have that $\mathsf{fold}(R_{1},i,j)$ is regular.

5. Let $\beta$ be the map that sends each tuple $(\sigma_{1},...,\sigma_{i-1},(\sigma_{i},...,\sigma_{j}),\sigma_{j+1},...,\sigma_{\mathfrak{a}_{1}})$ to the tuple $(\sigma_{1},...,\sigma_{\mathfrak{a}_{1}})\in\Sigma_{1}^{\mathfrak{a}_{1}}$. For a language $L\subseteq\Sigma_{1}^{\otimes_{i-1}}\times(\Sigma_{1}^{\otimes j-i+1})\times\Sigma_{1}^{\otimes\mathfrak{a}_{1}-j+1}$ we let $\beta(L)$ be the homomorphic image of $L$ under $\beta$. Since regular languages are closed under homomorphism, and $\mathsf{unfold}(R_{1},i)=\mathsf{rel}(\beta(\mathsf{lang}(R_{1})))$, we have that $\mathsf{unfold}(R_{1},i)$ is regular.

6. For each $i\in[2]$, let $\mathcal{F}_{i}^{\prime}$ be the finite automaton with state set $Q(\mathcal{F}_{i}^{\prime})=Q(\mathcal{F}_{i})$, transition set $T(\mathcal{F}_{i}^{\prime})=T(\mathcal{F}_{i})\cup\\{(q,\square^{\times\mathfrak{a}_{i}},q)\colon q\in F(\mathcal{F}_{i})\\}\text{,}$ initial state set $I(\mathcal{F}_{i}^{\prime})=I(\mathcal{F}_{i})$ and final state set $F(\mathcal{F}_{i}^{\prime})=F(\mathcal{F}_{i})$. Now, consider the finite automaton $\mathcal{F}^{\prime}$ with state set $Q(\mathcal{F}^{\prime})=Q(\mathcal{F}_{1}^{\prime})\times Q(\mathcal{F}_{2}^{\prime})$, transition set

$\begin{multlined}T(\mathcal{F}^{\prime})=\Big{\\{}\left((q^{\prime}_{1},q^{\prime}_{2}),(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}}),(q_{1},q_{2})\right)\colon\\\\[4.30554pt]
\hfil\left(q^{\prime}_{1},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}}),q_{1}\right)\in
T(\mathcal{F}_{1}^{\prime}),\left(q^{\prime}_{2},(\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}}),q_{2}\right)\in
T(\mathcal{F}_{2}^{\prime})\\\
\hfil(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}})\neq\square^{\times(\mathfrak{a}_{1}+\mathfrak{a}_{2})}\Big{\\}}\text{,}\end{multlined}T(\mathcal{F}^{\prime})=\Big{\\{}\left((q^{\prime}_{1},q^{\prime}_{2}),(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}}),(q_{1},q_{2})\right)\colon\\\\[4.30554pt]
\hfil\left(q^{\prime}_{1},(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}}),q_{1}\right)\in
T(\mathcal{F}_{1}^{\prime}),\left(q^{\prime}_{2},(\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}}),q_{2}\right)\in
T(\mathcal{F}_{2}^{\prime})\\\
\hfil(\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{\mathfrak{a}_{1}},\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{\mathfrak{a}_{2}})\neq\square^{\times(\mathfrak{a}_{1}+\mathfrak{a}_{2})}\Big{\\}}\text{,}$

initial state set $I(\mathcal{F}^{\prime})=I(\mathcal{F}_{1}^{\prime})\times
I(\mathcal{F}_{2}^{\prime})$ and final state set
$F(\mathcal{F}^{\prime})=F(\mathcal{F}_{1}^{\prime})\times
F(\mathcal{F}_{2}^{\prime})$. One can verify that
$\bm{\mathcal{L}}(\mathcal{F}^{\prime})=\mathsf{lang}(R_{1}\oplus
R^{\prime})$. Therefore, $R_{1}\oplus R^{\prime}$ is regular. ∎

Besides the operations described above, it is worth noting that, if $R_{1}$
and $R_{2}$ have the same arity, i.e. $\mathfrak{a}_{1}=\mathfrak{a}_{2}$,
then the _union_ $R_{1}\cup R_{2}$ and the _intersection_ $R_{1}\cap R_{2}$ of
$R_{1}$ and $R_{2}$ are regular relations. Moreover, if
$R\subseteq(\Sigma^{+})^{{\times}\mathfrak{a}}$ is a regular
$\mathfrak{a}$-ary relation, then the complement $\neg
R\doteq(\Sigma^{+})^{{\times}\mathfrak{a}}\setminus R$ of $R$ is also a
regular $\mathfrak{a}$-ary relation.

###  6.2 Core Relations

In this subsection we introduce some non-standard relations and prove that
these relations are regular. Intuitively, these relations will be used to
implicitly manipulate tuples of ODDs, and in particular to construct a finite
automaton accepting a string $D_{0}\otimes D_{1}\otimes\ldots\otimes
D_{l}\otimes u_{1}\ldots u_{t}$ if and only if the tuple
$(D_{0},D_{1},\ldots,D_{l})$ is $(\Sigma,0pt,\tau)$-structural and
$u_{1},\ldots,u_{t}$ belong to the domain $\mathcal{L}(D_{0})$.

######  Proposition 10.

For each alphabet $\Sigma$ and each $0pt\in\mathbb{N}_{+}$, the language
$\mathcal{B}(\Sigma,0pt)^{\circledast}$ is regular.

###### Proof.

Consider the finite automaton $\mathcal{F}$ over the alphabet
$\mathcal{B}(\Sigma,0pt)$ with state set
$Q(\mathcal{F})=\left\\{q_{I}\right\\}\cup\\{q_{B}\colon
B\in\mathcal{B}(\Sigma,0pt)\\}$, transition set

$\displaystyle T(\mathcal{F})=$ $\displaystyle\left\\{(q_{I},B,q_{B})\colon
B\in\mathcal{B}(\Sigma,0pt),\iota(B)=1\right\\}$ $\displaystyle\cup$
$\displaystyle\\{(q_{B^{\prime}},B,q_{B})\colon
B,B^{\prime}\in\mathcal{B}(\Sigma,0pt),\,\ell(B)=r(B^{\prime}),\phi(B^{\prime})=0,\iota(B)=0\\}\text{,}$

initial state set $I(\mathcal{F})=\\{q_{I}\\}$ and final state set
$F(\mathcal{F})=\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}q_{B}\in
Q(\mathcal{F})}\colon\phi(B)=1\right\\}$. One can verify that
$\bm{\mathcal{L}}(\mathcal{F})=\mathcal{B}(\Sigma,0pt)^{\circledast}$.
Therefore, $\mathcal{B}(\Sigma,0pt)^{\circledast}$ is regular. ∎

Let $\Sigma$ be an alphabet and $0pt\in\mathbb{N}_{+}$. We let
$\mathcal{R}_{\in}(\Sigma,0pt)$ be the relation defined as follows:

$\mathcal{R}_{\in}(\Sigma,0pt)\doteq\big{\\{}(D,s)\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},s\in\mathcal{L}(D)\big{\\}}\text{.}$

######  Proposition 11.

For each alphabet $\Sigma$ and each $0pt\in\mathbb{N}_{+}$, the relation
$\mathcal{R}_{\in}(\Sigma,0pt)$ is regular.

###### Proof.

Consider the finite automaton $\mathcal{F}$ over the alphabet
$\mathcal{B}(\Sigma,0pt)\otimes(\Sigma\uplus\\{\square\\})$ defined as
follows.

  * •

$Q(\mathcal{F})=\left\\{q_{I}\right\\}\cup\\{q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}\colon
B\in\mathcal{B}(\Sigma,0pt),(\mathfrak{p},\widetilde{\sigma},\mathfrak{q})\in
T(B)\\}$;

  * •

$\begin{aligned}
T(\mathcal{F})=&\left\\{({q_{I},(B,\widetilde{\sigma}),q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}})\colon
q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}\in
Q(\mathcal{F})\setminus\\{q_{I}\\},\mathfrak{p}\in I(B)\right\\}\\\
\cup&\begin{multlined}\Big{\\{}(q_{B^{\prime},{[\mathfrak{p}^{\prime},\widetilde{\nu},\mathfrak{q}^{\prime}]}},(B,\widetilde{\sigma}),q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}})\colon
q_{B^{\prime},{[\mathfrak{p}^{\prime},\widetilde{\nu},\mathfrak{q}^{\prime}]}},\,q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}\in
Q(\mathcal{F})\setminus\\{q_{I}\\},\\\
\ell(B)=r(B^{\prime}),\phi(B^{\prime})=0,\iota(B)=0,\mathfrak{p}=\mathfrak{q}^{\prime}\Big{\\}}\text{;}\end{multlined}\Big{\\{}(q_{B^{\prime},{[\mathfrak{p}^{\prime},\widetilde{\nu},\mathfrak{q}^{\prime}]}},(B,\widetilde{\sigma}),q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}})\colon
q_{B^{\prime},{[\mathfrak{p}^{\prime},\widetilde{\nu},\mathfrak{q}^{\prime}]}},\,q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}\in
Q(\mathcal{F})\setminus\\{q_{I}\\},\\\
\ell(B)=r(B^{\prime}),\phi(B^{\prime})=0,\iota(B)=0,\mathfrak{p}=\mathfrak{q}^{\prime}\Big{\\}}\text{;}\end{aligned}$

  * •

$I(\mathcal{F})=\\{q_{I}\\}$;
$F(\mathcal{F})=\left\\{q_{B,{[\mathfrak{p},\widetilde{\sigma},\mathfrak{q}]}}\in
Q(\mathcal{F})\setminus\\{q_{I}\\}\colon\mathfrak{q}\in F(B)\right\\}$.

One can verify that $\bm{\mathcal{L}}(\mathcal{F})=\left\\{D\otimes s\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},s\in\mathcal{L}(D)\right\\}$. In
other words,
$\mathsf{rel}(\bm{\mathcal{L}}(\mathcal{F}))=\mathcal{R}_{\in}(\Sigma,0pt)$.
Therefore, $\mathcal{R}_{\in}(\Sigma,0pt)$ is a regular relation. ∎

######  Lemma 12.

For each alphabet $\Sigma$ and each $0pt,c\in\mathbb{N}_{+}$, the following
relations are regular:

  1. 1.

$\begin{multlined}\textstyle\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)\doteq\big{\\{}(D,s_{1},\ldots,s_{c})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},\,s_{1},\ldots,s_{c}\in\mathcal{L}(D)\big{\\}}\text{;}\end{multlined}\textstyle\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)\doteq\big{\\{}(D,s_{1},\ldots,s_{c})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},\,s_{1},\ldots,s_{c}\in\mathcal{L}(D)\big{\\}}\text{;}$

  2. 2.

$\begin{multlined}\textstyle\widetilde{\mathcal{R}}(\Sigma,0pt,c)\doteq\\{(D,s_{1},\ldots,s_{c})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}},\,s_{1},\ldots,s_{c}\in\Sigma^{\leq
k},k\in\mathbb{N}_{+}\\}\text{;}\end{multlined}\textstyle\widetilde{\mathcal{R}}(\Sigma,0pt,c)\doteq\\{(D,s_{1},\ldots,s_{c})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}},\,s_{1},\ldots,s_{c}\in\Sigma^{\leq
k},k\in\mathbb{N}_{+}\\}\text{;}$

  3. 3.

$\begin{multlined}\textstyle\widetilde{\mathcal{R}}_{\not\in}(\Sigma,0pt,c)\doteq\big{\\{}\left(D,s_{1},\ldots,s_{c}\right)\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}},\,s_{1},\ldots,s_{c}\in\Sigma^{\leq
k},\\\ \hfill\textstyle s_{i}\not\in\mathcal{L}(D)\text{ for some
}i\in[c],\,k\in\mathbb{N}_{+}\big{\\}}\text{.}\end{multlined}\textstyle\widetilde{\mathcal{R}}_{\not\in}(\Sigma,0pt,c)\doteq\big{\\{}\left(D,s_{1},\ldots,s_{c}\right)\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}},\,s_{1},\ldots,s_{c}\in\Sigma^{\leq
k},\\\ \hfill\textstyle s_{i}\not\in\mathcal{L}(D)\text{ for some
}i\in[c],\,k\in\mathbb{N}_{+}\big{\\}}\text{.}$

###### Proof.

1. First, we prove that $\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)$ is regular. Consider the relation $R$ defined as follows:

$R=\mathsf{ident}\big{(}\overbrace{\mathcal{R}_{\in}(\Sigma,0pt)\oplus\cdots\oplus\mathcal{R}_{\in}(\Sigma,0pt)}^{c\text{
times
}},\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(2i+1,2i+3)\colon
i\in\llbracket c-1\rrbracket}\\}\big{)}\text{.}$

In other words, $R$ consists of all tuples
$\left(D,s_{1},\ldots,D,s_{c}\right)$ such that
$D\in\mathcal{B}(\Sigma,0pt)^{\circledast}$ and
$s_{1},\ldots,s_{c}\in\mathcal{L}(D)$. Therefore,
$\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)$ is regular, since it may be
defined as the regular relation $\mathsf{proj}(R,\\{2i+1\colon i\in[c-1]\\})$.

2. Consider the finite automaton $\mathcal{F}$ over the alphabet $\mathcal{B}(\Sigma,0pt)\otimes(\Sigma\uplus\\{\square\\})^{\otimes c}$ defined as follows:

  * •

$Q(\mathcal{F})=\left\\{q_{I}\right\\}\cup\left\\{q_{B,{[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}]}}\colon
B\in\mathcal{B}(\Sigma,0pt),\,\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}\in\Sigma\uplus\\{\square\\}\right\\}$;

  * •

$\begin{aligned}
T(\mathcal{F})=&\begin{multlined}\Big{\\{}\left(q_{I},(B,\sigma_{1},\ldots,\sigma_{c}),q_{B,[\sigma_{1},\ldots,\sigma_{c}]}\right)\colon
B\in\mathcal{B}(\Sigma,0pt),\iota(B)=1,\,\\\\[-6.45831pt]
\hfill\sigma_{1},\ldots,\sigma_{c}\in\Sigma\Big{\\}}\end{multlined}\Big{\\{}\left(q_{I},(B,\sigma_{1},\ldots,\sigma_{c}),q_{B,[\sigma_{1},\ldots,\sigma_{c}]}\right)\colon
B\in\mathcal{B}(\Sigma,0pt),\iota(B)=1,\,\\\\[-6.45831pt]
\hfill\sigma_{1},\ldots,\sigma_{c}\in\Sigma\Big{\\}}\\\
\cup&\begin{multlined}\Big{\\{}(q_{B^{\prime},[\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{c}]},(B,\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}),q_{B,{[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}]}})\colon
B,B^{\prime}\in\mathcal{B}(\Sigma,0pt),\\\\[2.15277pt]
\hfill\ell(B)=r(B^{\prime}),\phi(B^{\prime})=0,\iota(B)=0,\,\widetilde{\nu}_{i},\widetilde{\sigma}_{i}\in\Sigma\uplus\\{\square\\},\hskip
17.22217pt\\\\[-4.30554pt]
\hfill{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\widetilde{\nu}_{i}=\square\Rightarrow\widetilde{\sigma}_{i}=\square)\text{
for each
}i\in[c]}\Big{\\}}\text{;}\end{multlined}\Big{\\{}(q_{B^{\prime},[\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{c}]},(B,\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}),q_{B,{[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}]}})\colon
B,B^{\prime}\in\mathcal{B}(\Sigma,0pt),\\\\[2.15277pt]
\hfill\ell(B)=r(B^{\prime}),\phi(B^{\prime})=0,\iota(B)=0,\,\widetilde{\nu}_{i},\widetilde{\sigma}_{i}\in\Sigma\uplus\\{\square\\},\hskip
17.22217pt\\\\[-4.30554pt]
\hfill{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\widetilde{\nu}_{i}=\square\Rightarrow\widetilde{\sigma}_{i}=\square)\text{
for each }i\in[c]}\Big{\\}}\text{;}\end{aligned}$

  * •

$I(\mathcal{F})=\\{q_{I}\\}$;
$F(\mathcal{F})=\left\\{q_{B,{[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{c}]}}\in
Q(\mathcal{F})\setminus\\{q_{I}\\}\colon\phi(B)=1\right\\}$.

One can verify that

$\bm{\mathcal{L}}(\mathcal{F})=\left\\{D\otimes(s_{1}\otimes\cdots\otimes
s_{c})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}},\,s_{1},\ldots,s_{c}\in\Sigma^{\leq
k},k\in\mathbb{N}_{+}\right\\}\text{.}$

Therefore, $\widetilde{\mathcal{R}}(\Sigma,0pt,c)$ is a regular relation.

3. Note that, $\widetilde{\mathcal{R}}_{\not\in}(\Sigma,0pt,c)$ consists of all tuples $\left(D,s_{1},\ldots,s_{c}\right)\in\widetilde{\mathcal{R}}(\Sigma,0pt,k)$ such that $s_{i}\not\in\mathcal{L}(D)$ for some $i\in[c]$. Therefore, $\widetilde{\mathcal{R}}_{\not\in}(\Sigma,0pt,c)$ may be defined as the regular relation $\widetilde{\mathcal{R}}(\Sigma,0pt,c)\setminus\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)=\widetilde{\mathcal{R}}(\Sigma,0pt,c)\cap\neg\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,c)$. ∎

######  Lemma 13.

For each two alphabets $\Sigma_{1}$ and $\Sigma_{2}$ and each
$0pt\in\mathbb{N}_{+}$, the relation
$\mathcal{R}(\Sigma_{1},\Sigma_{2},0pt)\doteq\left\\{\left(D,D^{\prime}\right)\colon
D\in\mathcal{B}(\Sigma_{1},0pt)^{\circledast},\,D^{\prime}\in\mathcal{B}(\Sigma_{2},0pt)^{\circledast}\right\\}$
is regular.

###### Proof.

It follows from Proposition 10 that
$\mathcal{B}(\Sigma_{1},0pt)^{\circledast}$ and
$\mathcal{B}(\Sigma_{2},0pt)^{\circledast}$ are regular languages. In other
words, $R_{1}=\mathcal{B}(\Sigma_{1},0pt)^{\circledast}$ and
$R_{2}=\mathcal{B}(\Sigma_{2},0pt)^{\circledast}$ are regular unary relations.
Therefore, $\mathcal{R}(\Sigma_{1},\Sigma_{2},0pt)$ is regular, since it may
be defined as the regular relation $R_{1}\oplus R_{2}$. ∎

Let $\Sigma$ be an alphabet and $0pt,\mathfrak{a}\in\mathbb{N}_{+}$. We let
$\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a})$ be the relation defined as
follows:

$\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a})\doteq\big{\\{}\left(D,D^{\prime}\right)\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},\,D^{\prime}\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}},0pt)^{\circledast},\,\mathcal{L}(D^{\prime})\subseteq\mathcal{L}(D)^{\otimes\mathfrak{a}}\big{\\}}\text{.}$

######  Proposition 14.

For each alphabet $\Sigma$ and each $0pt,\mathfrak{a}\in\mathbb{N}_{+}$, the
relation $\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a})$ is regular.

###### Proof.

Consider the relation
$R=\mathsf{fold}(\widetilde{\mathcal{R}}_{\not\in}(\Sigma,0pt,\mathfrak{a}),2,\mathfrak{a}+1)\oplus\mathcal{R}_{\in}(\Sigma^{\otimes\mathfrak{a}},0pt)$.
Note that, $R$ consists of all tuples of the form
$\left(D,s_{1}\otimes\cdots\otimes
s_{\mathfrak{a}},D^{\prime},s^{\prime}_{1}\otimes\cdots\otimes
s^{\prime}_{\mathfrak{a}}\right)$ satisfying the following conditions:

  * •

$D\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}$,
$s_{1},\ldots,s_{\mathfrak{a}}\in\Sigma^{\leq k}$ but, for some
$i\in[\mathfrak{a}]$, $s_{i}\not\in\mathcal{L}(D)$;

  * •

$D^{\prime}\in\mathcal{B}(\Sigma,0pt)^{\circ{k^{\prime}}}$, and
$s^{\prime}_{1}\otimes\cdots\otimes
s^{\prime}_{\mathfrak{a}}\in\mathcal{L}(D^{\prime})$,

where $k,k^{\prime}\in\mathbb{N}_{+}$. Let $R^{\prime}=\mathsf{ident}(R,2,4)$.
By definition, $R^{\prime}$ is the sub-relation of $R$ comprising all tuples
$(D,s_{1}\otimes\cdots\otimes
s_{\mathfrak{a}},D^{\prime},s^{\prime}_{1}\otimes\cdots\otimes
s^{\prime}_{\mathfrak{a}})\in R$ such that $s_{i}=s^{\prime}_{i}$ for each
$i\in[\mathfrak{a}]$. Thus, $\mathsf{proj}(R^{\prime},\\{2,4\\})$ consists of
all tuples
$\left(D,D^{\prime}\right)\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}\times\mathcal{B}(\Sigma^{\otimes\mathfrak{a}},0pt)^{\circ{k^{\prime}}}$
such that there exist $s_{1},\ldots,s_{\mathfrak{a}}\in\Sigma^{\leq k}$ with
$s_{1}\otimes\cdots\otimes s_{\mathfrak{a}}\in\mathcal{L}(D^{\prime})$ but,
for some $i\in[\mathfrak{a}]$, $s_{i}\not\in\mathcal{L}(D)$, where
$k,k^{\prime}\in\mathbb{N}_{+}$. In other words, we have that

$\mathsf{proj}(R^{\prime},\\{2,4\\})=\big{\\{}\left(D,D^{\prime}\right)\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},D^{\prime}\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}},0pt)^{\circledast},\mathcal{L}(D^{\prime})\nsubseteq\mathcal{L}(D)^{\otimes\mathfrak{a}}\big{\\}}\text{,}$

Now, let
$\mathcal{R}(\Sigma,\Sigma^{\otimes\mathfrak{a}},0pt)=\\{(D,D^{\prime})\colon
D\in\mathcal{B}(\Sigma,0pt)^{\circledast},\,D^{\prime}\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}},0pt)^{\circledast}\\}$.
From Lemma 13, $\mathcal{R}(\Sigma,\Sigma^{\otimes\mathfrak{a}},0pt)$ is
regular. Therefore, $\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a})$ is
regular, since it may be simply regarded as the relation
$\mathcal{R}(\Sigma,\Sigma^{\otimes\mathfrak{a}},0pt)\cap\neg\mathsf{proj}(R^{\prime},\\{2,4\\})$.
∎

###  6.3 Regular-Structural Relations

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary and
$t\in\mathbb{N}$. We let $\mathcal{R}(\Sigma,0pt,\tau,t)$ be the relation
defined as follows:

$\begin{multlined}\textstyle\mathcal{R}(\Sigma,0pt,\tau,t)\doteq\big{\\{}(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})\colon\\\
\left(D_{0},D_{1},\ldots,D_{l}\right)\in\mathcal{R}(\Sigma,0pt,\tau),\,u_{1},\ldots,u_{t}\in\mathcal{L}(D_{0})\big{\\}}\text{.}\end{multlined}\textstyle\mathcal{R}(\Sigma,0pt,\tau,t)\doteq\big{\\{}(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})\colon\\\
\left(D_{0},D_{1},\ldots,D_{l}\right)\in\mathcal{R}(\Sigma,0pt,\tau),\,u_{1},\ldots,u_{t}\in\mathcal{L}(D_{0})\big{\\}}\text{.}$

In particular, note that, if $t=0$, then
$\mathcal{R}(\Sigma,0pt,\tau,t)=\mathcal{R}(\Sigma,0pt,\tau)$.

######  Lemma 15.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary and
$t\in\mathbb{N}$. The relation $\mathcal{R}(\Sigma,0pt,\tau,t)$ is regular.

###### Proof.

Consider the relations
$R=\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a}_{1})\oplus\cdots\oplus\mathcal{R}_{\subseteq}(\Sigma,0pt,\mathfrak{a}_{l})\oplus\widetilde{\mathcal{R}}_{\in}(\Sigma,0pt,t)$
and $R^{\prime}=\mathsf{ident}(R,\\{(2i+1,2i+3)\colon i\in\llbracket
l\rrbracket\\})$. One can verify that $R^{\prime}$ consists of tuples of the
form $(D_{0},D_{1},\ldots,D_{0},D_{l},D_{0},u_{1},\ldots,u_{t})$ satisfying
the conditions:
$\left(D_{0},D_{1},\ldots,D_{l}\right)\in\mathcal{R}(\Sigma,0pt,\tau)$ and
$u_{1},\ldots,u_{t}\in\mathcal{L}(D_{0})$. Therefore,
$\mathcal{R}(\Sigma,0pt,\tau,t)$ is regular, since it may regarded as the
relation $\mathsf{proj}(R^{\prime},\\{2i+1\colon i\in[l]\\})$. ∎

Let $\Sigma$ be a finite alphabet, $0pt\in\mathbb{N}_{+}$, $\tau$ be a
relational vocabulary, and $\psi(x_{1},\ldots,x_{t})$ be an
$\mathrm{FO}\\{\tau\\}$-formula, with free variables $x_{1},\dots,x_{t}$.
Consider the following relation.

$\begin{multlined}\textstyle\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))\doteq\big{\\{}(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})\in\mathcal{R}(\Sigma,0pt,\tau,t)\colon\\\
\mathfrak{s}(D_{0},D_{1},\ldots,D_{l})\models\psi[u_{1},\ldots,u_{t}]\\}\text{.}\end{multlined}\textstyle\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))\doteq\big{\\{}(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})\in\mathcal{R}(\Sigma,0pt,\tau,t)\colon\\\
\mathfrak{s}(D_{0},D_{1},\ldots,D_{l})\models\psi[u_{1},\ldots,u_{t}]\\}\text{.}$

In Theorem 16, we show that
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is a regular relation.
We remark that if $t=0$, then $\psi$ is an $\mathrm{FO}\\{\tau\\}$-sentence
and, in this case, the relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ coincides with the
relation $\mathcal{R}(\Sigma,0pt,\tau,\psi)$. Therefore, Theorem 16 implies
Theorem 6.

The proof of Theorem 16 is by induction on the structure of the input formula
$\psi(x_{1},\ldots,x_{t})$. The base case follows by combining the auxiliary
lemmas and propositions proven in this section. The induction step follows
from the fact that regular languages are closed under, negation, union,
intersection and projection.

######  Theorem 16.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary and
$\psi(x_{1},\ldots,x_{t})$ be an $\mathrm{FO}\\{\tau\\}$-formula. The relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is regular.

###### Proof.

We prove by induction on the structure of the formula
$\psi(x_{1},\ldots,x_{t})$ that the relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is regular.

Base case. Suppose that $\psi(x_{1},\ldots,x_{t})$ is an atomic formula. Then,
there are two subcases to be analyzed. In the first subcase,
$\psi(x_{1},\ldots,x_{t})\equiv(x_{i}=x_{j})$ for some $i,j\in[t]$. In this
case, one can verify that $\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t})$ is equal
to the relation
$\mathsf{ident}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathcal{R}(\Sigma,0pt,\tau,t)},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}l+i+1,l+j+1})$
which consists of the subset of tuples in $\mathcal{R}(\Sigma,0pt,\tau,t)$
where the coordinate corresponding to variable $x_{i}$ is equal to the
coordinate corresponding to variable $x_{j}$. We note that we need to add
$l+1$ to $i$ and $j$ because the first $l+1$ coordinates of each tuple in
$\mathcal{R}(\Sigma,0pt,\tau,t)$ are ODDs, while the last $t$ coordinates are
strings representing assignments to the variables.

In the second subcase,
$\psi(x_{1},\ldots,x_{t})\equiv\mathsf{R}_{i}(x_{\beta(1)},\ldots,x_{\beta(\mathfrak{a}_{i})})$
for some $\beta\colon[\mathfrak{a}_{i}]\rightarrow[t]$ and some $i\in[l]$. Let
$R=\mathsf{unfold}(\mathcal{R}_{\in}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt),2)$.
Intuitively, $R$ consists of all tuples of the form
$(D,v_{1},\ldots,v_{\mathfrak{a}_{i}})$ such that
$D\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt)^{\circ{k}}$ and
$v_{1}\otimes\cdots\otimes v_{\mathfrak{a}_{i}}\in\mathcal{L}(D)$. Let
$R^{\prime}=\mathsf{ident}(R\oplus{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathcal{R}(\Sigma,0pt,\tau,t)},1,i+\mathfrak{a}_{i}+2)$.
One can verify that $R^{\prime}$ comprises all tuples of the form
$(D_{i},v_{1},\ldots,v_{\mathfrak{a}_{i}},D_{0},D_{1},\ldots,D_{i},\ldots,D_{l},u_{1},\ldots,u_{t})$
such that
$(D_{0},D_{1},\ldots,D_{l},u_{1},\ldots,u_{t})\in{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathcal{R}(\Sigma,0pt,\tau,t)}$
and $v_{1}\otimes\cdots\otimes v_{\mathfrak{a}_{i}}\in\mathcal{L}(D_{i})$. Let
$R^{\prime\prime}=\mathsf{ident}(R^{\prime},\\{(j+1,\beta(j)+\mathfrak{a}_{i}+l+2)\colon
j\in[\mathfrak{a}_{i}]\\})$. In other words, $R^{\prime\prime}$ consists of
all tuples
$(D_{i},v_{1},\ldots,v_{\mathfrak{a}_{i}},D_{0},D_{1},\ldots,D_{i},\ldots,D_{l},u_{1},\ldots,u_{t})\in
R^{\prime}$ such that $v_{j}=u_{\beta(j)}$ for each $j\in[\mathfrak{a}_{i}]$,
which implies $u_{\beta(1)}\otimes\cdots\otimes
u_{\beta(\mathfrak{a}_{i})}\in\mathcal{L}(D_{i})$. As a result, we obtain the
regularity of $\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t})$, since in this case
$\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t})$ can be defined as the relation
$\mathsf{proj}(R^{\prime\prime},\\{1,\ldots,\mathfrak{a}_{i}+1\\})$.

Inductive step. It suffices to analyze the following four subcases:
$\psi\equiv\psi_{1}\lor\psi_{2}$, $\psi\equiv\psi_{1}\land\psi_{2}$,
$\psi\equiv\neg\psi_{1}$ and
$\psi(x_{1},\ldots,x_{t})\equiv\exists\,y\;\psi_{3}(x_{1},\ldots,x_{t},y)$ for
$\mathrm{FO}\\{\tau\\}$-formulas $\psi_{1}$, $\psi_{2}$ and $\psi_{3}$ and
variable $y$ that is free in $\psi_{3}$.

First, assume that $\psi\equiv\psi_{1}\lor\psi_{2}$. By the induction
hypothesis, $\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))$ and
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{2},\psi(x_{1},\dots,x_{t}))$ are regular
relations. This implies that
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is a regular relation,
since it is equal to the union

$\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))\cup\mathcal{R}(\Sigma,0pt,\tau,\psi_{2}(x_{1},\dots,x_{t}))$

of two regular relations. Similarly, assume that
$\psi\equiv\psi_{1}\land\psi_{2}$. By the induction hypothesis, the relations
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))$ and
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{2}(x_{1},\dots,x_{t}))$ are regular. Then
$\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t})$ is a regular relation,
since it is equal to the intersection

$\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))\cap\mathcal{R}(\Sigma,0pt,\tau,\psi_{2}(x_{1},\dots,x_{t}))$

of two regular relations.

Now, assume that $\psi\equiv\neg\psi_{1}$. By the induction hypothesis, we
have that the relation
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))$ is regular.
Therefore, $\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is regular,
since it is equal to the Boolean combination
$\neg\mathcal{R}(\Sigma,0pt,\tau,\psi_{1}(x_{1},\dots,x_{t}))\cap{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathcal{R}(\Sigma,0pt,\tau,t)}$
of two regular relations.

Finally, assume that $\psi(x_{1},\ldots,x_{t})\equiv\exists
y\;\psi_{3}(x_{1},\ldots,x_{t},y)$ for some variable $y$ that is free in
$\psi_{3}$. By the induction hypothesis,
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{3}(x_{1},\dots,x_{t},y))$ is a regular
relation. Therefore, $\mathcal{R}(\Sigma,0pt,\tau,\psi(x_{1},\dots,x_{t}))$ is
regular, since it can be obtained from
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{3}(x_{1},\dots,x_{t},y))$ by deleting the
coordinate corresponding to $y$ from each tuple in
$\mathcal{R}(\Sigma,0pt,\tau,\psi_{3}(x_{1},\dots,x_{t},y))$. In other words,
$\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t})=\mathsf{proj}(\mathcal{R}(\Sigma,0pt,\tau,\psi_{3}(x_{1},\dots,x_{t},y)),l+t+2)$.
∎

##  7 Counting Satisfying Assignments

Let $\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary,
$\psi(x_{1},\ldots,x_{t})$ be an $\mathrm{FO}\\{\tau\\}$-formula with
$\mathrm{freevar}(\psi)\subseteq\\{x_{1},\ldots,x_{t}\\}$, and let
$\mathfrak{A}$ be a finite $\tau$-structure. We say that an assignment
$(u_{1},\ldots,u_{t})\in\mathsf{R}_{0}(\mathfrak{A})^{t}$ of the variables
$(x_{1},\ldots,x_{t})$ _satisfies $\psi$ with respect to $\mathfrak{A}$_ if
$\mathfrak{A}\models\psi[u_{1},\ldots,u_{t}]$.

The next theorem states that given a $(\Sigma,0pt,\tau)$-structural tuple
$\mathcal{D}$ such that $\mathfrak{s}(\mathcal{D})=\mathfrak{A}$, the problem
of counting the number of satisfying assignments of $\psi$ with respect to
$\mathfrak{A}$ is fixed parameter tractable when parameterized by $\Sigma$,
$0pt$, $\tau$, $\psi$ and $t$. More specifically, such a problem can be solved
in time quadratic in the length of the $(\Sigma,0pt,\tau)$-structural tuple
$\mathcal{D}$. We remark that, in most applications, the parameters
$\Sigma,\tau,\psi,t$ are naturally already fixed, and therefore the only
complexity parameter that is indeed relevant in these situations is the width
$0pt$.

######  Theorem 17.

Let $\Sigma$ be an alphabet, $0pt\in\mathbb{N}_{+}$,
$\tau=(\mathsf{R}_{1},\ldots,\mathsf{R}_{l})$ be a relational vocabulary and
$\psi(x_{1},\ldots,x_{t})$ be an $\mathrm{FO}\\{\tau\\}$-formula. Given a
$(\Sigma,0pt,\tau)$-structural tuple $\mathcal{D}=(D_{0},D_{1}\ldots D_{l})$
of length $k$, one can count in time $f(\Sigma,0pt,\tau,\psi,t)\cdot k^{2}$,
for some computable function $f$, the number of satisfying assignments for
$\psi$ with respect to $\mathfrak{s}(\mathcal{D})$.

###### Proof.

Let $X_{t}=\\{x_{1},\ldots,x_{t}\\}$ and $\mathcal{F}_{1}$ be the minimum
deterministic finite automaton with language
$\bm{\mathcal{L}}(\mathcal{F}_{1})=\mathsf{lang}(\mathcal{R}(\Sigma,0pt,\tau,\psi,X_{t}))$.

Assume that $D_{0}=B_{1}^{0}\cdots
B_{k}^{0}\in\mathcal{B}(\Sigma,0pt)^{\circ{k}}$, and for each $i\in[k]$,
$D_{i}=B_{1}^{i}\cdots
B_{k}^{i}\in\mathcal{B}(\Sigma^{\otimes\mathfrak{a}_{i}},0pt)^{\circ{k}}$,
where $\mathfrak{a}_{i}$ denotes the arity of $\mathsf{R}_{i}$. Then, consider
the finite automaton $\mathcal{F}_{2}$ defined as follows:

  * •

$Q(\mathcal{F}_{2})=\\{q_{0}\\}\cup\\{q_{i,[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}]}\colon\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}\in\Sigma\uplus\\{\square\\},\,i\in[k]\\}\text{;}$

  * •

$\begin{aligned}
T(\mathcal{F}_{2})&=\big{\\{}(q_{0},(B_{1}^{0},B_{1}^{1},\ldots,B_{1}^{l},\sigma_{1},\ldots,\sigma_{t}),q_{1,[\sigma_{1},\ldots,\sigma_{t}]})\colon\sigma_{1},\ldots,\sigma_{t}\in\Sigma\big{\\}}\\\\[-2.15277pt]
&\cup\begin{multlined}\Big{\\{}(q_{i,[\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{t}]},(B_{i+1}^{0},B_{i+1}^{1},\ldots,B_{i+1}^{l},\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}),q_{i+1,[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}]})\colon\\\\[0.86108pt]
\hfill{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\widetilde{\nu}_{j},\widetilde{\sigma}_{j}\in\Sigma\uplus\\{\square\\}},\,(\widetilde{\nu}_{j}=\square\Rightarrow\widetilde{\sigma}_{j}=\square)\text{
for each }j\in[t],\hskip 17.22217pt\\\\[-4.30554pt] \hfill
i\in[k-1]\Big{\\}}\text{;}\end{multlined}\Big{\\{}(q_{i,[\widetilde{\nu}_{1},\ldots,\widetilde{\nu}_{t}]},(B_{i+1}^{0},B_{i+1}^{1},\ldots,B_{i+1}^{l},\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}),q_{i+1,[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}]})\colon\\\\[0.86108pt]
\hfill{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\widetilde{\nu}_{j},\widetilde{\sigma}_{j}\in\Sigma\uplus\\{\square\\}},\,(\widetilde{\nu}_{j}=\square\Rightarrow\widetilde{\sigma}_{j}=\square)\text{
for each }j\in[t],\hskip 17.22217pt\\\\[-4.30554pt] \hfill
i\in[k-1]\Big{\\}}\text{;}\end{aligned}$

  * •

$I(\mathcal{F}_{2})=\\{q_{0}\\}$;
$F(\mathcal{F}_{2})=\\{q_{k,[\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}]}\colon\widetilde{\sigma}_{1},\ldots,\widetilde{\sigma}_{t}\in\Sigma\uplus\\{\square\\}\\}$.

One can verify that the language $\bm{\mathcal{L}}(\mathcal{F}_{2})$ consists
of all strings of the form

$D_{0}\otimes D_{1}\otimes\cdots\otimes D_{l}\otimes u_{1}\otimes\cdots\otimes
u_{t}$

such that, for each $i\in[t]$, $u_{i}$ is a string in $\Sigma^{\leq k}$.

Note that, the set of states of $\mathcal{F}_{2}$ can be split into $k$ levels
such that states in level $i$ only have transitions to states in level $i+1$.
Therefore, $\mathcal{F}_{2}$ is acyclic. Additionally, one can readily check
that $\mathcal{F}_{2}$ is deterministic and that the number of states in each
level of $\mathcal{F}_{2}$ can be described as a function of
$\lvert\Sigma\rvert$ and $t$.

Now, consider the automaton
$\mathcal{F}_{\cap}=\mathcal{F}_{1}\cap\mathcal{F}_{2}$ whose language is the
intersection of the languages of $\mathcal{F}_{1}$ and of $\mathcal{F}_{2}$.
Note that $\mathcal{F}_{\cap}$ accepts precisely the strings of the form
$D_{0}\otimes D_{1}\otimes\cdots\otimes D_{l}\otimes u_{1}\otimes\cdots\otimes
u_{t}$ such that $(u_{1}\ldots u_{t})$ is a satisfying assignment for $\psi$
with respect to the $\tau$-structure $\mathfrak{s}(\mathcal{D})$. Furthermore,
one can verify that $\mathcal{F}_{\cap}$ is also an acyclic deterministic
automaton whose states can be split into $k$ levels such that there are only
transitions going from level $i$ to level $i+1$.

Therefore, counting the number of assignments that satisfy $\psi$ with respect
to $\mathfrak{s}(\mathcal{D})$ amounts to counting the number of accepting
paths in $\mathcal{F}_{\cap}$. This can be done in time
$\mathcal{O}(\lvert\mathcal{F}_{\cap}\rvert^{2})$ using standard dynamic
programming, starting from the states of $\mathcal{F}_{\cap}$ that are in the
last level and, then, recording, for each state of each level, the number of
paths from that state to a final state. Since $\mathcal{F}_{\cap}$ can be
constructed in time $g(\Sigma,0pt,\tau,\psi,t)\cdot k$, for some computable
function $g$, the overall algorithm takes time
$\mathcal{O}(g(\Sigma,0pt,\tau,\psi,t)^{2}\cdot k^{2})$. By setting
$f(\Sigma,0pt,\tau,\psi,t)=c\cdot g(\Sigma,0pt,\tau,\psi,t)^{2}+d$ for some
sufficiently large constants $c$ and $d$, the theorem follows.∎

##  8 Conclusion

In this work, we have introduced the notion of decisional-width of a
relational structure, as a measure that intuitively tries to provide a
quantification of how difficult it is to define the relations of the
structure. Subsequently we provided a suitable way of defining infinite
classes of structures of small width. Interestingly, there exist classes of
structures of constant decisional-width that have very high width with respect
to most width measures defined so far in structural graph theory. As an
example, we have shown that the class of hypercube graphs has regular-
decisional width $2$, while it is well known that they have unbounded
treewidth and cliquewidth. Additionally, this family is not nowhere-dense.
Therefore, first-order model-checking and validity-testing techniques
developed for these well studied classes of graphs do not generalize to graphs
of constant decisional width. Other examples of families of graphs of constant
decisional width are paths, cliques (which have unbounded treewidth),
unlabeled grids (which have unbounded treewidth and cliquewidth) and many
others. It is interesting to note that these mentioned classes have all a
regular structure and, therefore, are “easy” to describe.

#### Acknowledgements

Alexsander Andrade de Melo acknowledges support from the Brazilian National
Council for Scientific and Technological Development (CNPQ 140399/2017-8) and
from the Brazilian Federal Agency for Support and Evaluation of Graduate
Education (CAPES 88881.187636/2018-01). Mateus de Oliveira Oliveira
acknowledges support from the Bergen Research Foundation, from the Research
Council of Norway (288761) and from the Sigma2 network (NN9535K).

## References

  * [1] Andrade de Melo, A., de Oliveira Oliveira, M.: On the width of regular classes of finite structures.  In: Proc. of the 27th International Conference on Automated Deduction, _Lecture Notes in Computer Science_ , vol. 11716, pp. 18–34. Springer (2019)
  * [2] Blumensath, A.: Automatic structures.  Diploma thesis, Rheinisch-Westfälische Technische Hochschule Aachen (1999)
  * [3] Blumensath, A., Gradel, E.: Automatic structures.  In: Proc. of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 51–62. IEEE (2000)
  * [4] Bollig, B.: On symbolic OBDD-based algorithms for the minimum spanning tree problem.  Theoretical Computer Science 447, 2–12 (2012)
  * [5] Bollig, B.: On the width of ordered binary decision diagrams.  In: Proc. of the 8th International Conference on Combinatorial Optimization and Applications (COCOA), pp. 444–458. Springer (2014)
  * [6] Bonomo, F., Grippo, L.N., Milanič, M., Safe, M.D.: Graph classes with and without powers of bounded clique-width.  Discrete Applied Mathematics 199, 3–15 (2016)
  * [7] Büchi, J.R.: Weak second order arithmetic and finite automata.  Z. Math. Logik Grundl. Math. 6, 66–92 (1960)
  * [8] Bulatov, A.A.: Graphs of relational structures: restricted types.  In: Proc. of the 31st Symposium on Logic in Computer Science (LICS), pp. 642–651 (2016)
  * [9] Chandran, L.S., Kavitha, T.: The treewidth and pathwidth of hypercubes.  Discrete Mathematics 306(3), 359–365 (2006)
  * [10] Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs.  Inf. Comput. 85(1), 12–75 (1990)
  * [11] Courcelle, B., Makowsky, J.A., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width.  Theory of Computing Systems 33(2), 125–150 (2000)
  * [12] Ebbinghaus, H.D., Flum, J.: Finite model theory.  Springer Science & Business Media (2005)
  * [13] Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical logic.  Springer Science & Business Media (2013)
  * [14] Elgot, C.C.: Decision problems of finite automata and related arithmetics.  Transactions of the American Mathematical Society 98, 21–52 (1961)
  * [15] Farb, B.: Automatic groups: a guided tour.  Enseign. Math.(2) 38(3-4), 291–313 (1992)
  * [16] Getoor, L., Friedman, N., Koller, D., Taskar, B.: Learning probabilistic models of relational structure.  In: Proc. of the 28th International Conference on Machine Learning (ICML), vol. 1, pp. 170–177 (2001)
  * [17] Grohe, M.: Algorithmic meta theorems.  In: Proc. of the 34th International Workshop on Graph-Theoretic Concepts in Computer Science (WG), pp. 30–30. Springer (2008)
  * [18] Grohe, M.: Algorithmic meta theorems for sparse graph classes.  In: Proc. of the 9th International Computer Science Symposium in Russia (CSR), pp. 16–22. Springer (2014)
  * [19] Hachtel, G.D., Somenzi, F.: A symbolic algorithm for maximum flow in 0-1 networks.  In: Proc. of the 6th International Conference on Computer-Aided Design (ICCAD), pp. 403–406. IEEE Computer Society Press (1993)
  * [20] Hliněnỳ, P., Seese, D.: Trees, grids, and MSO decidability: From graphs to matroids.  Theoretical Computer Science 351(3), 372–393 (2006)
  * [21] Khoussainov, B., Minnes, M.: Three lectures on automatic structures.  In: Proc. of Logic Colloquium, pp. 132–176 (2007)
  * [22] Khoussainov, B., Nerode, A.: Automatic presentations of structures.  In: Logic and computational complexity, pp. 367–392. Springer (1995)
  * [23] Kolaitis, P.G., Vardi, M.Y.: A game-theoretic approach to constraint satisfaction.  In: H.A. Kautz, B.W. Porter (eds.) Proc. of the 17th AAAI Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, pp. 175–181 (2000)
  * [24] Kreutzer, S.: Algorithmic meta-theorems.  In: Proc. of the 3rd International Workshop on Parameterized and Exact Computation (IWPEC), pp. 10–12. Springer (2008)
  * [25] Kruckman, A., Rubin, S., Sheridan, J., Zax, B.: A myhill-nerode theorem for automata with advice.  In: Proc. of the 3rd International Symposium on Games, Automata, Logics and Formal Verification (GANDALF), _Electronic Proceedings in Theoretical Computer Science_ , vol. 96, pp. 238–246 (2012)
  * [26] Poon, H., Domingos, P.M., Sumner, M.: A general method for reducing the complexity of relational inference and its application to MCMC.  In: Proc. of the 25th AAAI Conference on Artificial Intelligence, vol. 8, pp. 1075–1080 (2008)
  * [27] Sawitzki, D.: Implicit flow maximization by iterative squaring.  In: Proc. of the 30th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), pp. 301–313. Springer (2004)
  * [28] Seese, D.: The structure of the models of decidable monadic theories of graphs.  Annals of pure and applied logic 53(2), 169–195 (1991)
  * [29] Sutskever, I., Tenenbaum, J.B., Salakhutdinov, R.R.: Modelling relational data using bayesian clustered tensor factorization.  In: Advances in neural information processing systems, pp. 1821–1828 (2009)
  * [30] Woelfel, P.: Symbolic topological sorting with obdds.  Journal of Discrete Algorithms 4(1), 51–71 (2006)
  * [31] Zaid, F.A., Grädel, E., Reinhardt, F.: Advice Automatic Structures and Uniformly Automatic Classes.  In: Proc. of the 26th Conference on Computer Science Logic (CSL), _LIPIcs_ , vol. 82, pp. 35:1–35:20 (2017)