[name=Theorem,numberwithin=section]thm

# Conjunctive Regular Path Queries under Injective Semantics

Diego Figueira<EMAIL_ADDRESS>0000-0003-0114-2257 Univ. Bordeaux,
CNRS,
Bordeaux INP, LaBRI, UMR 5800F-33400, TalenceFranceF-33400 and  Miguel Romero
<EMAIL_ADDRESS>0000-0002-2615-6455 Faculty of Engineering and Science,
Universidad Adolfo IbáñezChile

(2023)

###### Abstract.

We introduce injective semantics for Conjunctive Regular Path Queries (CRPQs),
and study their fundamental properties. We identify two such semantics: atom-
injective and query-injective semantics, both defined in terms of injective
homomorphisms. These semantics are natural generalizations of the well-studied
class of RPQs under simple-path semantics to the class of CRPQs. We study
their evaluation and containment problems, providing useful characterizations
for them, and we pinpoint the complexities of these problems. Perhaps
surprisingly, we show that containment for CRPQs becomes undecidable for atom-
injective semantics, and PSpace-complete for query-injective semantics, in
contrast to the known ExpSpace-completeness result for the standard semantics.
The techniques used differ significantly from the ones known for the standard
semantics, and new tools tailored to injective semantics are needed. We
complete the picture of complexity by investigating, for each semantics, the
containment problem for the main subclasses of CRPQs, namely Conjunctive
Queries and CRPQs with finite languages.

graph databases, regular path queries (RPQ), containment, evaluation, simple
paths, injective homomorphisms

Diego Figueira is partially supported by ANR QUID, grant ANR-18-CE400031.
Miguel Romero is funded by Fondecyt grant 11200956, the Data Observatory
Foundation, and the National Center for Artificial Intelligence CENIA
FB210017, Basal ANID

††journalyear: 2023††copyright: licensedothergov††conference: Proceedings of
the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems;
June 18–23, 2023; Seattle, WA, USA††booktitle: Proceedings of the 42nd ACM
SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS ’23),
June 18–23, 2023, Seattle, WA, USA††price: 15.00††doi:
10.1145/3584372.3588664††isbn: 979-8-4007-0127-6/23/06††ccs: Information
systems Query languages for non-relational engines††ccs: Theory of computation
Database query processing and optimization (theory)

##  1\. Introduction

Graph databases are important for many applications nowadays (Sakr et al.,
2021; Angles et al., 2017). In a nutshell, graph databases are abstracted as
edge-labeled directed graphs, where nodes represent entities and labeled edges
represent relations between these entities. A fundamental way to query graph
databases is by finding _patterns_ on the interrelation between entities. In
this respect, a central querying mechanism for modern graph query languages is
that of _regular path queries_ (RPQs). RPQs provide a simple form of recursion
tailored to discovering entities linked by paths with certain properties.
These are queries of the form $x\xrightarrow{L}y$, where $L$ is a regular
expression on the alphabet of database edge labels. Such a query returns all
pairs of nodes $(u,v)$ in the database such that there is a (directed) path
from $u$ to $v$ whose label matches $L$.

The closure under conjunction and existential quantification of RPQ yields
what is known as _Conjunctive RPQs_ (CRPQs). Indeed, CRPQs can be understood
as the generalization of conjunctive queries with this simple form of
recursion. CRPQs are part of SPARQL (Harris and Seaborne, 2013), the W3C
standard for querying RDF data (a widespread format for graph databases). Some
examples of RDF databases are well-known knowledge bases such as DBpedia and
Wikidata. For example, (C)RPQs are popular for querying Wikidata (Malyshev et
al., 2018; Bonifati et al., 2019). More generally, CRPQs are basic building
blocks for querying graph-structured databases (Barceló, 2013; Angles et al.,
2017). They are part of G-core (Angles et al., 2018) and Cypher (Francis et
al., 2018), the latter being the query language of Neo4j, which is currently
one of the most popular commercial graph databases. They are also part of the
ongoing standardization effort GQL for graph query languages (Deutsch et al.,
2022; GQL, 2021).

#### Alternative semantics.

The semantics for the evaluation of an RPQ $x\xrightarrow{L}y$ as above often
assumes that any, arbitrary, (directed) path from $u$ to $v$ is allowed as
long as it satisfies the regular property $L$. However, there are alternative
semantics in which one may restrict the path to have no repeated vertices
(a.k.a.  _simple path_), or no repeated edges (a.k.a.  _trail_). In this way,
only a _finite number_ of paths need to be considered. As a matter of fact,
these alternative semantics have received considerable attention both in
practice and from the database theory community. Indeed, they are part of
Neo4j’s Cypher query language and are included in GQL as possible ways to
evaluate RPQs. Furthermore, these alternative semantics have been extensively
studied in the literature from the late 80s onwards (Cruz et al., 1987;
Mendelzon and Wood, 1995; Bagan et al., 2020; Martens and Trautner, 2019;
Losemann and Martens, 2013; Martens and Popp, pear). However, rather
surprisingly, this body of research has focused mainly on RPQs, leaving the
case of CRPQs under alternative semantics essentially unexplored.

#### Contribution.

We introduce _injective_ semantics for CRPQs, which generalize the simple-path
semantics for RPQs, and we investigate the fundamental properties of CRPQs
under these semantics. Concretely, we identify two possible natural semantics:

(1) Atom-injective. The first semantics is to require that each CRPQ _atom_ is
interpreted with the simple-path semantics of RPQs, that is, atoms of the form
$x\xrightarrow{L}y$ must be mapped to simple paths and atoms of the form
$x\xrightarrow{L}x$ must be mapped to simple cycles. In particular, there is
no requirement that paths from different atoms be disjoint. Under this
semantics, a Boolean CRPQ like $Q=\exists
x,y,z\,(x\xrightarrow{(a+b)^{+}}y\land x\xrightarrow{(b+c)^{+}}z)$ holds true
in the graph database consisting of a directed path of $b$’s by mapping $x$ to
the first node of the path and $y$ and $z$ to the last node.

(2) Query-injective. The alternative is to consider a more restrictive
semantics in which paths corresponding to different atoms must be mapped to
different nodes, and hence there cannot be repeated nodes neither in paths nor
between paths. This semantics generalizes both RPQ under simple path semantics
and Conjunctive Queries under injective semantics. In this case, the query $Q$
above may only be true if the database contains two simple paths starting in
the same node with the corresponding language which are disjoint (except for
the origin).

We call the former _atom-injective semantics_ since the “no repeated nodes”
condition is required separately for each atom, and the latter _query-
injective semantics_ since injectivity is required for the query as a whole.
The three semantics (standard, atom-injective, query-injective) form a
hierarchy, where query-injective is the most restrictive and standard
semantics is the least.

We first consider the _evaluation problem_ for CRPQs, that is, checking
whether a tuple $\bar{v}$ belongs to the results of a query $Q$ over a
particular graph database $G$. For standard semantics, this problem is NP-
complete in _combined complexity_ , that is, when both query and database are
part of the input, and NL-complete in _data complexity_ , that is, when the
query is considered to be fixed. Under both injective semantics, the
evaluation problem remains NP-complete in combined complexity, and becomes NP-
complete in data complexity. This follows straight from the fact that RPQ
evaluation under simple-path semantics is NP-complete, even for very simple
RPQs (Mendelzon and Wood, 1995; Barceló, 2013).

We therefore turn our attention to the _containment problem_ , which is the
main focus of this paper. This problem asks whether every result of a query
$Q_{1}$ is also returned by a query $Q_{2}$, independently of the underlying
database. Checking containment is one of the most basic static analysis tasks,
and it can be a means for query optimization. The containment problem for
CRPQs is known to be ExpSpace-complete (Calvanese et al., 2000; Florescu et
al., 1998) under standard semantics, and the study of containment has been
extended to queries with restricted shapes (Figueira, 2020) or restricted
regular expressions (Figueira et al., 2020).

Rather surprisingly, as we show, the hierarchy of the three semantics
(standard, atom-injective, query-injective) is not reflected in the complexity
of the containment problem: the most restrictive semantics (query-injective)
is PSpace-complete, the least restrictive one (standard) is ExpSpace-complete,
and the middle one (atom-injective) is undecidable. These results for atom-
and query-injective semantics are the main technical contributions of this
paper. We complete the picture with a thorough study on the containment
problem for the two main subclasses of CRPQs: Conjunctive Queries, and CRPQs
with no Kleene star operator. We provide complexity completeness results for
all possible combinations (cf. Figure 1).

|  CQ/CQ |  CQ/CRPQ |  CRPQ/CQ |  CQ/$\textsf{CRPQ}^{\textsf{fin}}$ |  $\textsf{CRPQ}^{\textsf{fin}}$/CQ
---|---|---|---|---|---
standard |  NP-c (Chandra and Merlin, 1977) |  NP-c (${\dagger}$) |  $\Pi^{p}_{2}$-c (${\ddagger}$) |  NP-c (${\dagger}$) |  $\Pi^{p}_{2}$-c ($\mathsection$,${\ddagger}$)
query-injective |  NP-c (F.2) |  NP-c (F.2) |  $\Pi^{p}_{2}$-c (6.1,F.7) |  NP-c (F.2) |  $\Pi^{p}_{2}$-c (6.1,F.7)
atom-injective |  NP-c (F.4) |  $\Pi^{p}_{2}$-c (6.2,F.10) |  $\Pi^{p}_{2}$-c (F.6,F.7) |  $\Pi^{p}_{2}$-c (6.2,F.10) |  $\Pi^{p}_{2}$-c (F.6,F.7)

|  CRPQ/$\textsf{CRPQ}^{\textsf{fin}}$ |  $\textsf{CRPQ}^{\textsf{fin}}$/CRPQ |  $\textsf{CRPQ}^{\textsf{fin}}$/$\textsf{CRPQ}^{\textsf{fin}}$ |  CRPQ/CRPQ
---|---|---|---|---
standard |  PSpace-c (F.8,F.9) |  $\Pi^{p}_{2}$-c ($\mathsection$,F.10) |  $\Pi^{p}_{2}$-c ($\mathsection$,F.10) |  ExpSpace-c ($\mathdollar$,¢)
query-injective |  PSpace-c (F.8,5.1) |  $\Pi^{p}_{2}$-c (6.1,F.10) |  $\Pi^{p}_{2}$-c (6.1,F.10) |  PSpace-c (F.8,5.1)
atom-injective | undec. (5.2) |  $\Pi^{p}_{2}$-c (6.2,F.10) |  $\Pi^{p}_{2}$-c (6.2,F.10) | undec. (5.2)

${\dagger}$: (Figueira et al., 2020, Thm 4.2) $\mathsection$: (Figueira et
al., 2020, Thm 4.3) ${\ddagger}$: (Figueira et al., 2020, Thm 4.4)
$\mathdollar$: (Calvanese et al., 2000, Thm. 6) ¢: (Florescu et al., 1998,
Thm. 4.8)

Figure 1. Complexity of the containment problem under standard, query-
injective, and atom-injective semantics. Numbers in brackets reference
proposition/theorem numbers (some of them in Appendix F).

Our main results require the development of novel techniques, which yield
insights on the subtle difficulties for handling static analysis under these
semantics.

#### Organization.

After a preliminary section §2, we define and characterize the evaluation and
containment problems in §3 and §4, respectively. We study the containment
problem for arbitrary CRPQs in §5, and for subclasses of CRPQs in §6. We
conclude with §7. Omitted or sketched proofs can be found in the Appendix.

##  2\. Preliminaries

We assume familiarity with regular languages, regular expressions and non-
deterministic finite automata (NFA). We often blur the distinction between a
regular expression and the language it defines; similarly for NFAs.

#### Graph databases and paths.

A _graph database_ over a finite alphabet $\mathbb{A}$ is a finite edge-
labeled graph $G=(V,E)$ over $\mathbb{A}$, where $V$ is a finite set of
vertices and $E\subseteq V\times\mathbb{A}\times V$ is the set of labeled
edges (or simply _edges_). We write $u\xrightarrow{a}v$ to denote an edge
$(u,a,v)\in E$. A _path_ from $u$ to $v$ in a graph database $G=(V,E)$ over
alphabet $\mathbb{A}$ is a (possibly empty) sequence
$\pi=v_{0}\xrightarrow{a_{1}}v_{1},\,v_{1}\xrightarrow{a_{2}}v_{2},\,\dots\,,v_{k-1}\xrightarrow{a_{k}}v_{k}$
of edges of $G$, where $k\geq 0$, $u=v_{0}$ and $v=v_{k}$. An _internal node_
of such a path is any node $v_{i}$ with $0<i<k$. The label of $\pi$ is the
word $a_{1}\dots a_{k}\in\mathbb{A}^{*}$. When $k=0$ the label of $\pi$ is the
empty word $\varepsilon$. We say that $\pi$ is a _simple path_ if all the
nodes $v_{i}$ are pairwise distinct, and a _simple cycle_ if $v_{0}=v_{k}$ and
all the nodes $v_{i}$ (for $i<k$) are pairwise distinct.

#### Conjunctive queries and homomorphisms.

In the setting of graph databases, a _conjunctive query_ (CQ) $Q$ over a
finite alphabet $\mathbb{A}$ is an expression
$Q(x_{1},\dots,x_{n})=A_{1}\land\dots\land A_{m}$, for $m\geq 0$, where
$(x_{1},\dots,x_{n})$ is a tuple of variables, and each $A_{i}$ is an _atom_
of the form $x\xrightarrow{a}y$, for variables $x$ and $y$, and
$a\in\mathbb{A}$. We denote by $\textit{vars}(Q)$ the set of variables
appearing in $Q$. We often write $Q(\bar{x})$ instead of $Q$ to emphasize the
tuple $\bar{x}=(x_{1},\dots,x_{n})$ of _free variables_ of $Q$. We assume that
the free variables $x_{i}$ are not necessarily distinct. The variables of $Q$
which are not in $\\{x_{1},\dots,x_{n}\\}$ are (implicitly) existentially
quantified. As usual, if $\bar{x}$ is empty, we say that the CQ $Q$ is
_Boolean_. Note that every CQ can be seen as a graph database (each atom is an
edge), hence, by slightly abusing notation, we sometimes use graph database
terminology for CQs.

A _homomorphism_ $h$ from a CQ $Q(\bar{x})$ to a graph database $G=(V,E)$ is a
mapping from $\textit{vars}(Q)$ to $V$ such that $h(x)\xrightarrow{a}h(y)$
belongs to $E$ for each atom $x\xrightarrow{a}y$ of $Q$. We say that $h$ is
_injective_ if additionally we have $h(x)\neq h(y)$ for all pairs of distinct
variables $x$ and $y$. We write $Q\to G$ if there is a homomorphism from $Q$
to $G$ and $h:Q\to G$ if $h$ is such a homomorphism. Similarly, for a tuple
$\bar{v}$, we write $Q\to(G,\bar{v})$ if there is a homomorphism $h$ from $Q$
to $G$ such that $h(\bar{x})=\bar{v}$ and $h:Q\to(G,\bar{v})$ to make such $h$
explicit. We use similar notation for injective homomorphisms, replacing $\to$
by $\xrightarrow{\textit{inj}}$. Homomorphisms between CQs are essentially
defined as before with the difference that free variables are mapped to free
variables. That is, given two CQs $Q_{1}(\bar{x}_{1})$, $Q_{2}(\bar{x}_{2})$,
we have $h:Q_{1}\to Q_{2}$ if $h:Q_{1}\to(G,\bar{x}_{2})$, and
$h:Q_{1}\xrightarrow{\textit{inj}}Q_{2}$ if
$h:Q_{1}\xrightarrow{\textit{inj}}(G,\bar{x}_{2})$, where $G$ is the graph
database denoted by $Q_{2}$.

We also work with CQs with _equality atoms_ , which are queries of the form
$Q(\bar{x})=P\land I$, where $P$ is a CQ (without equality atoms) and $I$ is a
conjunction of equality atoms of the form $x=y$ (the variables $x$ and $y$ may
not belong to $\textit{vars}(P)$). Again, we denote by $\textit{vars}(Q)$ the
set of variables appearing in $Q$. We define the binary relation $=_{Q}$ over
$\textit{vars}(Q)$ to be the reflexive-symmetric-transitive closure of the
binary relation $\\{(x,y):\text{$x=y$ is an equality atom in $Q$}\\}$. In
other words, we have $x=_{Q}y$ if the equality $x=y$ is forced by the equality
atoms of $Q$. Note that every CQ with equality atoms $Q(\bar{x})=P\land I$ is
equivalent to a CQ without equality atoms $Q^{\equiv}$, which is obtained from
$Q$ by collapsing each equivalence class of the relation $=_{Q}$ into a single
variable. This transformation gives us a _canonical_ renaming, which we always
denote by $\Phi$, from $\textit{vars}(Q)$ to $\textit{vars}(Q^{\equiv})$,
defined by $\Phi(x)=C$, where $C$ is the equivalence class containing $x$. In
particular, the tuple of free variables of $Q^{\equiv}$ is $\Phi(\bar{x})$.

#### Conjunctive regular path queries.

A _conjunctive regular path query_ (CRPQ) $Q$ over a finite alphabet
$\mathbb{A}$ is an expression $Q(x_{1},\dots,x_{n})=A_{1}\land\dots\land
A_{m}$, for $m\geq 0$, where each $A_{i}$ is an atom of the form
$x\xrightarrow{L}y$, for variables $x$ and $y$, and a regular expression $L$
over $\mathbb{A}$. As before, we denote by $\textit{vars}(Q)$ the set of
variables of $Q$ and often write $Q(\bar{x})$ instead of $Q$ where
$\bar{x}=(x_{1},\dots,x_{n})$ is the tuple of (not necessarily distinct) free
variables of $Q$. If the tuple $\bar{x}$ is empty, we say that $Q$ is
_Boolean_. The class of CRPQs extends the class of CQs and the well-studied
class of _regular path queries_ (RPQs). Indeed, each CQ can be seen as a CRPQ
where the regular expressions are single labels from $\mathbb{A}$. On the
other hand, an RPQ corresponds to a CRPQ of the form
$Q(x,y)=x\xrightarrow{L}y$.

In this paper we shall consider three basic classes: the class CQ of all
Conjunctive Queries, the class CRPQ of all CRPQs, and the class
$\textsf{CRPQ}^{\textsf{fin}}$ of CRPQs using regular expressions with no
Kleene-star (denoting finite languages). Observe that the latter corresponds
to the subclass of CRPQ without recursion.

###  2.1. Standard, atom-injective, and query-injective semantics

We now define the _standard semantics_ for CRPQs (i.e., the usual semantics
from the database theory literature) and we introduce the two new sorts of
injective semantics.

For simplicity of exposition, we first give the semantics for CRPQ’s without
$\varepsilon$, and we then show how to expand the semantics to languages that
include $\varepsilon$. Let $Q$ be a CRPQ of the form
$Q(\bar{z})=x_{1}\xrightarrow{L_{1}}y_{1}\land\dotsb\land
x_{n}\xrightarrow{L_{n}}y_{n}$ and assume that no language $L_{i}$ contains
$\varepsilon$ (the empty word). Given a graph database $G$, the _evaluation_
of $Q$ over $G=(V,E)$ _under standard semantics_ ($st$-semantics for short),
denoted by $Q(G)^{st}$, is the set of tuples $\bar{v}$ of nodes for which
there is a mapping $\mu:\textit{vars}(Q)\to V$ such that
$\mu(\bar{z})=\bar{v}$ and for each $i$ there is a path $\pi_{i}$ from
$\mu(x_{i})$ to $\mu(y_{i})$ in $G$ whose label is in $L_{i}$. The evaluation
under _atom-injective semantics_ (a-inj-semantics for short), denoted by
$Q(G)^{\textit{a-inj}}$, is defined similarly, but we further require that
each $\pi_{i}$ is a simple path (if $x_{i}\neq y_{i}$) or a simple cycle (if
$x_{i}=y_{i}$). Finally, the evaluation under _query-injective semantics_
(q-inj-semantics for short), denoted by $Q(G)^{\textit{q-inj}}$, is similar to
the atom-injective semantics (i.e., each $\pi_{i}$ must be simple), but we
additionally require that $\mu$ is injective and that for every $i\neq j$
there are no internal nodes shared by $\pi_{i}$ and $\pi_{j}$.

The semantics for a CRPQ $Q$ with $\varepsilon$-words is defined as expected:
the query $Q$ is equivalent to a _union_ of $\varepsilon$-free CRPQs and hence
its evaluation is the union of the evaluation of these $\varepsilon$-free
queries. More formally, for $\star\in\\{st,\textit{a-inj},\textit{q-inj}\\}$,
the semantics under $\star$-semantics of $Q(\bar{z})=x\xrightarrow{L}y\land
Q^{\prime}$, where $L$ contains $\varepsilon$ and $Q^{\prime}$ is a CRPQ, is
the union of the set of tuples given by the $\star$-evaluation of
$Q(\bar{z})=x\xrightarrow{L\setminus\\{\varepsilon\\}}y\land Q^{\prime}$ and
by the $\star$-evaluation of $Q(\bar{z}[x/y])=Q^{\prime}[x/y]$, where $X[x/y]$
is the result of replacing every occurrence of variable $x$ with variable $y$
in $X$.

###### Remark 2.1.

The three semantics form a hierarchy. In particular, for every CRPQ $Q$ and
every graph database $G$, we have $Q(G)^{\textit{q-inj}}\subseteq
Q(G)^{\textit{a-inj}}\subseteq Q(G)^{st}$. The converse inclusions do not hold
in general.

Figure 2. The CRPQ $Q(x,y)$ and graph databases $G$ and $G^{\prime}$ from
Example 2.1.

###### Example 2.1.

Consider the CRPQ $Q(x,y)=x\xrightarrow{(ab)^{*}}y\land y\xrightarrow{c^{*}}x$
and the graph database $G$ from Figure 2. Observe that $(u,w)\in
Q(G)^{\textit{a-inj}}$ but $(u,w)\notin Q(G)^{\textit{q-inj}}$. On the other
hand, it is easy to check that $Q(G)^{st}=Q(G)^{\textit{a-inj}}$. The graph
database $G^{\prime}$ from Figure 2 provides a separation of the three
semantics. Indeed, as before $Q(G^{\prime})^{\textit{a-inj}}\not\subseteq
Q(G^{\prime})^{\textit{q-inj}}$, but additionally we have $(u,v)\in
Q(G^{\prime})^{st}$ and $(u,v)\not\in Q(G^{\prime})^{\textit{a-inj}}$.

###  2.2. Characterizing evaluation

We state the semantics defined above in terms of restrictive notions of
homomorphisms based on injectivity. This is based on the key notion of
_expansion_ of a CRPQ (a.k.a. canonical database), which will become useful
for the technical developments of the next sections.

For any atom $x\xrightarrow{L}y$ of a CRPQ $Q$ and $w\in L$, the _$w$
-expansion_ of $x\xrightarrow{L}y$ is the Boolean CQ with equality atoms of
the form (i) $P=x\xrightarrow{a_{1}}z_{1}\land
z_{1}\xrightarrow{a_{2}}z_{2}\land\cdots\land z_{k-1}\xrightarrow{a_{k}}y$ if
$w\neq\varepsilon$, such that the $z_{i}$ are fresh new variables, or of the
form (ii) $P=(y=z)$ if $w=\varepsilon$. We usually write $x\xrightarrow{w}y$
to denote such a $w$-expansion, with $w=a_{1}\cdots a_{k}$. An _expansion_ of
$x\xrightarrow{L}y$ is a _$w$ -expansion_ for some $w\in L$. An _expansion
profile_ of the CRPQ $Q$ is any function $\varphi$ mapping each atom of $Q$ to
an expansion thereof. An _expansion_ of the CRPQ
$Q(\bar{x})=A_{1}\land\dots\land A_{m}$ is a CQ $E(\bar{y})$ for which there
is an expansion profile $\varphi$ of $Q$ such that $E=\widetilde{E}^{\equiv}$,
where $\widetilde{E}$ is the CQ with equality atoms defined by
$\widetilde{E}(\bar{x})=\varphi(A_{1})\land\cdots\land\varphi(A_{m})$. We
denote by $\textup{{Exp}}^{\mathit{}}(Q)$ the set of all expansions of the
CRPQ $Q$. Intuitively, an expansion of $Q$ is obtained by expanding each atom
of $Q$ and then collapsing equivalent variables. For example, one possible
expansion of the query $Q(x,y)=x\xrightarrow{(ab)^{*}}y\land
y\xrightarrow{c^{*}}x$ from Figure 2 is $E_{1}(x,x)=x\xrightarrow{a}z\land
z\xrightarrow{b}x$ through the expansion profile mapping
$x\xrightarrow{(ab)^{*}}y$ to $ab$ and $y\xrightarrow{c^{*}}x$ to
$\varepsilon$, and another expansion $E_{2}(x,y)=x\xrightarrow{a}z\land
z\xrightarrow{b}y\land y\xrightarrow{c}x$ mapping the atoms to $ab$ and $c$
respectively.

#### Standard and query-injective semantics.

The standard and q-inj semantics can be rephrased as follows.

###### Proposition 2.2.

Let $Q$ be a CRPQ and $G$ be a graph database. Then $Q(G)^{st}$ [resp.
$Q(G)^{\textit{q-inj}}$] is the set of tuples $\bar{v}$ of nodes for which
there is $E\in\textup{{Exp}}^{\mathit{}}(Q)$ such that $E\to(G,\bar{v})$
[resp. $E\xrightarrow{\textit{inj}}(G,\bar{v})$].

#### Atom-injective semantics.

The atom-injective semantics corresponds to the less restrictive alternative
that an arbitrary homomorphism can be allowed as long as it is injective when
restricted to the expansions of each atom. Let $E(\bar{y})$ be an expansion of
a CRPQ $Q(\bar{x})$, $\varphi$ be an expansion profile producing $E$, and
$\widetilde{E}(\bar{x})=\varphi(A_{1})\land\cdots\land\varphi(A_{m})$ be the
associated CQ with equality atoms (in particular $E=\widetilde{E}^{\equiv}$).
Let $\Phi:\textit{vars}(\widetilde{E})\to\textit{vars}(E)$ be the canonical
renaming. We say that two variables $x,y\in\textit{vars}(E)$ are _$\varphi$
-atom-related_ if there is some atom expansion $\varphi(A_{i})$ containing
some $x^{\prime},y^{\prime}$ such that $\Phi(x^{\prime})=x$ and
$\Phi(y^{\prime})=y$.

We now define a notion of injective homomorphism tailored to CRPQ expansions.
We say that $h$ is an _atom-injective homomorphism_ from an expansion $E$ of a
CRPQ $Q$ to a graph database $G$ mapping free variables to $\bar{v}$ if
$h:E\to(G,\bar{v})$ and there is an expansion profile $\varphi$ producing $E$
such that $h(x)\neq h(y)$ for every pair of distinct $\varphi$-atom-related
variables $x$ and $y$. We write $E\xrightarrow{\textit{a-inj}}(G,\bar{v})$ if
such an $h$ exists. Atom-injective homomorphisms from $E$ to CQs are defined
in the obvious way.

###### Proposition 2.3.

Let $Q$ be a CRPQ and $G$ be a graph database. Then $Q(G)^{\textit{a-inj}}$ is
the set of tuples $\bar{v}$ of nodes for which there is
$E\in\textup{{Exp}}^{\mathit{}}(Q)$ such that
$E\xrightarrow{\textit{a-inj}}(G,\bar{v})$.

##  3\. The evaluation problem

The decision problem associated to evaluation is the _evaluation problem_ for
a class ${\mathcal{C}}$ of CRPQs and a semantics
$\star\in\\{st,\textit{a-inj},\textit{q-inj}\\}$.

Problem |  Evaluation problem for ${\mathcal{C}}$ under $\star$-semantics
---|---
Given |  A graph database $G$, a query $Q(\bar{x})\in{\mathcal{C}}$, and a tuple $\bar{v}$ of nodes.
Question |  Is $\bar{v}\in Q(G)^{\star}$?

The evaluation problem is NP-complete under injective semantics, as it is the
case under standard semantics.

###### Proposition 3.1.

The evaluation problem for CRPQ and CQ is NP-complete in combined complexity,
for all semantics.

###### Proof.

The lower bound follows by an easy reduction from the injective-homomorphism
testing problem, also known as the subgraph isomorphism problem, which is a
well-known NP-complete problem. (Cook, 1971; Garey and Johnson, 1979). Indeed,
a Boolean CQ $Q$ maps injectively to $G$ iff
$Q(G)^{\textit{q-inj}}\neq\emptyset$ iff
$Q^{+}(G^{+})^{\textit{a-inj}}\neq\emptyset$, where $G^{+}$ [resp. $Q^{+}$] is
the result of adding, for a fresh symbol $R$, an $R$-edge between every pair
of vertices [resp. an $R$-atom between every pair of variables].

The upper bound is a consequence of the polynomial-sized witness property.
That is, if $Q\in\textsf{CRPQ}$, and $\bar{v}\in Q(G)^{\star}$, then there
exists an expansion $E$ of $Q$ such that
$E\xrightarrow{\textit{inj}}(G,\bar{v})$ if $\star=\textit{q-inj}$ and
$E\xrightarrow{\textit{a-inj}}(G,\bar{v})$ if $\star=\textit{a-inj}$. In
either case, $E$ is linear in $G$ and $Q$. One can then guess such an
expansion and check the existence of the corresponding homomorphism. ∎

The data complexity for the alternative semantics (i.e., when the query is
considered to be of constant size) is also NP-complete, since evaluation of
RPQs under simple path semantics is NP-complete, even for very simple regular
expressions (Mendelzon and Wood, 1995):

###### Proposition 3.2.

The evaluation problem for CRPQ is NP-complete in data complexity, for atom-
injective and query-injective semantics.

The RPQs which can be evaluated efficiently in data complexity have been
characterized via a trichotomy result: they can be either NP-complete, NL-
complete, or in AC0 (Bagan et al., 2020, Theorem 2). The generalization of
this result to CRPQs under injective semantics seems highly non-trivial, and
in particular it would necessitate a comprehensive understanding of the query
equivalence problem, which is the focus of the next sections.

##  4\. The containment problem

A CRPQ $Q_{1}$ is _contained_ in a CRPQ $Q_{2}$ under $\star$-semantics,
denoted by $Q_{1}\subseteq_{\star}Q_{2}$, if $Q_{1}(G)^{\star}\subseteq
Q_{2}(G)^{\star}$ for every graph database $G$. We define the _containment
problem_ , which is parameterized by classes ${\mathcal{C}}_{1}$ and
${\mathcal{C}}_{2}$ of CRPQs as well as the semantics used (standard, query-
injective, or atom-injective).

Problem |  ${\mathcal{C}}_{1}$/${\mathcal{C}}_{2}$ containment problem under $\star$-semantics
---|---
Given |  CRPQs $Q_{1}\in{\mathcal{C}}_{1}$ and $Q_{2}\in{\mathcal{C}}_{2}$.
Question |  Does $Q_{1}\subseteq_{\star}Q_{2}$ hold?

Under standard semantics, all combinations among CQ, CRPQ and
$\textsf{CRPQ}^{\textsf{fin}}$ have been studied and are decidable. In
particular:

###### Theorem 4.1.

(Calvanese et al., 2000; Florescu et al., 1998) The CRPQ/CRPQ containment
problem under standard semantics is ExpSpace-complete.

We will dedicate the rest of the paper to study the situation for injective
semantics. We show that one injective semantics becomes undecidable while the
other becomes better behaved computationally under standard complexity
theoretic assumptions (cf. the CRPQ/CRPQ column of Figure 1).

###  4.1. Characterizing containment

For the standard semantics, it is well-known that containment of CRPQs can be
characterized in terms of expansions:

###### Proposition 4.2.

(Calvanese et al., 2000) Let $Q_{1}$ and $Q_{2}$ be CRPQs. Then
$Q_{1}\subseteq_{st}Q_{2}$ iff for every
$E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that $E_{2}\to E_{1}$.

A similar characterization holds for query-injective semantics:

###### Proposition 4.3.

Let $Q_{1}$ and $Q_{2}$ be CRPQs. Then $Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$
iff for every $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}E_{1}$.

As it turns out, the previous characterization does not work for atom-
injective semantics (replacing $\xrightarrow{\textit{inj}}$ by
$\xrightarrow{\textit{a-inj}}$). In this case, the space of expansions of
$Q_{1}$ is not enough and we need to check $Q_{2}$ against a _larger_ space of
expansions of $Q_{1}$ we define below.

An _atom-injective-expansion_ (a-inj-expansion for short) of a CRPQ
$Q(\bar{x})$ is a CQ $F(\bar{y})$ for which there is a CQ with equality atoms
$\widetilde{F}(\bar{z})=E(\bar{z})\land J$ such that (i)
$F=\widetilde{F}^{\equiv}$, (ii) $E(\bar{z})$ is an expansion of $Q$ produced
by some expansion profile $\varphi$, and (iii) $J$ is a conjunction of
equality atoms $x^{\prime}=y^{\prime}$, for variables
$x^{\prime},y^{\prime}\in\textit{vars}(E)$, such that for every pair of
distinct $\varphi$-atom-related variables $x,y$ in $E$, we have
$x\neq_{\widetilde{F}}y$. We denote by
$\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q)$ the set of all a-inj-expansions
of $Q$. The intuition is that these types of expansions are obtained from an
ordinary expansion of $Q$ by identifying some pairs of variables which are not
atom-related (the identifications are given by $J$). We use this for the
following useful result:

###### Lemma 4.4.

Let $Q$ be a CRPQ, $E^{\prime}$ be a CQ, $G$ be a graph database, and
$\bar{v}$ be a tuple of nodes. The following are equivalent:

  1. (1)

There is $E\in\textup{{Exp}}^{\mathit{}}(Q)$ s.t.
$E\xrightarrow{\textit{a-inj}}(G,\bar{v})$ [resp.
$E\xrightarrow{\textit{a-inj}}E^{\prime}$].

  2. (2)

There is $F\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q)$ s.t.
$F\xrightarrow{\textit{inj}}(G,\bar{v})$ [resp.
$F\xrightarrow{\textit{inj}}E^{\prime}$].

As a corollary of Lemma 4.4 we obtain an alternative definition of atom-
injective semantics:

###### Corollary 4.5.

Let $Q$ be a CRPQ, $G$ be a graph database and $\bar{v}$ be a tuple of nodes.
Then $\bar{v}\in Q(G)^{\textit{a-inj}}$ if and only if there is
$F\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q)$ such that
$F\xrightarrow{\textit{inj}}(G,\bar{v})$.

We now give our characterization of atom-injective containment:

###### Proposition 4.6.

For every pair $Q_{1}$, $Q_{2}$ of CRPQs, the following are equivalent:

  1. (1)

$Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$.

  2. (2)

For every $F_{1}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q_{1})$ there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{a-inj}}F_{1}$.

  3. (3)

For every $F_{1}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q_{1})$ there is
$F_{2}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q_{2})$ such that
$F_{2}\xrightarrow{\textit{inj}}F_{1}$.

From the characterizations above, for every pair of CRPQs $Q_{1},Q_{2}$, we
have that $Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$ implies
$Q_{1}\subseteq_{st}Q_{2}$ and that $Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$
implies $Q_{1}\subseteq_{st}Q_{2}$ (while the converse implications do not
hold in general). In contrast, and in spite of the hierarchy between the
semantics, there is no such implication between query-injective and atom-
injective containment, as the following example shows.

###### Example 4.7.

Consider the Boolean CRPQs $Q_{1}=x\xrightarrow{a}y\land y\xrightarrow{b}z$,
$Q_{2}=x\xrightarrow{ab}y$, $Q_{1}^{\prime}=x\xrightarrow{a}y\land
x\xrightarrow{b}y$ and $Q_{2}^{\prime}=x\xrightarrow{a}y\land
x^{\prime}\xrightarrow{b}y^{\prime}$. We have
$Q_{1}^{\prime}\subseteq_{\textit{a-inj}}Q_{2}^{\prime}$ (and
$Q_{1}^{\prime}\subseteq_{st}Q_{2}^{\prime}$) but
$Q_{1}^{\prime}\not\subseteq_{\textit{q-inj}}Q_{2}^{\prime}$ as there cannot
be an injective homomorphism from the unique expansion of $Q^{\prime}_{2}$ to
the unique expansion of $Q^{\prime}_{1}$. On the other hand, we have
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$ (and $Q_{1}\subseteq_{st}Q_{2}$) but
$Q_{1}\not\subseteq_{\textit{a-inj}}Q_{2}$. Indeed, we can take the a-inj-
expansion $F$ of $Q_{1}$ obtained from $x\xrightarrow{a}y\land
y\xrightarrow{b}z$ by identifying $x$ and $z$. Then, there cannot be an atom-
injective homomorphism from the unique expansion of $Q_{2}$ to $F$.

In view of the characterizations above, in the sequel we will sometimes write
_st-expansions_ or _q-inj-expansions_ to denote a (normal) expansion. For
$\star\in\\{st,\textit{q-inj},\textit{a-inj}\\}$, we say that $E_{1}(\bar{y})$
is a _counter-example_ for $\star$-semantics if $E_{1}$ is a $\star$-expansion
of $Q_{1}$ such that $\bar{y}\not\in Q_{2}(E_{1})^{\star}$ (recall that any
CQ, in particular $E_{1}$, can be seen as a graph database). Note that the
latter condition $\bar{y}\not\in Q_{2}(E_{1})^{\star}$ is equivalent to the
non-existence of a (normal) expansion $E_{2}$ of $Q_{2}$ such that either (a)
$E_{2}\to E_{1}$ if $\star=st$; (b) $E_{2}\xrightarrow{\textit{inj}}E_{1}$ if
$\star=\textit{q-inj}$; or (c) $E_{2}\xrightarrow{\textit{a-inj}}E_{1}$ if
$\star=\textit{a-inj}$. Hence, $Q_{1}\not\subseteq_{\star}Q_{2}$ if, and only
if, there exists a counter-example for $\star$-semantics.

##  5\. Containment for unrestricted CRPQs

In this section we study the CRPQ/CRPQ containment problem under query-
injective and atom-injective semantics. We show that the former is in PSpace
while the latter is undecidable. Both proofs are non-trivial and provide novel
insights on how the semantics can be exploited for static analysis problems:
In the first case by reducing the space needed from exponential to polynomial,
and in the second case by enforcing counter-examples to witness solutions of
the PCP problem, through an intricate encoding.

The CRPQ/CRPQ containment problem for standard semantics is in ExpSpace
(Florescu et al., 1998) and all proofs (Florescu et al., 1998; Calvanese et
al., 2000; Figueira, 2020) of which we are aware reduce the problem to test
containment or universality on exponentially-sized NFA’s, encoding the set of
expansions or the set of (non-)counter-examples. The PSpace bound for query-
injective semantics is, however, quite different in nature, and uses some
exponential number of polynomial-sized certificates to ensure that the
containment holds.

###### Theorem 5.1.

The CRPQ/CRPQ containment problem under query-injective semantics is in
PSpace.

###### Proof sketch(full proof in Appendix C).

Let $Q_{1},Q_{2}$ be CRPQs; we want to test
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$. We only give a high-level description
of the proof due to space constraints. We will work with polynomial-sized
‘abstractions’ of expansions of $Q_{1}$. These abstractions contain, for each
atom $A$ of $Q_{1}$, all the information on how the languages of $Q_{2}$ can
be mapped into it. For example, it includes the information “there is a
partial run from state $q$ to state $q^{\prime}$ of the NFA $\mathcal{A}_{L}$
of language $L$ from $Q_{2}$ reading the expansion word of $A$”, or “there is
a partial run from the initial state of $\mathcal{A}_{L}$ to $q$ reading some
suffix of the expansion word of $A$”. Such an abstraction contains all the
necessary information needed to retain from an expansion to check whether it
is a counter-example. Indeed, any expansion having the same abstraction as a
counter-example will be a counter-example.

In order to test whether an abstraction $\alpha$ abstracts a counter-example,
we need to consider all possible ways of injectively mapping an expansion of
$Q_{2}$ to an expansion of $Q_{1}$. We call this a _morphism type_ , which
contains the information of where each atom expansion of $Q_{2}$ is mapped to.
For example, we can have the information that the path to which the expansion
of atom $A$ of $Q_{2}$ is mapped starts at some internal node of the expansion
of atom $A_{1}=x\xrightarrow{L_{1}}y$ of $Q_{1}$ then arrives to variable $y$
with state $q$ and continues reading the full expansion of atom
$A_{2}=y\xrightarrow{L_{2}}z$ arriving to variable $z$ with state
$q^{\prime}$, and it ends its journey by reading a prefix of the expansion of
atom $A_{3}=z\xrightarrow{L_{3}}t$ arriving to a final state at some internal
node. For each morphism type, we can check if it is _compatible_ with an
abstraction by checking, for example, that $\alpha$ indeed contains the
information of having a partial run from $q^{\prime}$ to a final state reading
a prefix of the expansion of $A_{3}$.

More concretely, consider the directed graph $\mathbf{G}$ consisting of
replacing each atom $A=x\xrightarrow{L}y$ of $Q_{1}$ with a path
$\pi^{\mathbf{G}}_{A}$ of length 3 (i.e., adding two new internal vertices). A
_morphism type_ from $Q_{2}$ to $Q_{1}$ is a pair $(H,h)$ such that
$h:H\xrightarrow{\textit{inj}}\mathbf{G}$ and $H$ is a graph resulting from
replacing each atom $A=x\xrightarrow{L}y$ of $Q_{2}$ with a path $\pi^{H}_{A}$
from $x$ to $y$. Figure 3 has an example of a morphism type.

Figure 3. Example of definition of $\mathbf{G}$ and morphism type $(H,h)$ from
$Q_{1},Q_{2}$. In this case, the injective morphism $h$ from $H$ to
$\mathbf{G}$ maps each node of $H$ to the node in the same position on
$\mathbf{G}$ (e.g., the lower-right node $r$ of $H$ maps to the lower-right
node of $\mathbf{G}$).

By injectivity, the size of $H$ in any morphism type is linearly bounded on
$Q_{1}$.

A morphism type $(H,h)$ is _compatible_ with an abstraction $\alpha$ if there
is a mapping $\lambda$ from the internal nodes of paths $\pi^{H}_{A}$ to
states of $A$, such that for every atom $A=x_{1}\xrightarrow{L}x_{2}$ of
$Q_{1}$, all the expected properties must hold. For example, if there is an
atom $A^{\prime}$ of $Q_{2}$ and an infix $\pi$ of the path
$\pi_{A^{\prime}}^{H}$ with $h(\pi)=\pi^{\mathbf{G}}_{A}$, then the
abstraction $\alpha$ ensures that there is a run of $\mathcal{A}_{A^{\prime}}$
from $\lambda(src(\pi))$ to $\lambda(tgt(\pi))$, where
$\mathcal{A}_{A^{\prime}}$ is the NFA of the language of $A^{\prime}$, and
$src(\pi)$ and $tgt(\pi)$ are the first and last nodes of $\pi$, respectively.
Or, as another example, one must also check that if there is an atom
$A^{\prime}$ of $Q_{2}$ and a suffix $\pi$ of $\pi^{H}_{A^{\prime}}$ with
$h(\pi)$ being a prefix of $\pi^{\mathbf{G}}_{A}$, then $\alpha$ ensures that
there is a run from $\lambda(src(\pi))$ to some final state in
$\mathcal{A}_{A^{\prime}}$ on the prefix of the expansion of $A$. There are
actually many other possible cases (17 in total), but each of these cases can
be easily checked with the information compiled in an abstraction.

The key property of compatibility is that it captures whether an abstraction
contains a $Q_{1}$-expansion which is a counter-example:

###### Claim 5.1.

The following are equivalent:

  1. (1)

There is a morphism type compatible with an abstraction $\alpha$;

  2. (2)

for every expansion $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ with
abstraction $\alpha$ there exists some expansion
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}E_{1}$;

  3. (3)

there is an expansion $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ with
abstraction $\alpha$ and an expansion
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}E_{1}$.

Finally, the PSpace algorithm guesses a mapping $\alpha$ from the atoms of
$Q_{1}$ to subsets of $P$, checks that $\alpha$ is an abstraction of $Q_{1}$,
and checks that there is no morphism type $(H,h)$ which is compatible with
$\alpha$. Due to the Claim above, if the algorithm succeeds, then any
expansion $E_{1}$ of $Q_{1}$ is a counter-example, and thus
$Q_{1}\not\subseteq_{\textit{q-inj}}Q_{2}$; otherwise, for every expansion
$E_{1}$ with abstraction $\alpha$ there is a compatible morphism type, which
means that $E_{1}$ is not a counter-example and hence
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$. ∎

On the other hand, the CRPQ/CRPQ containment problem for atom-injective
semantics becomes undecidable. Remarkably, the bound holds even when the
right-hand side query has no infinite languages, and both queries are of very
simple shape (cf. Figure 4).

###### Theorem 5.2.

The CRPQ/CRPQ and CRPQ/$\textsf{CRPQ}^{\textsf{fin}}$ containment problems
under atom-injective semantics are undecidable.

###### Proof sketch(full proof in Appendix D).

We reduce from the _Post Correspondence Problem_ (PCP), a well-known
undecidable problem. An instance of the PCP is a sequence of pairs
$(u_{1},v_{1}),\dots,(u_{\ell},v_{\ell})$, where $u_{i}$ and $v_{i}$ are non-
empty words over an alphabet $\Sigma$. The goal is to decide whether there is
a _solution_ , that is, a sequence $i_{1},\dots,i_{k}$ of indices from
$\\{1,\dots,\ell\\}$, with $k\geq 1$, such that the words $u_{i_{1}}\cdots
u_{i_{k}}$ and $v_{i_{1}}\cdots v_{i_{k}}$ coincide.

We provide a high-level description of the reduction. The idea is to construct
Boolean CRPQs $Q_{1}$ and $Q_{2}$ such that the PCP instance
$(u_{1},v_{1}),\dots,(u_{\ell},v_{\ell})$ has a solution if and only if
$Q_{1}\not\subseteq_{\textit{a-inj}}Q_{2}$. In particular, the PCP instance
has a solution if and only if there exists a counterexample for a-inj-
semantics, i.e., an a-inj-expansion $F$ of $Q_{1}$ such that there is no
expansion $E\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ with
$E\xrightarrow{\textit{a-inj}}F$. The general structure of $Q_{1}$ is shown in
Figure 4. We have a “middle” variable $x$, two “incoming” atoms and two
“outgoing” atoms:

$y_{1}\xrightarrow{L_{I}}x\land y_{2}\xrightarrow{\widehat{L}_{a}}x\land
x\xrightarrow{\widehat{L}_{I}}z_{1}\land x\xrightarrow{L_{a}}z_{2}$

Words in the languages $L_{I}$ and $\widehat{L}_{I}$ encode sequences of
indices from $\\{1,\dots,\ell\\}$, using special symbols from
$\mathbb{I}:=\\{I_{1},\dots,I_{\ell}\\}$ and
$\widehat{\mathbb{I}}:=\\{\widehat{I}_{1},\dots,\widehat{I}_{\ell}\\}$,
respectively. On the other hand, words from $L_{a}$ and $\widehat{L}_{a}$
encode sequences of words from $\\{u_{1},\dots,u_{\ell}\\}$ and
$\\{v_{1},\dots,v_{\ell}\\}$, using symbols from the PCP alphabet $\Sigma$ and
$\widehat{\Sigma}:=\\{\widehat{a}:a\in\Sigma\\}$, respectively. In the four
languages, we have some extra symbols to make the reduction work. We stress
that the finite alphabet used for the CRPQ $Q_{1}$ (and also for $Q_{2}$)
depends on the PCP instance.

Figure 4. The general structure of Boolean CRPQs $Q_{1}$ and $Q_{2}$ from the
reduction.

We are interested in a particular type of a-inj-expansions of $Q_{1}$ that we
call _well-formed_. The idea is that well-formed a-inj-expansions correspond
to solutions of the PCP instance. In particular, if there is a well-formed
a-inj-expansion of $Q_{1}$ then there is a solution to the PCP instance and
vice versa. We then construct $Q_{2}$ such that an a-inj-expansion of $Q_{1}$
is well-formed if and only if it is a counterexample for
$Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$.

Let $F$ be an a-inj-expansion of $Q_{1}$ such that $F=\widetilde{F}^{\equiv}$
for $\widetilde{F}=E\land J$ (here $E\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ and
$J$ are the equality atoms). The a-inj-expansion $F$ is _well-formed_ if it
satisfies four structural conditions we call $I$-$\widehat{I}$-, $I$-$a$-,
$\widehat{a}$-$\widehat{I}$-, and $\widehat{a}$-${a}$-condition. Intuitively,
the $I$-$\widehat{I}$-condition requires that the words $w_{I}\in L_{I}$ and
$\widehat{I}\in\widehat{L}_{I}$ chosen in the expansion $E$ encode the _same_
sequence of indices from $\\{1,\dots,\ell\\}$. On the other hand, the
$I$-$a$-condition ensures that the word $w_{a}\in L_{a}$, chosen in the
expansion $E$, encodes a sequence of words from $\\{u_{1},\dots,u_{\ell}\\}$
_according_ to the sequence encoded in $w_{I}\in L_{I}$. Similarly, the
$\widehat{a}$-$\widehat{I}$-condition requires that the chosen word
$\widehat{w}_{a}\in\widehat{L}_{a}$ encodes a sequence of words from
$\\{v_{1},\dots,v_{\ell}\\}$ according to $\widehat{w}_{I}\in\widehat{L}_{I}$.
Finally, the $\widehat{a}$-${a}$-condition requires that the chosen words
$w_{a}\in L_{a}$ and $\widehat{w}_{a}\in\widehat{L}_{a}$ “coincide” after
removing the $\,\widehat{\cdot}\,$ superscripts from $\widehat{w}_{a}$ and
focusing on the symbols from $\Sigma$. In other words, the
$\widehat{a}$-${a}$-condition ensures that the sequence of indices chosen by
$w_{I}$ (and $\widehat{w}_{I}$) is actually a solution to the PCP. In the four
cases, we additionally need to require some conditions on the equality atoms
$J$ to make the reduction work (see Figure 5 for an example).

Figure 5. Example of the $I$-$\widehat{I}$-condition of well-formed expansions
of $Q_{1}$. We show the expansions $y_{1}\xrightarrow{w_{I}}x$ and
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ of the atoms $y_{1}\xrightarrow{L_{I}}x$
and $x\xrightarrow{\widehat{L}_{I}}z_{1}$, respectively. The words
$w_{I}=\square\,\\#\,I_{2}\,\square\,\\#\,I_{5}$ and
$\widehat{w}_{I}=\widehat{I}_{5}\,\widehat{\\#}\,\widehat{\square}\,\widehat{I}_{2}\,\widehat{\\#}\,\widehat{\square}$
encode the sequence of indices $5,2$. Dotted blue lines indicate pairs of
equal variables while red lines indicate distinct variables. We have some
extra symbols $\\#,\widehat{\\#},\square,\widehat{\square}$.

The key property of well-formedness is that it can be characterized in terms
of the non-existence of a finite number of simple cycles and simple paths
having certain labels. Let us illustrate this for the case of the
$I$-$\widehat{I}$-condition and the expansion $F$ of Figure 5. The forbidden
labels for simple cycles are given by the finite language
$K_{I\widehat{I}}=\mathbb{I}\,\widehat{\mathbb{I}}$. In the case of simple
paths, these are given by $M_{I\widehat{I}}=\sum_{i\neq
j}I_{i}\widehat{I}_{j}\,+\widehat{\mathbb{I}}\,\\#\,+\widehat{\\#}\,\mathbb{I}\,+\\#\,\mathbb{I}\,\widehat{\mathbb{I}}\,\widehat{\\#}\,+\square\,\widehat{\square}$.
We have that an a-inj-expansion $F$ of $Q_{1}$ satisfies the
$I$-$\widehat{I}$-condition if and only if $F$ does not contain simple cycles
with labels in $K_{I\widehat{I}}$ nor simple paths with labels in
$M_{I\widehat{I}}$.

To see the backward direction, note that $t_{1}$ and $t_{1}^{\prime}$ cannot
be identified, otherwise we have a simple cycle from $t_{1}$ to itself with
label in $\mathbb{I}\,\widehat{\mathbb{I}}\subseteq K_{I\widehat{I}}$. Now,
the symbols $I_{5}$ and $\widehat{I}_{5}$ need to correspond to the same index
from $\\{1,\dots,\ell\\}$; otherwise we find a simple path from $t_{1}$ to
$t_{1}^{\prime}$ with label in $\sum_{i\neq j}I_{i}\widehat{I}_{j}\subseteq
M_{I\widehat{I}}$. To see the identification between $s_{1}$ and
$s_{1}^{\prime}$, note first that $t_{1}$ and $s_{1}^{\prime}$ cannot be
identified, as this would imply a simple path from $t_{1}^{\prime}$ to $x$
with label in $\widehat{\\#}\,\mathbb{I}\subseteq M_{I\widehat{I}}$.
Analogously, we have that $t_{1}^{\prime}$ and $s_{1}$ cannot be identified.
This implies that $s_{1}$ and $s_{1}^{\prime}$ are actually identified,
otherwise we have a simple path from $s_{1}$ to $s_{1}^{\prime}$ with label in
$\\#\,\mathbb{I}\,\widehat{\mathbb{I}}\,\widehat{\\#}\subseteq
M_{I\widehat{I}}$. Finally, $r_{1}$ and $r_{1}^{\prime}$ are identified,
otherwise there would be a simple path from $r_{1}$ to $r_{1}^{\prime}$ with
label in $\square\,\widehat{\square}\subseteq M_{I\widehat{I}}$. Note that we
can repeat this argument from “left-to-right” starting from
$r_{i}=r_{i}^{\prime}$ instead of $x$, and obtain the
$I$-$\widehat{I}$-condition. In order to ensure that the words $w_{I}$ and
$\widetilde{w}_{I}$ have the same length, we need to slightly modify the
construction of $Q_{1}$, $K_{I\widehat{I}}$ and $M_{I\widehat{I}}$(see
Appendix D for details). The forward direction follows directly from the
definition of the $I$-$\widehat{I}$-condition.

Since all the four conditions can be characterized via forbidden finite sets
of simple cycles and paths, it is possible to write two CRPQs from
$\textsf{CRPQ}^{\textsf{fin}}$ of the form
$Q_{2}^{\circlearrowright}=x\xrightarrow{K^{\circlearrowright}}x$ and
$Q_{2}^{\rightarrow}=y\xrightarrow{M^{\rightarrow}}z$ such that for every
a-inj-expansion $F$ of $Q_{1}$, $F$ is well-formed if and only if
$Q_{2}^{\circlearrowright}\lor
Q_{2}^{\rightarrow}(F)^{\textit{a-inj}}=\emptyset$, where
$Q_{2}^{\circlearrowright}\lor Q_{2}^{\rightarrow}$ is the _union_ of both
CRPQs. In particular, there is a solution to the PCP instance if and only if
$Q_{1}\not\subseteq_{\textit{a-inj}}Q_{2}^{\circlearrowright}\lor
Q_{2}^{\rightarrow}$. We finally show how to simulate the union
$Q_{2}^{\circlearrowright}\lor Q_{2}^{\rightarrow}$ with a single query
$Q_{2}\in\textsf{CRPQ}^{\textsf{fin}}$ as in Figure 4. ∎

##  6\. Containment for CRPQ subclasses

With the two previous results in place for the containment of unconstrained
CRPQs, we now explore the ${\mathcal{C}}_{1}$/${\mathcal{C}}_{2}$ containment
problem under all the possible semantics, where ${\mathcal{C}}_{1}$ and/or
${\mathcal{C}}_{2}$ belong to simpler classes of queries, namely either
Conjunctive Queries or CPRQs with no Kleene star (and hence with finite
languages).

In many cases one can apply or adapt previously established techniques or
reductions. There are, however, two noticeable exceptions: the lower bounds
for $\textsf{CRPQ}^{\textsf{fin}}$/CQ under query-injective semantics and for
CQ/$\textsf{CRPQ}^{\textsf{fin}}$ under atom-injective semantics. We highlight
only these two results. The remaining proofs can be found in Appendix F. In
particular, as mentioned in Section 4, almost all the results for the standard
semantics follow from previous work (in particular (Calvanese et al., 2000;
Florescu et al., 1998; Figueira et al., 2020)).

###### Theorem 6.1.

The $\textsf{CRPQ}^{\textsf{fin}}$/CQ containment problem under query-
injective semantics is $\Pi^{p}_{2}$-hard.

###### Proof.

We show that even when the languages of the left-hand query are unions of
alphabet symbols, $\Pi^{p}_{2}$ hardness still holds. We show a reduction from
the following problem on graphs, which is known to be
$\Sigma^{p}_{2}$-complete (Rutenburg, 1986, Theorem 5), to non-containment.
For a graph $G$ let $V(G)$ denote its sets of vertices and let
$G|_{V^{\prime}}$ denote the subgraph induced by $V^{\prime}\subseteq V(G)$.

Problem |  Generalized Two-Coloring Problem (GCP${}_{\text{2}}$)
---|---
Given |  An undirected graph $G$, a number $n\in\mathbb{N}$ (in unary).
Question |  Is there a partition $V_{1}\mathop{\dot{\cup}}V_{2}=V(G)$ s.t. neither $G|_{V_{1}}$ nor $G|_{V_{2}}$ contains an $n$-vertex clique as subgraph?

We will produce two Boolean queries $Q_{1},Q_{2}$ over the alphabet
$\mathbb{A}=\\{E,1,2,\\#\\}$ such that: (1)
$Q_{1}\not\subseteq_{\textit{q-inj}}Q_{2}$ iff the GCP${}_{\text{2}}$ instance
is positive; and (2) $Q_{2}$ is a CQ, and every language of $Q_{1}$ is a set
of one-letter words. Consider the input graph $G$, and the associated CQ
$Q_{G}$ on over the alphabet $\\{E\\}$, where for each edge $\\{u,v\\}$ in $G$
we have atoms $u\xrightarrow{E}v\land v\xrightarrow{E}u$ in $Q_{G}$.
Similarly, let $K_{n}$ be the CQ associated to the $n$-vertex clique. For a CQ
$Q$ and $i\in\\{1,2\\}$, let us define $i\textit{-ext}(Q)$ [resp.
$(1+2)\textit{-ext}(Q)$; $(12)\textit{-ext}(Q)$] as the extension of $Q$ by
adding one atom $x\xrightarrow{i}x$ [resp. one atom $x\xrightarrow{1+2}x$; two
atoms $x\xrightarrow{1}x\land x\xrightarrow{2}x$] for every variable
$x\in\textit{vars}(Q)$. We define $Q_{1},Q_{2}$ as in Figure 6.

Figure 6. Definition of $Q_{1}$ and $Q_{2}$ in terms of $G$ and $n$ for the
reduction of Theorem 6.1. The $\\#$-labeled thick arrows denote that there is
an atom $x\xrightarrow{\\#}y$ for each variable $x$ from the source query to
each variable $y$ of the target query.

On the one hand, if $Q_{1}\not\subseteq_{\textit{q-inj}}Q_{2}$ there must be
some expansion $E$ of $Q_{1}$ which is a counter-example. From $E$ we can
derive the partitioning $V_{1}\mathop{\dot{\cup}}V_{2}$ of $V(G)$ where
$V_{i}$ is the set of vertices labeled with an $i$-loop in the middle gadget
of $Q_{1}$. Now observe that, for every $i$, $K_{n}$ is not injectively mapped
to $G|_{V_{i}}$, as otherwise we would have that
$i\textit{-ext}(K_{n})\xrightarrow{\textit{inj}}E$, implying
$Q_{2}\xrightarrow{\textit{inj}}E$ and contradicting that $E$ is a counter-
example. This means that the GCP${}_{\text{2}}$ instance is positive. On the
other hand, if there is a partitioning $V_{1}\mathop{\dot{\cup}}V_{2}$ of
$V(G)$ avoiding the $n$-clique as a subgraph, then the corresponding expansion
$E$ of $Q_{1}$ (by choosing to have an $i$-loop for each node $x\in V_{i}$) is
such that $Q_{2}$ cannot be injectively mapped to $E$; in other words showing
that $E$ is a counter-example and thus
$Q_{1}\not\subseteq_{\textit{q-inj}}Q_{2}$. ∎

###### Theorem 6.2.

The CQ/$\textsf{CRPQ}^{\textsf{fin}}$ containment problem under atom-injective
semantics is $\Pi^{p}_{2}$-hard.

###### Proof sketch(full proof in Appendix E).

We show that even when all languages on the right-hand side are of the form
$\\{w\\}$ with $|w|\leq 2$ we have $\Pi^{p}_{2}$-hardness for containment. For
this, we show how to adapt the proof of $\Pi^{p}_{2}$-hardness of (Figueira et
al., 2020, Theorem 4.3), which shows $\Pi^{p}_{2}$-hardness for
$\textsf{CRPQ}^{\textsf{fin}}$/CQ containment for the standard semantics. We
reduce from $\forall\exists$-QBF (i.e., $\Pi_{2}$-Quantified Boolean
Formulas). Let $\Phi=\forall x_{1},\ldots,x_{n}\;\exists
y_{1},\ldots,y_{\ell}\;\varphi(x_{1},\ldots,x_{n},y_{1},\ldots,y_{\ell})$ be
an instance of $\forall\exists$-QBF such that $\varphi$ is quantifier-free and
in 3-CNF. We construct boolean queries $Q_{1}$ and $Q_{2}$ such that
$Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$ if, and only if, $\Phi$ is satisfiable.

The query $Q_{1}$ is defined in Figure 7, over the alphabet of labels
$\\{a,x_{1},\dots,\allowbreak x_{n},\allowbreak y_{1},\dots,\allowbreak
y_{\ell},\allowbreak t,f,r\\}$. We now explain how we define $Q_{2}$, over the
same alphabet. Every clause of $\Phi$ is represented by a subquery in $Q_{2}$,
as depicted in Figure 7. All nodes with identical label ($y_{1,t}$ and
$y_{1,f}$ in gadgets $D,E$) in the figures are the same node. Note that for
every clause and every existentially quantified literal $y_{i}$ therein we
have one node named $y_{i,tf}$ in $Q_{2}$. The $E$-gadget is designed such
that every represented literal can be homomorphically embedded, while exactly
one literal has to be embedded in the $D$-gadget.

The intuitive idea is that the valuation of the $x$-variables is given by the
a-inj-expansion $E_{1}$ of $Q_{1}$, whether the two nodes under $x$ incident
to $t$ are equal or not: if they are equal this corresponds to a _false_
valuation, otherwise a _true_ valuation. On the other hand, the valuation of
the $y$-variables is given by the homomorphism of an expansion of $Q_{2}$ into
$E_{1}$ (i.e., whether the corresponding node is mapped to the node
$y_{\mbox{\textvisiblespace},t}$ or $y_{\mbox{\textvisiblespace},f}$). The
homomorphism of $y$-variables across several clauses has to be consistent, as
all clauses share the same nodes $y_{\mbox{\textvisiblespace},tf}$, which
uniquely get mapped either into $y_{\mbox{\textvisiblespace},t}$ or
$y_{\mbox{\textvisiblespace},f}$. Hence, when the formula $\Phi$ is
satisfiable, for any assignment to the variables $\\{x_{i}\\}$ (given by the
choice of $t$/$f$ edges in $D$), there is a mapping from
$y_{\mbox{\textvisiblespace},tf}$ to one of $y_{\mbox{\textvisiblespace},f}$
or $y_{\mbox{\textvisiblespace},t}$. This gives
$Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$. Conversely, if an expansion of $Q_{2}$
can be mapped into $K$, then, for a choice of $t$/$f$ edges in $D$, we have an
embedding of each clause gadget of $Q_{2}$ in $K$. In particular, we can
always map a literal in each clause of $Q_{2}$ to $D$, ensuring that $\varphi$
is satisfied. As this is true for any expansion $K$ obtained by any $t$/$f$
assignment to $\\{x_{i}\\}$, we obtain that $\Phi$ is satisfiable.

Figure 7. Left: Query $Q_{1}$ used in Theorem 6.2 and the gadgets $D$, and $E$
used in its definition. The $\bar{r}$ blue edges depict the edges of the
complement of $r$ (i.e., the edges which are _not_ in relation $r$) for
clarity. Right: Example of $Q_{2}$ for $\varphi=(x_{2}\lor\lnot x_{5}\lor\lnot
y_{4})$.

∎

#### Other results

The remaining results are summarized on Figure 1 and the following theorem,
whose proofs can be found in Appendix F.

###### Theorem 6.3.

  1. (1)

The CQ/CRPQ and CQ/CQ containment problems are NP-complete under query-
injective semantics. (Proposition F.2 in Appendix F.)

  2. (2)

The CQ/CQ containment problem under atom-injective semantics is NP-complete.
(Corollary F.4 in Appendix F.)

  3. (3)

The CRPQ/CQ and $\textsf{CRPQ}^{\textsf{fin}}$/CQ containment problems are
$\Pi^{p}_{2}$-hard, under standard and atom-injective semantics. (Proposition
F.6 in Appendix F.)

  4. (4)

The CRPQ/CQ and $\textsf{CRPQ}^{\textsf{fin}}$/CQ containment problems are in
$\Pi^{p}_{2}$, under all semantics. (Proposition F.7 in Appendix F.)

  5. (5)

The CRPQ/$\textsf{CRPQ}^{\textsf{fin}}$ containment problem is PSpace-hard
under all semantics. (Proposition F.8 in Appendix F.)

  6. (6)

The CRPQ/$\textsf{CRPQ}^{\textsf{fin}}$ containment problem is in PSpace under
standard semantics. (Proposition F.9 in Appendix F.)

  7. (7)

The $\textsf{CRPQ}^{\textsf{fin}}$/CRPQ containment problem is in
$\Pi^{p}_{2}$, under all semantics. (Proposition F.10 in Appendix F.)

##  7\. Discussion and Outlook

We have defined two possible injective semantics for CRPQs, providing two ways
to extend the simple-path semantics of RPQs to the realm of CRPQs. On these
semantics, we have shown that the containment problem differs drastically from
the standard semantics, in some cases improving the complexity, and in some
cases making the problem directly undecidable.

Both of these semantics are natural generalizations of simple-path semantics
of RPQs. For instance, if we revert the role of edges and nodes, CRPQs under
atom-injective semantics is present in the popular graph database Neo4j. While
query-injective semantics is less common in practice, we still believe that
this semantics, and in particular, looking for disjoint paths, may be useful
for users and may provide an interesting feature for graph query languages.
Further empirical investigation is needed to assess the practical usefulness
of these two semantics.

While the fragments of the class of CRPQs we have studied are probably the
three most fundamental subclasses, there are other more fine-grained fragments
based on the form of regular expressions used in the CRPQs, which are
practically very relevant (Bonifati et al., 2020, 2019). These fragments have
been studied under standard semantics (Figueira et al., 2020), and it would be
interesting to understand how they behave under injective semantics. A
different direction is to consider larger classes of queries, understanding
how injective semantics are extended, and the impact on the bounds for
containment – such as CRPQ with two-way navigation and union (UC2RPQ)
(Calvanese et al., 2000), Extended CRPQ (ECRPQ) (Barceló et al., 2012), or
Regular Queries (Reutter et al., 2017).

We have limited our investigation to (extensions of) the simple-path
semantics. Another possibility is to consider _trail_ semantics, which can be
extended in a similar way to CRPQs, obtaining again two alternative semantics:
query-edge-injective and atom-edge-injective, based on the notion of edge-
injective homomorphisms. Many of our results can be extended to these
semantics, and we suspect that complexities for query-edge-injective and
query-injective coincide on all studied fragments, and likewise for atom-edge-
injective and atom-injective. In particular, while neither the undecidability
nor the PSpace upper-bound seem to go through when simply reversing the role
of nodes and edges, we believe that both proofs can be adapted.

One possible research direction is on another fundamental static analysis
problem for CRPQs, namely the _boundedness_ problem, which checks whether a
CRPQ is equivalent to a finite union of CQs. This problem is decidable for
standard semantics (Barceló et al., 2019).

## References

  * (1)
  * Angles et al. (2018) Renzo Angles, Marcelo Arenas, Pablo Barceló, Peter A. Boncz, George H. L. Fletcher, Claudio Gutiérrez, Tobias Lindaaker, Marcus Paradies, Stefan Plantikow, Juan F. Sequeda, Oskar van Rest, and Hannes Voigt. 2018.  G-CORE: A Core for Future Graph Query Languages. In _Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, June 10-15, 2018_ , Gautam Das, Christopher M. Jermaine, and Philip A. Bernstein (Eds.). ACM, 1421–1432.  https://doi.org/10.1145/3183713.3190654
  * Angles et al. (2017) Renzo Angles, Marcelo Arenas, Pablo Barceló, Aidan Hogan, Juan Reutter, and Domagoj Vrgoč. 2017\.  Foundations of Modern Query Languages for Graph Databases.  _ACM Comput. Surv._ 50, 5, Article 68 (sep 2017), 40 pages.  https://doi.org/10.1145/3104031
  * Bagan et al. (2020) Guillaume Bagan, Angela Bonifati, and Benoît Groz. 2020\.  A trichotomy for regular simple path queries on graphs.  _J. Comput. Syst. Sci._ 108 (2020), 29–48.  https://doi.org/10.1016/j.jcss.2019.08.006
  * Barceló (2013) Pablo Barceló. 2013\.  Querying graph databases. In _Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY, USA - June 22 - 27, 2013_ , Richard Hull and Wenfei Fan (Eds.). ACM, 175–188.  https://doi.org/10.1145/2463664.2465216
  * Barceló et al. (2019) Pablo Barceló, Diego Figueira, and Miguel Romero. 2019\.  Boundedness of Conjunctive Regular Path Queries. In _International Colloquium on Automata, Languages and Programming (ICALP)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 132)_. Leibniz-Zentrum für Informatik, 104:1–104:15.  https://doi.org/10.4230/LIPIcs.ICALP.2019.104
  * Barceló et al. (2012) Pablo Barceló, Leonid Libkin, Anthony Widjaja Lin, and Peter T. Wood. 2012.  Expressive Languages for Path Queries over Graph-Structured Data.  _ACM Trans. Database Syst._ 37, 4 (2012), 31:1–31:46.  https://doi.org/10.1145/2389241.2389250
  * Bonifati et al. (2019) Angela Bonifati, Wim Martens, and Thomas Timm. 2019\.  Navigating the Maze of Wikidata Query Logs. In _World Wide Web Conference (WWW)_. 127–138.
  * Bonifati et al. (2020) Angela Bonifati, Wim Martens, and Thomas Timm. 2020\.  An Analytical Study of Large SPARQL Query Logs.  _VLDB Journal_ (2020).  To appear, https://doi.org/10.1007/s00778-019-00558-9.
  * Calvanese et al. (2000) Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. 2000.  Containment of Conjunctive Regular Path Queries with Inverse. In _Principles of Knowledge Representation and Reasoning (KR)_. 176–185.
  * Chandra and Merlin (1977) Ashok K. Chandra and Philip M. Merlin. 1977.  Optimal Implementation of Conjunctive Queries in Relational Data Bases. In _Proceedings of the 9th Annual ACM Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, USA_ , John E. Hopcroft, Emily P. Friedman, and Michael A. Harrison (Eds.). ACM, 77–90.  https://doi.org/10.1145/800105.803397
  * Cook (1971) Stephen A. Cook. 1971\.  The Complexity of Theorem-Proving Procedures. In _Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA_ , Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman (Eds.). ACM, 151–158.  https://doi.org/10.1145/800157.805047
  * Cruz et al. (1987) Isabel F. Cruz, Alberto O. Mendelzon, and Peter T. Wood. 1987\.  A Graphical Query Language Supporting Recursion. In _Proceedings of the Association for Computing Machinery Special Interest Group on Management of Data 1987 Annual Conference, San Francisco, CA, USA, May 27-29, 1987_ , Umeshwar Dayal and Irving L. Traiger (Eds.). ACM Press, 323–330.  https://doi.org/10.1145/38713.38749
  * Deutsch et al. (2022) Alin Deutsch, Nadime Francis, Alastair Green, Keith Hare, Bei Li, Leonid Libkin, Tobias Lindaaker, Victor Marsault, Wim Martens, Jan Michels, Filip Murlak, Stefan Plantikow, Petra Selmer, Oskar van Rest, Hannes Voigt, Domagoj Vrgoč, Mingxi Wu, and Fred Zemke. 2022\.  Graph Pattern Matching in GQL and SQL/PGQ. In _Proceedings of the 2022 International Conference on Management of Data_ _(SIGMOD ’22)_. 2246–2258.  https://doi.org/10.1145/3514221.3526057
  * Figueira (2020) Diego Figueira. 2020\.  Containment of UC2RPQ: the hard and easy cases. In _International Conference on Database Theory (ICDT)_ _(Leibniz International Proceedings in Informatics (LIPIcs))_. Leibniz-Zentrum für Informatik.
  * Figueira et al. (2020) Diego Figueira, Adwait Godbole, S. Krishna, Wim Martens, Matthias Niewerth, and Tina Trautner. 2020\.  Containment of Simple Conjunctive Regular Path Queries. In _Principles of Knowledge Representation and Reasoning (KR)_.  https://hal.archives-ouvertes.fr/hal-02505244
  * Florescu et al. (1998) Daniela Florescu, Alon Levy, and Dan Suciu. 1998.  Query Containment for Conjunctive Queries with Regular Expressions. In _ACM Symposium on Principles of Database Systems (PODS)_. ACM Press, 139–148.  https://doi.org/10.1145/275487.275503
  * Francis et al. (2018) Nadime Francis, Alastair Green, Paolo Guagliardo, Leonid Libkin, Tobias Lindaaker, Victor Marsault, Stefan Plantikow, Mats Rydberg, Petra Selmer, and Andrés Taylor. 2018\.  Cypher: An Evolving Query Language for Property Graphs. In _Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, June 10-15, 2018_ , Gautam Das, Christopher M. Jermaine, and Philip A. Bernstein (Eds.). ACM, 1433–1445.  https://doi.org/10.1145/3183713.3190657
  * Garey and Johnson (1979) M. R. Garey and David S. Johnson. 1979.  _Computers and Intractability: A Guide to the Theory of NP-Completeness_.  W. H. Freeman.
  * GQL (2021) GQL 2021.  GQL standard website.  https://www.gqlstandards.org/.
  * Harris and Seaborne (2013) Steve Harris and Andy Seaborne. 2013.  SPARQL 1.1 Query Language. http://www.w3.org/TR/sparql11-query.
  * Kozen (1977) Dexter Kozen. 1977\.  Lower Bounds for Natural Proof Systems. In _Annual Symposium on Foundations of Computer Science (FOCS)_. IEEE Computer Society Press, 254–266.  https://doi.org/10.1109/SFCS.1977.16
  * Losemann and Martens (2013) Katja Losemann and Wim Martens. 2013.  The complexity of regular expressions and property paths in SPARQL.  _ACM Trans. Database Syst._ 38, 4 (2013), 24:1–24:39.  https://doi.org/10.1145/2494529
  * Malyshev et al. (2018) Stanislav Malyshev, Markus Krötzsch, Larry González, Julius Gonsior, and Adrian Bielefeldt. 2018\.  Getting the Most Out of Wikidata: Semantic Technology Usage in Wikipedia’s Knowledge Graph. In _International Semantic Web Conference (ISWC)_. 376–394.
  * Martens and Popp (pear) Wim Martens and Tina Popp. 2022. To appear.  The Complexity of Regular Trail and Simple Path Queries on Undirected Graphs. In _ACM Symposium on Principles of Database Systems (PODS)_. ACM.
  * Martens and Trautner (2019) Wim Martens and Tina Trautner. 2019.  Dichotomies for Evaluating Simple Regular Path Queries.  _ACM Trans. Database Syst._ 44, 4 (2019), 16:1–16:46.  https://doi.org/10.1145/3331446
  * Mendelzon and Wood (1995) Alberto O. Mendelzon and Peter T. Wood. 1995.  Finding Regular Simple Paths in Graph Databases.  _SIAM J. Comput._ 24, 6 (1995), 1235–1258.  https://doi.org/10.1137/S009753979122370X
  * Reutter et al. (2017) Juan L. Reutter, Miguel Romero, and Moshe Y. Vardi. 2017\.  Regular Queries on Graph Databases.  _Theory Comput. Syst._ 61, 1 (2017), 31–83.  https://doi.org/10.1007/s00224-016-9676-2
  * Rutenburg (1986) Vladislav Rutenburg. 1986\.  Complexity of Generalized Graph Coloring. In _Mathematical Foundations of Computer Science 1986, Bratislava, Czechoslovakia, August 25-29, 1996, Proceedings_ _(Lecture Notes in Computer Science, Vol. 233)_ , Jozef Gruska, Branislav Rovan, and Juraj Wiedermann (Eds.). Springer, 573–581.  https://doi.org/10.1007/BFb0016284
  * Sakr et al. (2021) Sherif Sakr, Angela Bonifati, Hannes Voigt, Alexandru Iosup, Khaled Ammar, Renzo Angles, Walid Aref, Marcelo Arenas, Maciej Besta, Peter A. Boncz, Khuzaima Daudjee, Emanuele Della Valle, Stefania Dumbrava, Olaf Hartig, Bernhard Haslhofer, Tim Hegeman, Jan Hidders, Katja Hose, Adriana Iamnitchi, Vasiliki Kalavri, Hugo Kapp, Wim Martens, M. Tamer Özsu, Eric Peukert, Stefan Plantikow, Mohamed Ragab, Matei R. Ripeanu, Semih Salihoglu, Christian Schulz, Petra Selmer, Juan F. Sequeda, Joshua Shinavier, Gábor Szárnyas, Riccardo Tommasini, Antonino Tumeo, Alexandru Uta, Ana Lucia Varbanescu, Hsiang-Yun Wu, Nikolay Yakovets, Da Yan, and Eiko Yoneki. 2021.  The Future is Big Graphs: A Community View on Graph Processing Systems.  _Commun. ACM_ 64, 9 (aug 2021), 62–71.  https://doi.org/10.1145/3434642

##  Appendix A Appendix to Section 2

###### Proof of Proposition 2.2.

The result is well-known for the case of standard semantics so we focus on
query-injective semantics. Suppose $G=(V,E)$ and $Q$ is of the form
$Q(\bar{x})=A_{1}\land\dots\land A_{m}$. Recall $Q(\bar{x})$ is equivalent to
a union $\mathcal{Q}_{\varepsilon-free}$ of $\varepsilon$-free CRPQs. Assume
first that $\bar{v}\in Q(G)^{\textit{q-inj}}$. Then $\bar{v}\in
Q^{\prime}(G)^{\textit{q-inj}}$ for some
$Q^{\prime}\in\mathcal{Q}_{\varepsilon-free}$ of the form
$Q^{\prime}(\bar{z})=A^{\prime}_{1}\land\dots\land A^{\prime}_{k}$. Without
loss of generality, assume $A_{k+1},\dots,A_{m}$ are precisely the atoms of
$Q$ collapsed in the construction of $Q^{\prime}$ (that is, we take the
$\varepsilon$-word on those atoms). In particular, the language of the atom
$A^{\prime}_{i}$ is the language of $A_{i}$ minus $\varepsilon$, for
$i\in\\{1,\dots,k\\}$. There exists then an injective mapping $\mu$ from
$\textit{vars}(Q^{\prime})$ to $V$ (satisfying $\mu(\bar{z})=\bar{v}$), and
for each atom $A^{\prime}_{i}=x_{i}\xrightarrow{L_{i}^{\prime}}y_{i}$, a
simple path $\pi_{i}$ from $\mu(x_{i})$ to $\mu(y_{i})$ such that distinct
paths do not share internal nodes. We can take the expansion
$E\in\textup{{Exp}}^{\mathit{}}(Q)$ produced by the expansion profile of $Q$
that maps $A_{i}$ to the word $\varepsilon$, if $i\in\\{k+1,\dots,m\\}$, and
maps $A_{i}$ to the label of $\pi_{i}$, for $i\in\\{1,\dots,k\\}$. We can
define a homomorphism $h:E\to(G,\bar{v})$ by mapping the non-internal
variables of $E$ according to $\mu$ and each atom expansion to the
corresponding simple path in $G$. As the paths do not share internal nodes
this is an injective homomorphism, and hence
$E\xrightarrow{\textit{inj}}(G,\bar{v})$.

For the other direction, suppose that
$h:E\xrightarrow{\textit{inj}}(G,\bar{v})$ for some expansion
$E\in\textup{{Exp}}^{\mathit{}}(Q)$. Let $\varphi$ be the expansion profile
generating $E$. We construct an $\varepsilon$-free CRPQ
$Q^{\prime}\in\mathcal{Q}_{\varepsilon-free}$ as follows: if $\varphi$ assigns
the word $\varepsilon$ to $A_{i}$, then collapse $A_{i}$, otherwise, remove
$\varepsilon$ from its language. Suppose that $Q^{\prime}$ is of the form
$Q^{\prime}(\bar{z})=A^{\prime}_{1}\land\dots\land A^{\prime}_{k}$. We have
that $\bar{v}\in Q^{\prime}(G)^{\textit{q-inj}}$. Indeed, define the mapping
$\mu:\textit{vars}(Q^{\prime})\to V$ as the restriction of $h$ to the non-
internal variables of $E$, and define the path $\pi_{i}$ to be the image via
$h$ of the expansion of the atom $A^{\prime}_{i}$ in $E$. Since $h$ is
injective, the $\pi_{i}$’s are simple paths and do not share internal nodes.
Moreover, the mapping $\mu$ is injective. Hence $\bar{v}\in
Q^{\prime}(G)^{\textit{q-inj}}$, which implies that $\bar{v}\in
Q(G)^{\textit{q-inj}}$ as required.

∎

###### Proof of Proposition 2.3.

The proof is analogous to the proof of Proposition 2.2, replacing injective
homomorphisms by atom-injective homomorphisms. ∎

##  Appendix B Appendix to Section 4

###### Proof of Proposition 4.3.

The proof is identical to the proof of Proposition 4.2 replacing homomorphisms
by injective homomorphisms. For the sake of completeness, we give the proof
below.

Assume $Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$ and take
$E_{1}(\bar{y})\in\textup{{Exp}}^{\mathit{}}(Q_{1})$. Recall that we can see
the query $E_{1}(\bar{y})$ as a graph database (of the same name) where each
atom is interpreted as an edge. We have
$E_{1}\xrightarrow{\textit{inj}}(E_{1},\bar{y})$ and hence $\bar{y}\in
Q_{1}(E_{1})^{\textit{q-inj}}$. By hypothesis, $\bar{y}\in
Q_{2}(E_{1})^{\textit{q-inj}}$, that is, there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}(E_{1},\bar{y})$, i.e,
$E_{2}\xrightarrow{\textit{inj}}E_{1}$. For the other direction, assume
$\bar{v}\in Q_{1}(G)^{\textit{q-inj}}$ for some graph database $G$ and tuple
$\bar{v}$ of nodes. There is an expansion
$E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ such that
$E_{1}\xrightarrow{\textit{inj}}(G,\bar{v})$. By hypothesis, there exists
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ with
$E_{2}\xrightarrow{\textit{inj}}E_{1}$. By composition, we obtain
$E_{2}\xrightarrow{\textit{inj}}(G,\bar{v})$, hence $\bar{v}\in
Q_{2}(G)^{\textit{q-inj}}$. ∎

###### Proof of Lemma 4.4.

We start with (1)$\Rightarrow$(2). Let $h$ be a witness for
$E\xrightarrow{\textit{a-inj}}(G,\bar{v})$. Define the query
$\widetilde{F}=E\land J$ where $J$ is the conjunction of all equality atoms
$x=y$ with $x,y\in\textit{vars}(E)$ and $h(x)=h(y)$. Since $h$ is atom-
injective, we have
$F:=\widetilde{F}^{\equiv}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q)$.
Moreover, there is $g:F\xrightarrow{\textit{inj}}(G,\bar{v})$ as required.
Indeed, let $\Phi:\textit{vars}(E)\to\textit{vars}(F)$ be the canonical
renaming. For each $x\in\textit{vars}(F)$, we set $g(x)=h(x^{\prime})$, where
$x^{\prime}$ is any variable in $E$ with $\Phi(x^{\prime})=x$. By
construction, $g$ is an injective homomorphism. Conversely, suppose
$F=\widetilde{F}^{\equiv}$ for $\widetilde{F}=E\land J$ with expansion
$E\in\textup{{Exp}}^{\mathit{}}(Q)$ and let $g$ be a witness for
$F\xrightarrow{\textit{inj}}(G,\bar{v})$. Let
$\Phi:\textit{vars}(E)\to\textit{vars}(F)$ be the canonical renaming. Observe
that $\Phi$ is actually a homomorphism from $E$ to $F$. By definition of
a-inj-expansions, $\Phi$ is an atom-injective homomorphism from $E$ to $F$. By
composing $\Phi$ with $g$ we obtain
$E\xrightarrow{\textit{a-inj}}(G,\bar{v})$. The case of $E^{\prime}$ instead
of $G$ is analogous. ∎

###### Proof of Proposition 4.6.

By Lemma 4.4 it suffices to consider the equivalence between items (1) and
(2). Suppose first $Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$ and take
$F_{1}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q_{1})$. We can see
$F_{1}(\bar{y})$ as a graph database (of the same name) where each atom is
interpreted as an edge. We have
$F_{1}\xrightarrow{\textit{inj}}(F_{1},\bar{y})$ and, by Corollary 4.5, we
obtain $\bar{y}\in Q_{1}(F_{1})^{\textit{a-inj}}$. By hypothesis, $\bar{y}\in
Q_{2}(F_{1})^{\textit{a-inj}}$, that is, there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{a-inj}}(F_{1},\bar{y})$, i.e,
$E_{2}\xrightarrow{\textit{a-inj}}F_{1}$. For the other direction, assume
$\bar{v}\in Q_{1}(G)^{\textit{a-inj}}$ for some graph database $G$ and tuple
$\bar{v}$ of nodes. By Corollary 4.5, there is
$F_{1}\in\textup{{Exp}}^{\mathit{\textit{a-inj}}}(Q_{1})$ and
$g:F_{1}\xrightarrow{\textit{inj}}(G,\bar{v})$. By hypothesis, there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ and
$f:E_{2}\xrightarrow{\textit{a-inj}}F_{1}$. By composing $f$ with $g$ we
obtain that $E_{2}\xrightarrow{\textit{a-inj}}(G,\bar{v})$. We conclude that
$\bar{v}\in Q_{2}(G)^{\textit{a-inj}}$. ∎

##  Appendix C Full proof of Theorem 5.1

Let $Q_{1}(\bar{x}_{1}),Q_{2}(\bar{x}_{2})$ be CRPQs; we want to test
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$.

We often blur the distinction between a CRPQ and an edge-labeled graph, whose
edges are regular expressions. Hence, the _degree_ [resp.  _in-degree_ ; _out-
degree_] of a variable is the number of atoms containing it [resp. as a second
variable; as a first variable].

_High-level idea._ We first give a high-level description of the proof. We
will work with polynomial-sized ‘abstractions’ of expansions of $Q_{1}$. These
abstractions contain, for each atom $A$ of $Q_{1}$, all the information on how
the languages of $Q_{2}$ can be mapped into it. For example, it includes the
information “there is a partial run from state $q$ to state $q^{\prime}$ of
the NFA $\mathcal{A}_{L}$ of language $L$ from $Q_{2}$ reading the expansion
word of $A$”, or “there is a partial run from the initial state of
$\mathcal{A}_{L}$ to $q$ reading some suffix of the expansion word of $A$”.
Such an abstraction contains all the necessary information needed to retain
from an expansion to check if it is a counter-example. Indeed, any expansion
with the same abstraction as a counter-example will be a counter-example.

In order to test whether an abstraction $\alpha$ abstracts a counter-example,
we need to consider all possible ways of injectively mapping an expansion of
$Q_{2}$ to an expansion of $Q_{1}$. We call this _morphism type_ , which
contains the information of where each atom expansion of $Q_{2}$ is mapped.
For example, we can have the information that the path to which the expansion
of atom $A$ of $Q_{2}$ is mapped starts at some internal node of the expansion
of atom $A_{1}=x\xrightarrow{L_{1}}y$ of $Q_{1}$ then arrives to variable $y$
with state $q$ and continues reading the full expansion of atom
$A_{2}=y\xrightarrow{L_{2}}z$ arriving to variable $z$ with state
$q^{\prime}$, and it ends its journey by reading a prefix of the expansion of
atom $A_{3}=z\xrightarrow{L_{3}}t$ arriving to a final state at some internal
node. For each morphism type, we can check if it is _compatible_ with an
abstraction by checking, for example, that $\alpha$ indeed contains the
information of having a partial run from $q^{\prime}$ to a final state reading
a prefix of the expansion of $A_{3}$.

The important property is that an abstraction $\alpha$ is compatible with a
morphism type $\tau$ iff for every expansion $E_{1}$ of $Q_{1}$ with
abstraction $\alpha$ there is an expansion $E_{2}$ of $Q_{2}$ with morphism
type $\tau$ such that $E_{2}\xrightarrow{\textit{inj}}E_{1}$. Hence, the
PSpace algorithm simply guesses $\alpha$ and checks that $\alpha,\tau$ are not
compatible, for every possible morphism type $\tau$. We now give some more
details for these ideas.

###### Remark C.1.

Any CRPQ is q-inj-equivalent to one in which there is no variable $y$ incident
to two atoms, with in-degree and out-degree equal to one. This is because
$x\xrightarrow{L}y\land y\xrightarrow{L^{\prime}}x^{\prime}$ is equivalent
(under q-inj or standard semantics) to $x\xrightarrow{L\cdot
L^{\prime}}x^{\prime}$ (assuming $y\not\in\\{x,x^{\prime}\\}$).

Due to Remark C.1, we can assume that the mapping from the expansion of
$Q_{2}$ to the expansion of $Q_{1}$ is such that no two variables can be
mapped to two internal nodes of an atom expansion.

###### Remark C.2.

For every CRPQ $Q$ one can produce an equivalent union $Q^{\prime}$ of CRPQs
such that (i) no language of $Q^{\prime}$ contains $\varepsilon$ and (ii)
there are no two distinct atoms $x\xrightarrow{L}y$ and
$x\xrightarrow{L^{\prime}}y$ in $Q^{\prime}$ with some single-letter word
$a\in\mathbb{A}$ in $L\cap L^{\prime}$. Further, $Q^{\prime}$ is an
exponential union of polynomial-sized CRPQs, and testing whether a CRPQ is in
the union is in PSpace.

_Terminology._ By _path_ (of an expansion or directed graph) we mean a
directed path, that is, a sequence of edges of the form
$\pi=(v_{0},v_{1})(v_{1},v_{2})\dotsb(v_{n-1},v_{n})$. An _internal node_ of a
path is any node excluding the initial and final ones (i.e., $v_{0}$ and
$v_{n}$). For a path $\pi$, and a morphism $h$, we denote by $h(\pi)$ the path
obtained by replacing each vertex $v$ with $h(v)$. For a (directed) path
$\pi$, we denote by _$src(\pi)$ [resp. $tgt(\pi)$]_ the first [resp. last]
vertex. A _subpath_ of a path $\pi$ as above, is a path of the form
$(v_{i},v_{i+1})\dotsb(v_{j},v_{j+1})$ where $0\leq i\leq j<n$ (in particular
of length at least 1). An _infix [resp. prefix, suffix]_ of a path of $\pi$ is
a subpath which does not contain $src(\pi)$ or $tgt(\pi)$ [resp. contains
$tgt(\pi)$ and excludes $src(\pi)$, contains $src(\pi)$ and excludes
$tgt(\pi)$]. We often blur the distinction between regular languages, regular
expressions, NFA, and CRPQ atoms containing a regular language. For instance,
we may write “$q$ is a final state of atom $x\xrightarrow{L}y$”, meaning that
it is a final state of the NFA representing $L$.

_Restriction of queries._ To simplify the proof, we will assume that
$Q_{1},Q_{2}$ have the following properties:

  * •

there is no $\varepsilon$ in any of the languages;

  * •

there are no two atoms $x\xrightarrow{L}y$ and $x\xrightarrow{L^{\prime}}y$
with some single-letter word $a\in\mathbb{A}$ in $L\cap L^{\prime}$;

  * •

the queries are connected.

We will later show how to lift these assumptions.

###### Remark C.3.

As a consequence of Remark C.1, for the CRPQ/CRPQ containment problem of
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$ under q-inj semantics, and assuming the
properties above, we can restrict our attention to injective homomorphisms
$E_{1}\xrightarrow{\textit{inj}}E_{1}$ (where
$E_{i}\in\textup{{Exp}}^{\mathit{}}(Q_{i})$) such that if two distinct
variables $x,y\in\textit{vars}(Q_{1})$ are mapped to distinct internal nodes
of an atom expansion, then they must both be of degree 1. That is, in view of
the characterization of Proposition 4.3,
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$ iff for every
$E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ there is
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$h:E_{2}\xrightarrow{\textit{inj}}E_{1}$, where $h$ has the property above.

Without any loss of generality, let us assume that all the NFA of the
languages of $Q_{2}$ have pairwise disjoint sets of states, and that they are
complete and co-complete (i.e., for every letter and state there is an
incoming and an outgoing transition with that letter). Let us consider
$\mathcal{A}_{Q_{2}}$ as an automaton having as transitions the (disjoint)
union of all the transitions for the automata of $Q_{2}$. In this context we
will denote by _initial state_ [resp.  _final state_] a state which is initial
[resp. final] in the automaton from which it comes.

An _abstraction of an expansion_ $E_{1}$ of $Q_{1}$ is a mapping $\alpha$ from
the atoms of $Q_{1}$ to subsets of $P$, where

$\displaystyle P={}$ $\displaystyle\\{\langle
q\text{-}q^{\prime}\rangle:q,q^{\prime}\text{ states of
}\mathcal{A}_{Q_{2}}\\}\cup{}\\{\langle
q\text{-}\\!{|}\\!\text{-}q^{\prime}\rangle:q,q^{\prime}\text{ states of
}\mathcal{A}_{Q_{2}}\\}\cup{}$ $\displaystyle\\{\langle
q\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}q^{\prime}\rangle:q,q^{\prime}\text{
states of
}\mathcal{A}_{Q_{2}}\\}\cup{}\\{\langle{\cdot}{\cdot}q\text{-}q^{\prime}{\cdot}{\cdot}\rangle:q,q^{\prime}\text{
states of }\mathcal{A}_{Q_{2}}\\}$

such that for every expansion $x\xrightarrow{w}y$ of an atom $A$ we have:

  * •

$\langle q\text{-}q^{\prime}\rangle\in\alpha(A)$ if there is a partial run of
$\mathcal{A}_{Q_{2}}$ from $q$ to $q^{\prime}$ reading $w$;

  * •

$\langle q\text{-}\\!{|}\\!\text{-}q^{\prime}\rangle\in\alpha(A)$ if for some
$w=u\cdot v$ with $u,v\neq\varepsilon$ there is a partial run of
$\mathcal{A}_{Q_{2}}$ from $q$ to a final state reading $u$, and a partial run
from an initial state to $q^{\prime}$ reading $v$;

  * •

$\langle
q\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}q^{\prime}\rangle\in\alpha(A)$ if
for some $w=u\cdot s\cdot v$ with $s,u,v\neq\varepsilon$ there is a partial
run of $\mathcal{A}_{Q_{2}}$ from $q$ to a final state reading $u$, and a
partial run of $\mathcal{A}_{Q_{2}}$ from an initial state to $q^{\prime}$
reading $v$;

  * •

$\langle{\cdot}{\cdot}q\text{-}q^{\prime}{\cdot}{\cdot}\rangle\in\alpha(A)$ if
for some $w=u\cdot s\cdot v$ with $s,u,v\neq\varepsilon$ there is a partial
run of $\mathcal{A}_{Q_{2}}$ from $q$ to $q^{\prime}$ reading $s$.

Observe that the size of any abstraction is polynomial in $Q_{1},Q_{2}$.

The set of _abstractions of $Q_{1}$_, is the set of abstractions of all its
expansions.

###### Claim C.1.

Testing whether a mapping is an abstraction of $Q_{1}$ is in PSpace.

Indeed, a standard pumping argument shows that if $\alpha$ is an abstraction
of $Q_{1}$, it has a witnessing expansion of at most exponential size. Using
this bound, an on-the-fly PSpace algorithm can guess the expansion for each
atom and check that each atom $A$ has abstraction $\alpha(A)$. This is done by
guessing one letter at a time while keeping track of all possible partial runs
it contains. The procedure also keeps a poly-sized counter to keep track of
the size of the expansion being produced, and rejects the computation whenever
the size exceeds the exponential bound.

Consider the directed graph $\mathbf{G}$ consisting of replacing each atom
$A=x\xrightarrow{L}y$ of $Q_{1}$ with a path $\pi^{\mathbf{G}}_{A}$ of length
3 (i.e., adding two new internal vertices). A _morphism type_ from
$Q_{2}(\bar{x}_{2})$ to $Q_{1}(\bar{x}_{1})$ is a pair $(H,h)$ such that
$h:H\xrightarrow{\textit{inj}}\mathbf{G}$, and $H$ is a graph resulting from
replacing each atom $A=x\xrightarrow{L}y$ of $Q_{2}$ with a (non-empty) path
$\pi^{H}_{A}$ from $x$ to $y$. Further, we also ask that free variables are
mapped accordingly, that is, $h(\bar{x}_{2})=\bar{x}_{1}$. Figure 8 contains
an example of a morphism type $(H,h)$.

Figure 8. Example of definition of $\mathbf{G}$ and morphism type $(H,h)$ from
$Q_{1},Q_{2}$. In this case, the injective morphism $h$ from $H$ to
$\mathbf{G}$ maps each node of $H$ to the node in the same position on
$\mathbf{G}$ (e.g., the lower-right node $r$ of $H$ maps to the lower-right
node of $\mathbf{G}$).

It follows that, by injectivity, the size of $H$ in any morphism type is
linearly bounded on $Q_{1}$.

###### Claim C.2.

Testing whether a pair $(H,h)$ is a morphism type is in PSpace.

A morphism type $(H,h)$ is _compatible_ with an abstraction $\alpha$ if there
is a mapping $\lambda$ from the internal nodes of paths $\pi^{H}_{A}$ to
states of $A$, such that for every atom $A=x_{1}\xrightarrow{L}x_{2}$ of
$Q_{1}$,

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ and an infix subpath $\pi$ of
$\pi_{A^{\prime}}^{H}$ with $h(\pi)=\pi^{\mathbf{G}}_{A}$, then
$\langle\lambda(src(\pi))\text{-}\lambda(tgt(\pi))\rangle\in\alpha(A)$
(corresponding to case 1 in Figure 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ and a suffix subpath $\pi$ of
$\pi_{A^{\prime}}^{H}$ with $h(\pi)=\pi^{\mathbf{G}}_{A}$, then
$\langle\lambda(src(\pi))\text{-}q_{F}\rangle\in\alpha(A)$ where $q_{F}$ is a
final state of $A^{\prime}$ (case 2 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ and a suffix subpath $\pi$ of
$\pi^{H}_{A^{\prime}}$ with $h(\pi)$ being a prefix of $\pi^{\mathbf{G}}_{A}$,
then $\langle\lambda(src(\pi))\text{-}\\!{|}\\!\text{-}q\rangle\in\alpha(A)$
for some $q$ (case 3 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$, a suffix
subpath $\pi_{1}$ of $\pi^{H}_{A^{\prime}_{1}}$ and a prefix subpath $\pi_{2}$
of $\pi^{H}_{A^{\prime}_{2}}$ with $tgt(\pi_{1})=src(\pi_{2})$ and
$h(\pi_{1}\pi_{2})=\pi^{\mathbf{G}}_{A}$, then $\langle
src(\pi_{1})\text{-}\\!{|}\\!\text{-}tgt(\pi_{2})\rangle\in\alpha(A)$ (case 4
in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$ and a suffix
subpath $\pi$ of $\pi_{A^{\prime}_{1}}^{H}$ with
$tgt(\pi)=src(\pi_{A^{\prime}_{2}}^{H})$ and
$h(\pi\pi_{A^{\prime}_{2}}^{H})=\pi^{\mathbf{G}}_{A}$, then
$\langle\lambda(src(\pi))\text{-}\\!{|}\\!\text{-}q_{F}\rangle\in\alpha(A)$
where $q_{F}$ is a final state of $A^{\prime}_{2}$ (case 5 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$, a suffix
subpath $\pi_{1}$ of $\pi_{A^{\prime}_{1}}^{H}$, and a prefix subpath
$\pi_{2}$ of $\pi_{A^{\prime}_{2}}^{H}$ with $tgt(\pi_{1})\neq src(\pi_{2})$,
$h(\pi_{1})$ is a prefix of $\pi^{\mathbf{G}}_{A}$ and $h(\pi_{2})$ is a
suffix of $\pi^{\mathbf{G}}_{A}$, then
$\langle\lambda(src(\pi_{1}))\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}\lambda(tgt(\pi_{2}))\rangle\in\alpha(A)$
(case 6 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$, and a suffix
subpath $\pi$ of $\pi^{H}_{A^{\prime}_{1}}$ where $h(\pi)$ is a prefix of
$\pi^{\mathbf{G}}_{A}$, $h(\pi^{H}_{A^{\prime}_{2}})$ is a suffix of
$\pi^{\mathbf{G}}_{A}$ and $tgt(\pi)\neq src(\pi^{H}_{A^{\prime}_{2}})$, then
$\langle\lambda(src(\pi))\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}q_{F}\rangle\in\alpha(A)$
for some final state $q_{F}$ of $A^{\prime}_{2}$ (case 7 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ and a prefix subpath $\pi$ of
$\pi_{A^{\prime}}^{H}$ with $h(\pi)=\pi^{\mathbf{G}}_{A}$, then $\langle
q_{0}\text{-}\lambda(tgt(\pi))\rangle\in\alpha(A)$ where $q_{0}$ is an initial
state of $A^{\prime}$ (case 8 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ with
$h(\pi_{A^{\prime}}^{H})=\pi^{\mathbf{G}}_{A}$, then $\langle
q_{0}\text{-}q_{F}\rangle\in\alpha(A)$ where $q_{0}$/$q_{F}$ is an
initial/final state of $A^{\prime}$ (case 9 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ with $h(\pi_{A^{\prime}}^{H})$ a
prefix of $\pi^{\mathbf{G}}_{A}$, then $\langle
q_{0}\text{-}\\!{|}\\!\text{-}q\rangle\in\alpha(A)$ where $q_{0}$ is an
initial state of $A^{\prime}$ and $q$ is any state. (case 10 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$ and a prefix
subpath $\pi_{2}$ of $\pi_{A^{\prime}_{2}}^{H}$ with
$tgt(\pi_{A^{\prime}_{1}}^{H})=src(\pi_{2})$,
$h(\pi_{A^{\prime}_{1}}^{H}\pi_{2})=\pi^{\mathbf{G}}_{A}$, then $\langle
q_{0}\text{-}\\!{|}\\!\text{-}\lambda(tgt(\pi_{2}))\rangle\in\alpha(A)$ where
$q_{0}$ is an initial state of $A^{\prime}_{1}$ (case 11 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$ with
$tgt(\pi_{A^{\prime}_{1}}^{H})=src(\pi_{A^{\prime}_{2}}^{H})$,
$h(\pi_{A^{\prime}_{1}}^{H}\pi_{A^{\prime}_{2}}^{H})=\pi^{\mathbf{G}}_{A}$,
then $\langle q_{0}\text{-}\\!{|}\\!\text{-}q_{F}\rangle\in\alpha(A)$ where
$q_{0}$ is an initial state of $A^{\prime}_{1}$ and $q_{F}$ a final state of
$A^{\prime}_{2}$ (case 12 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ and a prefix $\pi$ of
$\pi_{A^{\prime}}^{H}$ with $h(\pi)$ a suffix of $\pi^{\mathbf{G}}_{A}$, then
and $\langle
q\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}\lambda(tgt(\pi))\rangle\in\alpha(A)$
for some $q$ (case 13 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$ and a prefix
subpath $\pi_{2}$ of $\pi_{A^{\prime}_{2}}^{H}$ with
$tgt(\pi_{A^{\prime}_{1}}^{H})\neq src(\pi_{2})$,
$h(\pi_{A^{\prime}_{1}}^{H})$ is a prefix of $\pi^{\mathbf{G}}_{A}$ and
$h(\pi_{2})$ is a suffix of $\pi^{\mathbf{G}}_{A}$, then $\langle
q_{0}\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}\lambda(tgt(\pi_{2}))\rangle\in\alpha(A)$
where $q_{0}$ is an initial state of $A^{\prime}_{1}$ (case 14 in Fig. 9);

  * •

if there are atoms $A^{\prime}_{1},A^{\prime}_{2}$ of $Q_{2}$ with
$tgt(\pi_{A^{\prime}_{1}}^{H})\neq src(\pi_{A^{\prime}_{2}}^{H})$,
$h(\pi_{A^{\prime}_{1}}^{H})$ is a prefix of $\pi^{\mathbf{G}}_{A}$ and
$h(\pi_{A^{\prime}_{2}}^{H})$ is a suffix of $\pi^{\mathbf{G}}_{A}$, then
$\langle
q_{0}\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}q_{F}\rangle\in\alpha(A)$ where
$q_{0}$ is an initial state of $A^{\prime}_{1}$ and $q_{F}$ a final state of
$A^{\prime}_{2}$ (case 15 in Fig. 9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ with $h(\pi^{H}_{A^{\prime}})$
being an infix of $\pi^{\mathbf{G}}_{A}$, then
$\langle{\cdot}{\cdot}q_{0}\text{-}q_{F}{\cdot}{\cdot}\rangle\in\alpha(A)$ for
$q_{0}$ and $q_{F}$ initial and final states of $A^{\prime}$ (case 16 in Fig.
9);

  * •

if there is an atom $A^{\prime}$ of $Q_{2}$ where $h(\pi^{H}_{A^{\prime}})$ is
a suffix of $\pi^{\mathbf{G}}_{A}$, then $\langle
q\text{-}\\!{|}\\!\text{-}q_{F}\rangle\in\alpha(A)$ for some state $q$ and
some final state $q_{F}$ of $A^{\prime}$ (case 17 in Fig. 9).

Figure 9. All the possible cases for compatibility. Observe that there are no
other cases due to Remark C.3.

The following statement is a direct consequence of $H,h,\lambda$ being
polynomially bounded and each of the conditions above being polynomial-time
testable.

###### Claim C.3.

Testing whether a morphism type is compatible with an abstraction is in
PSpace.

The key property of compatible abstractions, is that they allow to capture
whether an expansion of $Q_{1}$ with a given abstraction is a counter-example
for the containment problem $Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$.

###### Claim C.4.

The following are equivalent:

  1. (1)

There is a morphism type compatible with an abstraction $\alpha$;

  2. (2)

for every expansion $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ with
abstraction $\alpha$ there exists some expansion
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}E_{1}$;

  3. (3)

there is an expansion $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ with
abstraction $\alpha$ and an expansion
$E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$E_{2}\xrightarrow{\textit{inj}}E_{1}$.

###### Proof.

$1\Rightarrow 2)$ Assume $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ has
abstraction $\alpha$, and $(H,h)$ is a compatible morphism type through the
mapping $\lambda$. Fore every atom $A$ of $Q_{1}$, we replace every path $\pi$
of $H$ such that $h(\pi)=\pi^{\mathbf{G}}_{A}$ with the expansion of $A$ in
$E_{1}$. The remaining edges of $H$ are all part of paths which map
_partially_ to some $\pi^{\mathbf{G}}_{A}$, these are replaced with paths
according to the witnessing words for the elements of the form $\langle
q\text{-}\\!{|}{\cdot}{\cdot}{|}\\!\text{-}q^{\prime}\rangle$ and
$\langle{\cdot}{\cdot}q\text{-}q^{\prime}{\cdot}{\cdot}\rangle$ in each
$\alpha(A)$.

Figure 10. Example for proof of Claim C.4

For example, in the case depicted in Figure 10, we know that the expansion
$w\in L$ of $A$ is of the form $w=u\cdot s\cdot v$ such that there is a
partial run of $\mathcal{A}_{Q_{2}}$ from $q$ to some final state reading $u$,
and a partial run of $\mathcal{A}_{Q_{2}}$ from an initial state to
$q^{\prime}$ reading $v$. Hence, we replace edge $e_{1}$ with a path reading
$u$, and edge $e_{2}$ with a path reading $v$. It follows that by the
definition of abstraction the resulting CQ (i.e., the query represented by the
resulting edge-labeled graph) is an expansion of $Q_{2}$ that maps to $E_{1}$
through an injective homomorphism.

$2\Rightarrow 3)$ This is trivial since an abstraction of $Q_{1}$ is the
abstraction of an expansion thereof.

$3\Rightarrow 1)$ Take any $E_{1}\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ with
abstraction $\alpha$ and $E_{2}\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ such that
$g:E_{2}\xrightarrow{\textit{inj}}E_{1}$. We now build a graph $H$ from
$E_{2}$ as follows. In the sequel, whenever we say that we replace a path
$\pi$ with a path of length $n$, we mean that we (1) remove all internal nodes
of $\pi$, and all edges incident to these and (2) we add $n-1$ fresh nodes and
$n$ edges in such a way that there is a path of length $n$ from $src(\pi)$ to
$tgt(\pi)$. For every path $\pi$ in $E_{1}$ corresponding to the expansion of
atom $A$ :

  * •

If there is a prefix [resp. suffix] of $\pi$ which has no $g$-preimage, we
replace the path $g^{-1}(\pi)$ with just one edge, and we send the variable to
the first internal node of $\pi^{\mathbf{G}}_{A}$. For the remaining cases let
us assume that every node of $\pi$ has a $g$-preimage.

  * •

If $g^{-1}(\pi)$ is a path with no $Q_{2}$-variables as internal nodes, then
we replace it with an unlabeled path $\pi^{\prime}$ of length 3. We define $h$
to map the first [resp. second] internal node of $\pi^{\prime}$ to the first
[resp. second] internal node of $\pi_{A}^{\mathbf{G}}$.

  * •

If $g^{-1}(\pi)$ is a path that contains one variable
$x\in\textit{vars}(Q_{2})$ as internal node, we replace the first half path of
$g^{-1}(\pi)$ until $x$ with just an unlabeled edge, and the other half with a
path $\pi^{\prime}$ of length 2. We set $h$ to map the variable $x$ to the
first internal node of $\pi^{\mathbf{G}}_{A}$ and the internal node of $\pi$
to the second internal node of $\pi^{\mathbf{G}}_{A}$.

  * •

If $g^{-1}(\pi)$ contains two variables and two disjoint paths, we replace
each of them with an unlabeled edge. We send the variables (i.e., the
endpoints of the paths) correspondingly to the two internal vertices of
$\pi^{\mathbf{G}}_{A}$.

The resulting graph $H$ and mapping $h$ is a morphism type which is compatible
with $\alpha$. ∎

Finally, the PSpace algorithm guesses a mapping $\alpha$ from the atoms of
$Q_{1}$ to subsets of $P$, checks that $\alpha$ is an abstraction of $Q_{1}$
(in PSpace due to Claim C.1), and checks that there is no morphism type
$(H,h)$ which is compatible with $\alpha$ (in PSpace, due to Claims C.2 and
C.3, and closure under complement of PSpace). Due to Claim C.4, if the
algorithm succeeds, then any expansion $E_{1}$ of $Q_{1}$ is a counter-
example, and thus $Q_{1}\not\subseteq_{\textit{q-inj}}Q_{2}$; otherwise, for
every expansion $E_{1}$ with abstraction $\alpha$ there is a compatible
morphism type, which means that $E_{1}$ is not a counter-example and hence
$Q_{1}\subseteq_{\textit{q-inj}}Q_{2}$.

First note that if $Q_{2}$ is not connected, we can adapt the PSpace algorithm
by testing that there are no morphism types for the connected components of
$Q_{2}$ such that all of them are compatible with the guessed abstraction of
$Q_{1}$. Further, observe that the procedure can be extended to an exponential
union of polynomial-sized CRPQs: the PSpace algorithm first chooses one CRPQ
$Q_{1}$ from the left-hand side union, guesses an abstraction of $Q_{1}$ and
checks that no CRPQ coming from the right-hand side union has a compatible
morphism type. For this reason, combined with Remark C.2, the same argument
extends to (unions of) arbitrary CRPQ’s. ∎

##  Appendix D Full Proof of Theorem 5.2

We reduce from _Post Correspondence Problem_ (PCP), a well-known undecidable
problem. An instance of the PCP is a sequence of pairs
$(u_{1},v_{1}),\dots,(u_{\ell},v_{\ell})$, where $u_{i}$ and $v_{i}$ are non-
empty words over an alphabet $\Sigma$. The goal is to decide whether there is
a _solution_ , that is, a sequence $i_{1},\dots,i_{k}$ of indices from
$\\{1,\dots,\ell\\}$, with $k\geq 1$, such that the words $u_{i_{1}}\cdots
u_{i_{k}}$ and $v_{i_{1}}\cdots v_{i_{k}}$ coincide.

For an alphabet $\mathbb{A}$, we denote by $\widehat{\mathbb{A}}$ the alphabet
$\widehat{\mathbb{A}}=\\{\widehat{a}:a\in\mathbb{A}\\}$. Let
$(u_{1},v_{1}),\dots,(u_{\ell},v_{\ell})$ be a PCP instance and let $\Sigma$
be its underlying alphabet. Let $\mathbb{I}$ and $\mathbb{A}$ be the alphabets
$\mathbb{I}=\\{I_{1},\dots,I_{\ell}\\}$ and
$\mathbb{A}=\Sigma\cup\mathbb{I}\cup\\{\\#,\\#_{\infty},\square,\$,\$^{\prime},\$_{\infty},\blacksquare,\blacksquare^{\prime}\\}$.
We construct Boolean CRPQs $Q_{1}$ and $Q_{2}$ over alphabet
$\mathbb{A}\cup\widehat{\mathbb{A}}$ such that the PCP instance
$(u_{1},v_{1}),\dots,(u_{\ell},v_{\ell})$ has a solution if and only if
$Q_{1}\not\subseteq_{\textit{a-inj}}Q_{2}$. In particular, the PCP instance
has a solution if and only if there exists a counterexample for a-inj-
semantics, i.e., an a-inj-expansion $F$ of $Q_{1}$ such that there is no
expansion $E\in\textup{{Exp}}^{\mathit{}}(Q_{2})$ with
$E\xrightarrow{\textit{a-inj}}F$.

The symbols in $\mathbb{A}$ are associated with the words $u_{i}$, while the
symbols in $\widehat{\mathbb{A}}$ with the words $v_{i}$. For each
$u_{i}=a_{1}\cdots a_{k}$, we define the word
$U_{i}=a_{1}\,\$\,\blacksquare\,a_{2}\,\$\,\blacksquare\,\cdots\,a_{k}\,\$^{\prime}\,\blacksquare^{\prime}$.
Similarly, for each $v_{i}=a_{1}\cdots a_{k}$ we define
$V_{i}=\widehat{\blacksquare}^{\prime}\,\widehat{\$}^{\prime}\,\widehat{a}_{k}\,\widehat{\blacksquare}\,\widehat{\$}\,\widehat{a}_{k-1}\,\cdots\,\widehat{\blacksquare}\,\widehat{\$}\,\widehat{a}_{1}$.
The CRPQ $Q_{1}$ is defined as follows (see Figure 11 for an illustration):

$\displaystyle Q_{1}=y_{1}\xrightarrow{L_{I}}x\land
y_{2}\xrightarrow{\widehat{L}_{a}}x\land
x\xrightarrow{\widehat{L}_{I}}z_{1}\land x\xrightarrow{L_{a}}z_{2}$
$\displaystyle\qquad\qquad\land x\xrightarrow{\square}x^{\prime}\land
x\xrightarrow{\widehat{\blacksquare}}x^{\prime}\land
x^{\prime}\xrightarrow{\widehat{\square}}x\land
x^{\prime}\xrightarrow{\blacksquare}x$ $\displaystyle\qquad\qquad\land
y^{\prime}_{1}\xrightarrow{\\#_{\infty}}y_{1}\land
y^{\prime}_{2}\xrightarrow{\widehat{\$}_{\infty}}y_{2}\land
z_{1}\xrightarrow{\widehat{\\#}_{\infty}\widehat{\\#}}z_{1}^{\prime}\land
z_{2}\xrightarrow{\$_{\infty}\$}z_{2}^{\prime}$

where:

$\displaystyle
L_{I}=(\square\,\\#\,\mathbb{I})^{+}\qquad\widehat{L}_{I}=(\widehat{\mathbb{I}}\,\widehat{\\#}\,\widehat{\square})^{+}$
$\displaystyle
L_{a}=(U_{1}+\cdots+U_{\ell})^{+}\qquad\widehat{L}_{a}=(V_{1}+\cdots+V_{\ell})^{+}$

Figure 11. The Boolean CRPQs $Q_{1}$ and $Q_{2}$ from the reduction.

Intuitively, a word from $L_{I}$ corresponds to a choice of indices from
$\\{1,\dots,\ell\\}$, similarly for $\widehat{L}_{I}$. On the other hand, a
word from $L_{a}$ [resp. $\widehat{L}_{a}$] corresponds to a choice of words
from $\\{u_{1},\dots,u_{\ell}\\}$ [resp. $\\{v_{1},\dots,v_{\ell}\\}$].

We are interested in a particular type of a-inj-expansions of $Q_{1}$ that we
call _well-formed_ and define below. The idea is that well-formed a-inj-
expansions correspond to solutions of the PCP instance. In particular, if
there is a well-formed a-inj-expansion of $Q_{1}$ then there is a solution to
the PCP instance and vice versa. We then show how to construct $Q_{2}$ such
that an a-inj-expansion of $Q_{1}$ is well-formed if and only if it is a
counterexample for $Q_{1}\subseteq_{\textit{a-inj}}Q_{2}$.

Figure 12. Example of the $I$-$\widehat{I}$-condition of well-formed
expansions of $Q_{1}$. We show the expansions $y_{1}\xrightarrow{w_{I}}x$ and
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ of the atoms $y_{1}\xrightarrow{L_{I}}x$
and $x\xrightarrow{\widehat{L}_{I}}z_{1}$, respectively. The words
$w_{I}=\square\,\\#\,I_{2}\,\square\,\\#\,I_{5}$ and
$\widehat{w}_{I}=\widehat{I}_{5}\,\widehat{\\#}\,\widehat{\square}\,\widehat{I}_{2}\,\widehat{\\#}\,\widehat{\square}$
encode the sequence of indices $5,2$. Dotted blue lines indicate pairs of
equal variables while red lines indicate distinct variables. We have some
extra symbols $\\#,\widehat{\\#},\square,\widehat{\square}$.

Let $F$ be an a-inj-expansion of $Q_{1}$ such that $F=\widetilde{F}^{\equiv}$
for $\widetilde{F}=E\land J$ (here $E\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ and
$J$ are the equality atoms). We say that $F$ is _well-formed_ if it satisfies
the following four conditions:

  1. (1)

_$I$ -$\widehat{I}$-condition :_ This condition applies to the atoms
$y_{1}\xrightarrow{L_{I}}x$ and $x\xrightarrow{\widehat{L}_{I}}z_{1}$ of
$Q_{1}$. Let $y_{1}\xrightarrow{w_{I}}x$ and
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ be the expansions associated to the
atoms $y_{1}\xrightarrow{L_{I}}x$ and $x\xrightarrow{\widehat{L}_{I}}z_{1}$ in
the expansion $E$. The condition requires the words $w_{I}$ and
$\widehat{w}_{I}$ to be of the form
$w_{I}=\square\,\\#\,I_{i_{k}}\,\cdots\,\square\,\\#\,I_{i_{1}}$ and
$\widehat{w}_{I}=\widehat{I}_{i_{1}}\,\widehat{\\#}\,\widehat{\square}\,\cdots\,\widehat{I}_{i_{k}}\,\widehat{\\#}\,\widehat{\square}$,
for a sequence of indices $i_{1},\dots,i_{k}\in\\{1,\dots,\ell\\}$. In other
words, the expansions of the atoms $y_{1}\xrightarrow{L_{I}}x$ and
$x\xrightarrow{\widehat{L}_{I}}z_{1}$ correspond to the same sequence on
indices. The $I$-$\widehat{I}$-condition also requires a particular behavior
on the equality atoms $J$ (see Figure 12). Suppose the expansion
$y_{1}\xrightarrow{w_{I}}x$ is of the form:

$\displaystyle\qquad\quad
y_{1}\xrightarrow{\square}s_{k}\xrightarrow{\\#}t_{k}\xrightarrow{I_{i_{k}}}r_{{k-1}}\xrightarrow{\square}$
$\displaystyle
s_{{k-1}}\xrightarrow{\\#}t_{{k-1}}\xrightarrow{I_{i_{k-1}}}r_{{k-2}}\cdots$
$\displaystyle\cdots
r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x$

and $x\xrightarrow{\widehat{w}_{I}}z_{1}$ is of the form:

$\displaystyle\qquad\quad
x\xrightarrow{\widehat{I}_{i_{1}}}t^{\prime}_{1}\xrightarrow{\widehat{\\#}}s^{\prime}_{1}\xrightarrow{\widehat{\square}}r^{\prime}_{{1}}\xrightarrow{\widehat{I}_{i_{2}}}$
$\displaystyle
t^{\prime}_{{2}}\xrightarrow{\widehat{\\#}}s^{\prime}_{{2}}\xrightarrow{\widehat{\square}}r^{\prime}_{{2}}\cdots$
$\displaystyle\cdots
r^{\prime}_{{k-1}}\xrightarrow{\widehat{I}_{i_{k}}}t^{\prime}_{k}\xrightarrow{\widehat{\\#}}s^{\prime}_{k}\xrightarrow{\widehat{\square}}z_{1}$

Then the relation $=_{\widetilde{F}}$ produced by the equality atoms $J$
satisfies:

    1. (a)

$t_{1}\neq_{\widetilde{F}}t^{\prime}_{1},\cdots,t_{k}\neq_{\widetilde{F}}t^{\prime}_{k}$

    2. (b)

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{k}=_{\widetilde{F}}s^{\prime}_{k}$

    3. (c)

$r_{1}=_{\widetilde{F}}r^{\prime}_{1},\cdots,r_{{k}}=_{\widetilde{F}}r^{\prime}_{{k}}$

where $r_{k}:=y_{1}$ and $r^{\prime}_{k}:=z_{1}$.

  2. (2)

_$I$ -$a$-condition :_ This condition applies to the atoms
$y_{1}\xrightarrow{L_{I}}x$ and $x\xrightarrow{L_{a}}z_{2}$ of $Q_{1}$. Let
$y_{1}\xrightarrow{w_{I}}x$ and $x\xrightarrow{w_{a}}z_{2}$ be the expansions
associated to the atoms $y_{1}\xrightarrow{L_{I}}x$ and
$x\xrightarrow{L_{a}}z_{2}$ in the expansion $E$. The condition requires the
words $w_{I}$ and $w_{a}$ to be of the form
$w_{I}=\square\,\\#\,I_{i_{k}}\,\cdots\,\square\,\\#\,I_{i_{1}}$ and
$w_{a}=U_{i_{1}}\cdots U_{i_{k}}$, for a sequence of indices
$i_{1},\dots,i_{k}\in\\{1,\dots,\ell\\}$. Intuitively, the word $w_{a}$
chooses words from $\\{u_{1},\dots,u_{\ell}\\}$ according to the sequence
$i_{1},\dots,i_{k}$. The $I$-$a$-condition also requires a particular behavior
on the equality atoms $J$. Suppose the expansion $y_{1}\xrightarrow{w_{I}}x$
is of the form:

$\displaystyle\qquad\quad
y_{1}\xrightarrow{\square}s_{k}\xrightarrow{\\#}t_{k}\xrightarrow{I_{i_{k}}}r_{{k-1}}\xrightarrow{\square}$
$\displaystyle
s_{{k-1}}\xrightarrow{\\#}t_{{k-1}}\xrightarrow{I_{i_{k-1}}}r_{{k-2}}\cdots$
$\displaystyle\cdots
r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x$

and the expansion $x\xrightarrow{w_{a}}z_{2}$ is of the form:

$\displaystyle\qquad\quad
x\xrightarrow{\widetilde{U}_{i_{1}}}s^{\prime}_{1}\xrightarrow{\blacksquare^{\prime}}r^{\prime}_{{1}}\xrightarrow{\widetilde{U}_{i_{2}}}s^{\prime}_{{2}}\xrightarrow{\blacksquare^{\prime}}r^{\prime}_{{2}}\cdots
r^{\prime}_{{k-1}}\xrightarrow{\widetilde{U}_{i_{k}}}s^{\prime}_{k}\xrightarrow{\blacksquare^{\prime}}z_{2}$

where $\widetilde{U}_{i}$ is the word obtained from $U_{i}$ by removing the
last symbol $\blacksquare^{\prime}$. Then the relation $=_{\widetilde{F}}$
produced by the equality atoms $J$ satisfies:

    1. (a)

$t_{j}\neq_{\widetilde{F}}t$, for every internal variable $t$ of the expansion
$r^{\prime}_{{j-1}}\xrightarrow{\widetilde{U}_{i_{j}}}s^{\prime}_{{j}}$ (here
$r^{\prime}_{0}:=x$)

    2. (b)

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{k}=_{\widetilde{F}}s^{\prime}_{k}$

    3. (c)

$r_{1}=_{\widetilde{F}}r^{\prime}_{1},\cdots,r_{{k}}=_{\widetilde{F}}r^{\prime}_{{k}}$

where $r_{k}:=y_{1}$ and $r^{\prime}_{k}:=z_{2}$.

  3. (3)

_$\widehat{a}$ -$\widehat{I}$-condition :_ This is analogous to the
$I$-$a$-condition and applies to the atoms
$y_{2}\xrightarrow{\widehat{L}_{a}}x$ and
$x\xrightarrow{\widehat{L}_{I}}z_{1}$ of $Q_{1}$. Let
$y_{2}\xrightarrow{\widehat{w}_{a}}x$ and
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ be the expansions associated to the
atoms $y_{2}\xrightarrow{\widehat{L}_{a}}x$ and
$x\xrightarrow{\widehat{L}_{I}}z_{1}$ in the expansion $E$. The condition
requires the words $\widehat{w}_{a}$ and $\widehat{w}_{I}$ to be of the form
$\widehat{w}_{I}=\widehat{I}_{i_{1}}\,\widehat{\\#}\,\widehat{\square}\,\cdots\,\widehat{I}_{i_{k}}\,\widehat{\\#}\,\widehat{\square}$
and $\widehat{w}_{a}=V_{i_{k}}\cdots V_{i_{1}}$, for a sequence of indices
$i_{1},\dots,i_{k}\in\\{1,\dots,\ell\\}$. That is, the word $\widehat{w}_{a}$
chooses words from $\\{v_{1},\dots,v_{\ell}\\}$ according to the sequence
$i_{1},\dots,i_{k}$. We also require some conditions on the equality atoms
$J$. Suppose the expansion $y_{2}\xrightarrow{\widehat{w}_{a}}x$ is of the
form:

$\displaystyle\qquad
y_{2}\xrightarrow{\widehat{\blacksquare}^{\prime}}s_{k}\xrightarrow{\widetilde{V}_{i_{k}}}r_{{k-1}}\xrightarrow{\widehat{\blacksquare}^{\prime}}s_{{k-1}}\xrightarrow{\widetilde{V}_{i_{k-1}}}r_{{k-2}}\cdots
r_{1}\xrightarrow{\widehat{\blacksquare}^{\prime}}s_{1}\xrightarrow{\widetilde{V}_{i_{1}}}x$

where $\widetilde{V}_{i}$ is the word obtained from $V_{i}$ by removing the
first symbol $\widehat{\blacksquare}^{\prime}$. Suppose also the expansion
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ is of the form:

$\displaystyle\qquad\quad
x\xrightarrow{\widehat{I}_{i_{1}}}t^{\prime}_{1}\xrightarrow{\widehat{\\#}}s^{\prime}_{1}\xrightarrow{\widehat{\square}}r^{\prime}_{{1}}\xrightarrow{\widehat{I}_{i_{2}}}$
$\displaystyle
t^{\prime}_{{2}}\xrightarrow{\widehat{\\#}}s^{\prime}_{{2}}\xrightarrow{\widehat{\square}}r^{\prime}_{{2}}\cdots$
$\displaystyle\cdots
r^{\prime}_{{k-1}}\xrightarrow{\widehat{I}_{i_{k}}}t^{\prime}_{k}\xrightarrow{\widehat{\\#}}s^{\prime}_{k}\xrightarrow{\widehat{\square}}z_{1}$

Then the relation $=_{\widetilde{F}}$ produced by the equality atoms $J$
satisfies:

    1. (a)

$t^{\prime}_{j}\neq_{\widetilde{F}}t$, for every internal variable $t$ of the
expansion $s_{j}\xrightarrow{\widetilde{V}_{i_{j}}}r_{{j-1}}$ (here
$r_{0}:=x$)

    2. (b)

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{k}=_{\widetilde{F}}s^{\prime}_{k}$

    3. (c)

$r_{1}=_{\widetilde{F}}r^{\prime}_{1},\cdots,r_{{k}}=_{\widetilde{F}}r^{\prime}_{{k}}$

where $r_{k}:=y_{2}$ and $r^{\prime}_{k}:=z_{1}$.

  4. (4)

_$\widehat{a}$ -$a$-condition :_ This condition applies to the atoms
$y_{2}\xrightarrow{\widehat{L}_{a}}x$ and $x\xrightarrow{L_{a}}z_{2}$ of
$Q_{1}$. Let $y_{2}\xrightarrow{\widehat{w}_{a}}x$ and
$x\xrightarrow{w_{a}}z_{2}$ be the expansions associated to the atoms
$y_{2}\xrightarrow{\widehat{L}_{a}}x$ and $x\xrightarrow{L_{a}}z_{2}$ in the
expansion $E$. The condition requires the words $\widehat{w}_{a}$ and $w_{a}$
to be of the form
$\widehat{w}_{a}=\clubsuit\,\clubsuit\,\widehat{a}_{n}\,\cdots\,\clubsuit\,\clubsuit\,\widehat{a}_{1}$
and $w_{a}=a_{1}\,\clubsuit\,\clubsuit\,\cdots\,a_{n}\,\clubsuit\,\clubsuit$,
for a word $a_{1}\cdots a_{n}\in\Sigma^{*}$ (recall $\Sigma$ is the alphabet
of the PCP instance). Here, $\clubsuit$ is a placeholder representing some
symbol. Intuitively, the word $\widehat{w}_{a}$ and $w_{a}$ represent the same
word from $\Sigma^{*}$. The $\widehat{a}$-$a$-condition also requires some
conditions on the equality atoms $J$. Assume the expansion
$y_{2}\xrightarrow{\widehat{w}_{a}}x$ is of the form:

$\displaystyle\qquad\quad
y_{2}\xrightarrow{\clubsuit}s_{n}\xrightarrow{\clubsuit}t_{n}\xrightarrow{\widehat{a}_{n}}r_{n-1}\xrightarrow{\clubsuit}$
$\displaystyle
s_{n-1}\xrightarrow{\clubsuit}t_{n-1}\xrightarrow{\widehat{a}_{n-1}}r_{n-2}\cdots$
$\displaystyle\cdots
r_{1}\xrightarrow{\clubsuit}s_{1}\xrightarrow{\clubsuit}t_{1}\xrightarrow{\widehat{a}_{1}}x$

and the expansion $x\xrightarrow{w_{a}}z_{2}$ is of the form:

$\displaystyle\qquad\quad
x\xrightarrow{a_{1}}t^{\prime}_{1}\xrightarrow{\clubsuit}s^{\prime}_{1}\xrightarrow{\clubsuit}r^{\prime}_{1}\xrightarrow{a_{2}}$
$\displaystyle
t^{\prime}_{2}\xrightarrow{\clubsuit}s^{\prime}_{2}\xrightarrow{\clubsuit}r^{\prime}_{2}\cdots$
$\displaystyle\cdots
r^{\prime}_{n-1}\xrightarrow{a_{n}}t^{\prime}_{n}\xrightarrow{\clubsuit}s^{\prime}_{n}\xrightarrow{\clubsuit}z_{2}$

Then the relation $=_{\widetilde{F}}$ produced by the equality atoms $J$
satisfies:

    1. (a)

$t_{1}\neq_{\widetilde{F}}t^{\prime}_{1},\cdots,t_{n}\neq_{\widetilde{F}}t^{\prime}_{n}$

    2. (b)

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{n}=_{\widetilde{F}}s^{\prime}_{n}$

    3. (c)

$r_{1}=_{\widetilde{F}}r^{\prime}_{1},\cdots,r_{n}=_{\widetilde{F}}r^{\prime}_{n}$

where $r_{n}:=y_{2}$ and $r^{\prime}_{n}:=z_{2}$.

The key property of well-formedness is that it can be characterized in terms
of the non-existence of a finite number of simple cycles and simple paths
having certain labels. In order to do this, we need to define some finite
languages. Recall $\widetilde{U}_{i}$ is obtained from $U_{i}$ by removing the
last symbol $\blacksquare^{\prime}$ and $\widetilde{V}_{i}$ is obtained from
$V_{i}$ by removing the first symbol $\widehat{\blacksquare}^{\prime}$. We
define $N$ to be the maximum length of the words $U_{i}$. We denote by
$e^{i,j}$, for $i\leq j$, the regular expression
$(e^{i}+e^{i+1}+\cdots+e^{j})$. We have:

$\displaystyle
K_{I\,\widehat{I}}=\mathbb{I}\,\widehat{\mathbb{I}}+\\#_{\infty}\,\widehat{\mathbb{I}}+\mathbb{I}\,\widehat{\\#}_{\infty}$
$\displaystyle M_{I\,\widehat{I}}=\sum_{i\neq
j}I_{i}\widehat{I}_{j}+\widehat{\mathbb{I}}\,\\#+\widehat{\\#}\,\mathbb{I}+\\#\,\mathbb{I}\,\widehat{\mathbb{I}}\,\widehat{\\#}+\square\,\widehat{\square}+\\#_{\infty}\,\widehat{\mathbb{I}}+\mathbb{I}\,\widehat{\\#}_{\infty}$
$\displaystyle
K_{Ia}=\mathbb{I}\,\Sigma+\\#_{\infty}\,\Sigma+\mathbb{I}\,\$_{\infty}$
$\displaystyle
M_{Ia}=(\Sigma+\$+\$^{\prime}+\blacksquare)\,\mathbb{I}+(\Sigma+\$+\blacksquare)^{1,N}\,\\#+\sum_{i}\sum_{j\neq
i}I_{i}\widetilde{U}_{j}\,+$
$\displaystyle\qquad+\\#\,\mathbb{I}\,(\widetilde{U}_{1}+\cdots+\widetilde{U}_{\ell})+\square\,\blacksquare^{\prime}+\\#_{\infty}\,\Sigma+\mathbb{I}\,\$_{\infty}$
$\displaystyle
K_{\widehat{a}\,\widehat{I}}=\widehat{\Sigma}\,\widehat{\mathbb{I}}+\widehat{\$}_{\infty}\,\widehat{\mathbb{I}}+\widehat{\Sigma}\,\widehat{\\#}_{\infty}$
$\displaystyle
M_{\widehat{a}\,\widehat{I}}=\widehat{\mathbb{I}}\,(\widehat{\Sigma}+\widehat{\$}+\widehat{\$}^{\prime}+\widehat{\blacksquare})+\widehat{\\#}\,\widehat{\Sigma}+\widehat{\mathbb{I}}\,\widehat{\\#}\,(\widehat{\Sigma}+\widehat{\$}+\widehat{\blacksquare})+\sum_{i}\sum_{j\neq
i}\widetilde{V}_{j}\widehat{I}_{i}\,+$
$\displaystyle\qquad+(\widetilde{V}_{1}+\cdots+\widetilde{V}_{\ell})\,\widehat{\mathbb{I}}\,\widehat{\\#}\,+\widehat{\blacksquare}^{\prime}\widehat{\square}+\widehat{\$}_{\infty}\,\widehat{\mathbb{I}}+\widehat{\Sigma}\,\widehat{\\#}_{\infty}$
$\displaystyle
K_{\widehat{a}a}=\widehat{\Sigma}\,\Sigma+\widehat{\$}_{\infty}\,\Sigma+\widehat{\Sigma}\,\$_{\infty}$
$\displaystyle M_{\widehat{a}a}=\sum_{a\neq
b}\widehat{a}b+\Sigma\,(\widehat{\$}+\widehat{\$}^{\prime})+(\$+\$^{\prime})\,\widehat{\Sigma}+(\widehat{\$}+\widehat{\$}^{\prime})\,\widehat{\Sigma}\,\Sigma\,(\$+\$^{\prime})+$
$\displaystyle\qquad+(\widehat{\blacksquare}+\widehat{\blacksquare}^{\prime})(\blacksquare+\blacksquare^{\prime})+\widehat{\$}_{\infty}\,\Sigma+\widehat{\Sigma}\,\$_{\infty}$

###### Claim D.1.

Let $F$ be an a-inj-expansion of $Q_{1}$. Then:

  1. (1)

$F$ satisfies the $I$-$\widehat{I}$-condition iff $F$ does not contain a
simple cycle with label in $K_{I\widehat{I}}$ nor a simple path with label in
$M_{I\widehat{I}}$.

  2. (2)

$F$ satisfies the $I$-$a$-condition iff $F$ does not contain a simple cycle
with label in $K_{Ia}$ nor a simple path with label in $M_{Ia}$.

  3. (3)

$F$ satisfies the $\widehat{a}$-$\widehat{I}$-condition iff $F$ does not
contain a simple cycle with label in $K_{\widehat{a}\,\widehat{I}}$ nor a
simple path with label in $M_{\widehat{a}\,\widehat{I}}$.

  4. (4)

$F$ satisfies the $\widehat{a}$-$a$-condition iff $F$ does not contain a
simple cycle with label in $K_{\widehat{a}a}$ nor a simple path with label in
$M_{\widehat{a}a}$.

###### Proof.

Suppose $F=\widetilde{F}^{\equiv}$ for $\widetilde{F}=E\land J$, where
$E\in\textup{{Exp}}^{\mathit{}}(Q_{1})$ and $J$ are equality atoms. We start
with item (1). Let $y_{1}\xrightarrow{w_{I}}x$ and
$x\xrightarrow{\widehat{w}_{I}}z_{1}$ be the expansions associated to the
atoms $y_{1}\xrightarrow{L_{I}}x$ and $x\xrightarrow{\widehat{L}_{I}}z_{1}$ in
the expansion $E$. Suppose that
$w_{I}=\square\,\\#\,I_{i_{k}}\,\cdots\,\square\,\\#\,I_{i_{1}}$ and
$\widehat{w}_{I}=\widehat{I}_{j_{1}}\,\widehat{\\#}\,\widehat{\square}\,\cdots\,\widehat{I}_{j_{p}}\,\widehat{\\#}\,\widehat{\square}$,
for indices $i_{1},\dots,i_{k},$ $j_{1},\dots,j_{p}$ $\in\\{1,\dots,\ell\\}$.
Assume also that $y_{1}\xrightarrow{w_{I}}x$ is of the form:

$\displaystyle
y_{1}\xrightarrow{\square}s_{k}\xrightarrow{\\#}t_{k}\xrightarrow{I_{i_{k}}}r_{{k-1}}\xrightarrow{\square}$
$\displaystyle
s_{{k-1}}\xrightarrow{\\#}t_{{k-1}}\xrightarrow{I_{i_{k-1}}}r_{{k-2}}\cdots$
$\displaystyle\cdots
r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x$

and $x\xrightarrow{\widehat{w}_{I}}z_{1}$ is of the form:

$\displaystyle
x\xrightarrow{\widehat{I}_{j_{1}}}t^{\prime}_{1}\xrightarrow{\widehat{\\#}}s^{\prime}_{1}\xrightarrow{\widehat{\square}}r^{\prime}_{{1}}\xrightarrow{\widehat{I}_{i_{2}}}$
$\displaystyle
t^{\prime}_{{2}}\xrightarrow{\widehat{\\#}}s^{\prime}_{{2}}\xrightarrow{\widehat{\square}}r^{\prime}_{{2}}\cdots$
$\displaystyle\cdots
r^{\prime}_{{p-1}}\xrightarrow{\widehat{I}_{j_{p}}}t^{\prime}_{p}\xrightarrow{\widehat{\\#}}s^{\prime}_{p}\xrightarrow{\widehat{\square}}z_{1}$

We consider first the backward direction of item (1). We have
$t_{1}\neq_{\widetilde{F}}t_{1}^{\prime}$, otherwise there would be a simple
cycle
$t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\widehat{I}_{j_{1}}}t_{1}^{\prime}$
with label in $\mathbb{I}\,\widehat{\mathbb{I}}\subseteq K_{I\widehat{I}}$.
This implies that $i_{1}=j_{1}$. If this is not the case, we would have a
simple path
$t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\widehat{I}_{j_{1}}}t_{1}^{\prime}$
with a label in $\sum_{i\neq j}I_{i}\widehat{I}_{j}\subseteq
M_{I\widehat{I}}$. We claim that $s_{1}=_{\widetilde{F}}s_{1}^{\prime}$. Note
first that $t_{1}\neq_{\widetilde{F}}s_{1}^{\prime}$ and
$t_{1}^{\prime}\neq_{\widetilde{F}}s_{1}$. Indeed, if
$t_{1}=_{\widetilde{F}}s_{1}^{\prime}$, then there would be a simple path
$t_{1}^{\prime}\xrightarrow{\widehat{\\#}}s_{1}^{\prime}\xrightarrow{I_{i_{1}}}x$
with label in $\widehat{\\#}\,\mathbb{I}\subseteq M_{I\widehat{I}}$. If
$t_{1}^{\prime}=_{\widetilde{F}}s_{1}$, then there would be a simple path
$x\xrightarrow{\widehat{I}_{j_{1}}}t_{1}^{\prime}\xrightarrow{\\#}t_{1}$ with
label in $\widehat{\mathbb{I}}\,\\#\subseteq M_{I\widehat{I}}$. It follows
that $s_{1}=_{\widetilde{F}}s_{1}^{\prime}$ as otherwise the path
$s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\widehat{I}_{j_{1}}}t^{\prime}_{1}\xrightarrow{\widehat{\\#}}s^{\prime}_{1}$
would be a simple path with a label in
$\\#\,\mathbb{I}\,\widehat{\mathbb{I}}\,\widehat{\\#}\subseteq
M_{I\widehat{I}}$. Finally, we have that
$r_{1}=_{\widetilde{F}}r_{1}^{\prime}$. If this is not true, then
$r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\widehat{\square}}r^{\prime}_{{1}}$
would be a simple path with a label in $\square\,\widehat{\square}\subseteq
M_{I\widehat{I}}$.

We can iterate this argument, replacing in each step the “middle” variable $x$
by the corresponding new “middle” variable $r_{i}$ (see Figure 12). We obtain
the following ($\alpha=\min\\{k,p\\}$):

  * •

$i_{1}=j_{1}$, $i_{2}=j_{2}$, $\dots$, $i_{\alpha}=j_{\alpha}$

  * •

$t_{1}\neq_{\widetilde{F}}t^{\prime}_{1},\cdots,t_{\alpha}\neq_{\widetilde{F}}t^{\prime}_{\alpha}$

  * •

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{\alpha}=_{\widetilde{F}}s^{\prime}_{\alpha}$

  * •

$r_{1}=_{\widetilde{F}}r^{\prime}_{1},\cdots,r_{\alpha}=_{\widetilde{F}}r^{\prime}_{\alpha}$

where $r_{k}:=y_{1}$ and $r^{\prime}_{p}:=z_{1}$. Note that to conclude the
$I$-$\widehat{I}$-condition, it suffices to show that $\alpha=k=p$. Towards a
contradiction, suppose first that $k<p$. We know that
$y_{1}=_{\widetilde{F}}r^{\prime}_{k}$, and $r^{\prime}_{k}\neq z_{1}$. In
particular, we have at least the following atoms:

$y_{1}^{\prime}\xrightarrow{\\#_{\infty}}y_{1}\qquad
r^{\prime}_{k}\xrightarrow{\widehat{I}_{j}}t^{\prime}_{k+1}$

We have two cases. If $y_{1}^{\prime}=_{\widetilde{F}}t^{\prime}_{k+1}$ then
we have a simple cycle
$y_{1}^{\prime}\xrightarrow{\\#_{\infty}}y_{1}\xrightarrow{\widehat{I}_{j}}t^{\prime}_{k+1}$
with a label in $\\#_{\infty}\,\widehat{\mathbb{I}}\subseteq
K_{I\widehat{I}}$. On the other hand, if
$y_{1}^{\prime}\neq_{\widetilde{F}}t^{\prime}_{k+1}$ then we have a simple
path
$y_{1}^{\prime}\xrightarrow{\\#_{\infty}}y_{1}\xrightarrow{\widehat{I}_{j}}t^{\prime}_{k+1}$
with a label in $\\#_{\infty}\,\widehat{\mathbb{I}}\subseteq
M_{I\widehat{I}}$. In either case, we obtain a contradiction. Suppose now that
$k>p$. We know that $r_{p}=_{\widetilde{F}}z_{1}$, and $r_{p}\neq y_{1}$. We
have at least the following atoms:

$t_{p+1}\xrightarrow{I_{i}}r_{p}\qquad
z_{1}\xrightarrow{\widehat{\\#}_{\infty}}z_{1}^{\prime\prime}$

Again we have two cases. If $t_{p+1}=_{\widetilde{F}}z_{1}^{\prime\prime}$
then we have a simple cycle
$t_{p+1}\xrightarrow{I_{i}}r_{p}\xrightarrow{\widehat{\\#}_{\infty}}z_{1}^{\prime\prime}$
with a label in $\mathbb{I}\,\widehat{\\#}_{\infty}\subseteq
K_{I\widehat{I}}$. On the other hand, if
$t_{p+1}\neq_{\widetilde{F}}z_{1}^{\prime\prime}$ then we have a simple path
$t_{p+1}\xrightarrow{I_{i}}r_{p}\xrightarrow{\widehat{\\#}_{\infty}}z_{1}^{\prime\prime}$
with a label in $\mathbb{I}\,\widehat{\\#}_{\infty}\subseteq
M_{I\widehat{I}}$. We obtain a contradiction in either case. We conclude that
$k=p$ and hence the $I$-$\widehat{I}$-condition holds.

The forward direction of item (1) follows directly from the definition of the
$I$-$\widehat{I}$-condition and inspection of the languages $K_{I\widehat{I}}$
and $M_{I\widehat{I}}$.

Now we turn to item (2). Let $y_{1}\xrightarrow{w_{I}}x$ and
$x\xrightarrow{w_{a}}z_{2}$ be the expansions associated to the atoms
$y_{1}\xrightarrow{L_{I}}x$ and $x\xrightarrow{L_{a}}z_{2}$ in the expansion
$E$. Suppose that
$w_{I}=\square\,\\#\,I_{i_{k}}\,\cdots\,\square\,\\#\,I_{i_{1}}$ and
$w_{a}=U_{j_{1}}\cdots U_{j_{p}}$ for indices $i_{1},\dots,i_{k},$
$j_{1},\dots,j_{p}$ $\in\\{1,\dots,\ell\\}$. Assume that the expansion
$y_{1}\xrightarrow{w_{I}}x$ is of the form:

$\displaystyle
y_{1}\xrightarrow{\square}s_{k}\xrightarrow{\\#}t_{k}\xrightarrow{I_{i_{k}}}r_{{k-1}}\xrightarrow{\square}$
$\displaystyle
s_{{k-1}}\xrightarrow{\\#}t_{{k-1}}\xrightarrow{I_{i_{k-1}}}r_{{k-2}}\cdots$
$\displaystyle\cdots
r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x$

and the expansion $x\xrightarrow{w_{a}}z_{2}$ is of the form:

$\displaystyle
x\xrightarrow{\widetilde{U}_{j_{1}}}s^{\prime}_{1}\xrightarrow{\blacksquare^{\prime}}r^{\prime}_{{1}}\xrightarrow{\widetilde{U}_{i_{2}}}s^{\prime}_{{2}}\xrightarrow{\blacksquare^{\prime}}r^{\prime}_{{2}}\cdots
r^{\prime}_{{p-1}}\xrightarrow{\widetilde{U}_{j_{p}}}s^{\prime}_{p}\xrightarrow{\blacksquare^{\prime}}z_{2}$

where $\widetilde{U}_{j}$ is the word obtained from $U_{j}$ by removing the
last symbol $\blacksquare^{\prime}$.

We consider first the backward direction of item (2). Suppose the expansion
$x\xrightarrow{\widetilde{U}_{j_{1}}}s^{\prime}_{1}$ has the form:

$\displaystyle x\xrightarrow{\clubsuit}o_{1}\xrightarrow{\clubsuit}o_{2}\cdots
o_{m}\xrightarrow{\clubsuit}s^{\prime}_{1}$

where $\clubsuit$ is a placeholder representing some symbol. We claim that
$t_{1}\neq_{\widetilde{F}}t$, for all $t\in\\{o_{1},\dots,o_{m},o_{m+1}\\}$,
where $o_{m+1}:=s^{\prime}_{1}$. Note first that
$t_{1}\neq_{\widetilde{F}}o_{1}$, otherwise there would be a simple cycle
$t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\clubsuit}o_{1}$, where
$\clubsuit\in\Sigma$. In particular, the label would belong to
$\mathbb{I}\,\Sigma\subseteq K_{Ia}$; a contradiction. Now we argue by
induction. Suppose $t_{1}\neq_{\widetilde{F}}o_{h}$, for some
$h\in\\{1,\dots,m\\}$. By contradiction, assume
$t_{1}=_{\widetilde{F}}o_{h+1}$. We have a simple path
$o_{h}\xrightarrow{\clubsuit}o_{h+1}\xrightarrow{I_{i_{1}}}x$, where
$\clubsuit\in\Sigma\cup\\{\$,\blacksquare,\$^{\prime}\\}$ (note that
$\clubsuit$ cannot be $\blacksquare^{\prime}$). Then the label belongs to
$(\Sigma+\$+\$^{\prime}+\blacksquare)\,\mathbb{I}\subseteq M_{Ia}$; a
contradiction.

We now claim that $s_{1}\neq_{\widetilde{F}}t$, for all
$t\in\\{o_{1},\dots,o_{m}\\}$. By contradiction, suppose that
$s_{1}=_{\widetilde{F}}t$, for some $t\in\\{o_{1},\dots,o_{m}\\}$. Then there
is a simple path $x\xrightarrow{U}t\xrightarrow{\\#}t_{1}$, where
$U\in(\Sigma+\$+\blacksquare)^{1,N}$ (note how we use the fact that
$t_{1}\neq_{\widetilde{F}}t$, for all $t\in\\{o_{1},\dots,o_{m}\\}$; otherwise
the path would not be necessarily simple). The label of the simple path
belongs to $(\Sigma+\$+\blacksquare)^{1,N}\,\\#\subseteq M_{Ia}$; a
contradiction.

We have that $i_{1}=j_{1}$. If this is not the case, then we would have the
simple path
$t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\widetilde{U}_{j_{1}}}s^{\prime}_{1}$
with a label in $\sum_{i}\sum_{j\neq i}I_{i}\widetilde{U}_{j}\subseteq
M_{Ia}$. Moreover, we have $s_{1}=_{\widetilde{F}}s_{1}^{\prime}$, otherwise
we would have the simple path
$s_{1}\xrightarrow{\\#}t_{1}\xrightarrow{I_{i_{1}}}x\xrightarrow{\widetilde{U}_{j_{1}}}s^{\prime}_{1}$
with a label in
$\\#\,\mathbb{I}\,(\widetilde{U}_{1}+\cdots+\widetilde{U}_{\ell})\subseteq
M_{Ia}$. Finally, we have $r_{1}=_{\widetilde{F}}r_{1}^{\prime}$. If this is
not the case, then we have a simple path
$r_{1}\xrightarrow{\square}s_{1}\xrightarrow{\blacksquare^{\prime}}r_{1}^{\prime}$
with a label in $\square\,\blacksquare^{\prime}\subseteq M_{Ia}$.

As in the case of item (1), we can iterate this argument, replacing in each
step the “middle” variable $x$ by the corresponding new “middle” variable
$r_{i}$. We obtain the following ($\alpha=\min\\{k,p\\}$):

  * •

$i_{1}=j_{1}$, $i_{2}=j_{2}$, $\dots$, $i_{\alpha}=j_{\alpha}$

  * •

For every $j\in\\{1,\dots,\alpha\\}$, we have $t_{j}\neq_{\widetilde{F}}t$,
for every internal variable $t$ of the expansion
$r^{\prime}_{{j-1}}\xrightarrow{\widetilde{U}_{i_{j}}}s^{\prime}_{{j}}$ (here
$r^{\prime}_{0}:=x$)

  * •

$s_{1}=_{\widetilde{F}}s^{\prime}_{1},\cdots,s_{\alpha}=_{\widetilde{F}}s^{\prime}_{\alpha}$

  * •