# Reverse Engineering of Temporal Queries Mediated by LTL Ontologies

Marie Fortin1 Boris Konev2 Vladislav Ryzhikov3 Yury Savateev4
Frank Wolter2&Michael Zakharyaschev3 1Université Paris Cité, CNRS, IRIF,
France
2Department of Computer Science, University of Liverpool, UK
3Department of Computer Science and Information Systems, Birkbeck, University
of London, UK
4School of Electronics and Computer Science, University of Southampton, UK
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

In reverse engineering of database queries, we aim to construct a query from a
given set of answers and non-answers; it can then be used to explore the data
further or as an explanation of the answers and non-answers. We investigate
this query-by-example problem for queries formulated in positive fragments of
linear temporal logic LTL over timestamped data, focusing on the design of
suitable query languages and the combined and data complexity of deciding
whether there exists a query in the given language that separates the given
answers from non-answers. We consider both plain LTL queries and those
mediated by LTL-ontologies.

##  1 Introduction

Supporting users of databases by constructing a query from examples of answers
and non-answers to the query has been a major research area since the 2000s
Martins (2019). In the database community, research has focussed on standard
query languages such as SQL, graph query languages, and SPARQL Zhang et al.
(2013); Weiss and Cohen (2017); Kalashnikov et al. (2018); Deutch and Gilad
(2019); Staworko and Wieczorek (2012); Barceló and Romero (2017); Cohen and
Weiss (2016); Arenas et al. (2016). The KR community has been concerned with
constructing queries from examples under the open world semantics and with
background knowledge given by an ontology Gutiérrez-Basulto et al. (2018);
Ortiz (2019); Cima et al. (2021); Jung et al. (2021, 2022). A fundamental
problem that has been investigated by both communities is known as
_separability_ or _query-by-example_ (QBE), a term coined by Zloof [1977]:

Given:

sets $E^{+}$ and $E^{-}$ of pairs $(\mathcal{D},\boldsymbol{d})$ with a
database instance $\mathcal{D}$ and a tuple $\boldsymbol{d}$ in $\mathcal{D}$,
a (possibly empty) ontology $\mathcal{O}$, and a query language $\mathcal{Q}$.

Problem:

decide whether there exists a query $\boldsymbol{q}\in\mathcal{Q}$
_separating_ $(E^{+},E^{-})$ in the sense that
$\mathcal{O},\mathcal{D}\models\boldsymbol{q}(\boldsymbol{d})$ for all
$(\mathcal{D},\boldsymbol{d})\in E^{+}$ and
$\mathcal{O},\mathcal{D}\not\models\boldsymbol{q}(\boldsymbol{d})$ for all
$(\mathcal{D},\boldsymbol{d})\in E^{-}$.

If such a $\boldsymbol{q}$ exists, then $(E^{+},E^{-})$ is often called
_satisfiable_ w.r.t. $\mathcal{Q}$ under $\mathcal{O}$, and the construction
of $\boldsymbol{q}$ is called _learning_.

In many applications, the input data is timestamped and queries are naturally
formulated in languages with temporal operators. In this paper, we investigate
temporal query-by-example by focusing on the basic but very useful case where
data $\mathcal{D}$ is a set of timestamped atomic propositions. Our query
languages are positive fragments of _linear temporal logic_ LTL with the
temporal operators $\Diamond$ (eventually), $\bigcirc$ (next), and
$\mathbin{\mathsf{U}}$ (until) interpreted under the strict semantics Demri et
al. (2016). To enforce generalisation, we do not admit $\lor$. Our most
expressive query language $\mathcal{Q}[\mathbin{\mathsf{U}}]$ is thus defined
as the set of formulas constructed from atoms using $\land$ and
$\mathbin{\mathsf{U}}$ (via which $\bigcirc$ and $\Diamond$ are expressible);
the fragments $\mathcal{Q}[\Diamond]$ and
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
are defined analogously. Ontologies can be given in full LTL or its fragments
$\textsl{LTL}^{\smash{\Box\Diamond}}$ (known as the _Prior logic_ Prior
(1956)), which only uses the operators $\Box$ (always in the future) and
$\Diamond$, and the Horn fragment
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
containing axioms of the form $C_{1}\land\dots\land C_{k}\to C_{k+1}$, where
the $C_{i}$ are atoms possibly prefixed by $\Box$ and $\bigcirc$ for $i\leq
k+1$, and also by $\Diamond$ for $i\leq k$. Ontology axioms are supposed to
hold at all times. In fact, already this basic ‘one-dimensional’ temporal
ontology-mediated querying formalism provides enough expressive power in those
real-world situations where the interaction among individuals in the object
domain is not important and can be disregarded in data modelling; see Artale
et al. (2021) and also Example 1 and the references before it.

Withinthis temporal setting, we take a broad view of the potential
applications of the QBE problem. On the one hand, there are non-expert users
who would like to explore data via queries but are not familiar with temporal
logic. They usually are, however, capable of providing data examples
illustrating the queries they are after. QBE supports such users in the
construction of those queries. On the other hand, the positive and negative
data examples might come from an application, and the user is interested in
possible explanations of the examples. Such an explanation is then provided by
a temporal query separating the positive examples from the negative ones. In
this case, our goal is similar to recent work on learning LTL formulas in
explainable planning and program synthesis Lemieux et al. (2015); Neider and
Gavran (2018); Camacho and McIlraith (2019); Fijalkow and Lagarde (2021); Raha
et al. (2022); Fortin et al. (2022).

######  Example 1.

Imagine an engineer whose task is to explain the behaviour of the monitored
equipment (say, why an engine stops) in terms of qualitative sensor data such
as ‘low temperature’ ($T$), ‘strong vibration’ ($V$), etc. Suppose the engine
stopped after the runs $\mathcal{D}^{+}_{1}$ and $\mathcal{D}^{+}_{2}$ below
but did not stop after the runs $\mathcal{D}^{-}_{1}$, $\mathcal{D}^{-}_{2}$,
$\mathcal{D}^{-}_{3}$, where we assume the runs to start at $0$ and
measurements to be recorded at moments $0,1,2,\dots$:

$\mathcal{D}^{+}_{1}=\\{T(2),V(4)\\},\mathcal{D}^{+}_{2}=\\{T(1),V(4)\\},\\\
\mathcal{D}^{-}_{1}=\\{T(1)\\},\mathcal{D}^{-}_{2}=\\{V(4)\\},\mathcal{D}^{-}_{3}=\\{V(1),T(2)\\}.$

The $\Diamond$-query $\boldsymbol{q}=\Diamond(T\land\Diamond\Diamond V)$ is
true at $0$ in the $\mathcal{D}^{+}_{i}$, false in $\mathcal{D}^{-}_{i}$, and
so gives a possible explanation of what could cause the engine failure. The
example set
$(\\{\mathcal{D}^{+}_{3},\mathcal{D}^{+}_{4}\\},\\{\mathcal{D}^{-}_{4}\\})$
with

$\mathcal{D}^{+}_{3}=\\{T(1),V(2)\\},\ \
\mathcal{D}^{+}_{4}=\\{T(1),T(2),V(3)\\},\\\
\mathcal{D}^{-}_{4}=\\{T(1),V(3)\\}$

is explained by the $\mathbin{\mathsf{U}}$-query $T\mathbin{\mathsf{U}}V$.
Using background knowledge, we can compensate for sensor failures resulting in
incomplete data. To illustrate, suppose $\mathcal{E}^{+}_{1}=\\{H(3),V(4)\\}$,
where $H$ means ‘heater is on’. If an ontology $\mathcal{O}$ has the axiom
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}H\to T$ saying that a
heater can only be triggered by the low temperature at the previous moment,
then the same $\boldsymbol{q}$ separates
$\\{\mathcal{E}^{+}_{1},\mathcal{D}^{+}_{2}\\}$ from
$\\{\mathcal{D}^{-}_{1},\mathcal{D}^{-}_{2},\mathcal{D}^{-}_{3}\\}$ under
$\mathcal{O}$. $\dashv$

Query $\boldsymbol{q}$ in Example 1 is of a particular ‘linear’ form, in which
the order of atoms is fixed and not left open as, for instance, in the
‘branching’ $\Diamond T\wedge\Diamond V$. More precisely, _path
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond$-queries_ in the
class
$\smash{\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]}$
take the form

$\displaystyle\boldsymbol{q}=\rho_{0}\land{\boldsymbol{o}}_{1}(\rho_{1}\land{\boldsymbol{o}}_{2}(\rho_{2}\land\dots\land{\boldsymbol{o}}_{n}\rho_{n})),$
(1)

where
${\boldsymbol{o}}_{i}\in\\{{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond\\}$
and $\rho_{i}$ is a conjunction of atoms; $\mathcal{Q}_{p}[\Diamond]$
restricts ${\boldsymbol{o}}_{i}$ to $\\{\Diamond\\}$; and _path
$\mathbin{\mathsf{U}}$-queries_ $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$ look
like

$\displaystyle\boldsymbol{q}=\rho_{0}\land(\lambda_{1}\mathbin{\mathsf{U}}(\rho_{1}\land(\lambda_{2}\mathbin{\mathsf{U}}(\dots(\lambda_{n}\mathbin{\mathsf{U}}\rho_{n})\dots)))),$
(2)

where $\lambda_{i}$ is a conjunction of atoms or $\bot$. Path queries are
motivated by two observations. First, if a query language admits conjunctions
of queries—unlike our classes of path queries—then, dually to overfitting for
$\lor$, multiple negative examples become redundant: if
$\boldsymbol{q}_{\mathcal{D}}$ separates $(E^{+},\\{\mathcal{D}\\})$, for each
$\mathcal{D}\in E^{-}$, then $\bigwedge_{\mathcal{D}\in
E^{-}}\boldsymbol{q}_{\mathcal{D}}$ separates $(E^{+},E^{-})$. Second,
numerous natural query types known from applications can be captured by path
queries. For example, the existence of a _common subsequence_ of the positive
examples (regarded as words) that is not a subsequence of any negative one
corresponds to the existence of a separating $\mathcal{Q}_{p}[\Diamond]$-query
with $\rho_{0}=\top$ and $\rho_{i}\not=\top$ for $i>0$, and the existence of a
_common subword_ of the positive examples that is not a subword of any
negative one corresponds to the existence of a separating query of the form
$\Diamond(\rho_{1}\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}(\rho_{2}\land\dots\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\rho_{n}))$.
These and similar queries are the basis of data comparison programs with
numerous applications in computational linguistics, bioinformatics, and
revision control systems Bergroth et al. (2000); Chowdhury et al. (2010); Blum
et al. (2021).

While path queries express the intended separating pattern of events in many
applications, branching queries are needed if the order of events is
irrelevant for separation.

######  Example 2.

In the setting of Example 1, the positive examples $\\{T(2),V(4)\\}$ and
$\\{V(1),T(4)\\}$ are separated from the negative $\\{T(1)\\}$ and
$\\{V(4)\\}$ by the branching $\mathcal{Q}[\Diamond]$-query $\Diamond
T\land\Diamond V$ while no path query is capable of doing this. $\dashv$

Branching
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$-queries
express transparent existential conditions and can be regarded as LTL CQs.
However, branching $\mathcal{Q}[\mathbin{\mathsf{U}}]$-queries with nestings
of $\mathbin{\mathsf{U}}$ on the left-hand side correspond to complex first-
order formulas with multiple alternations of quantifiers $\exists$ and
$\forall$, which are hard to comprehend. So we also consider the language
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]\supseteq\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$
of ‘simple’ $\mathcal{Q}[\mathbin{\mathsf{U}}]$-queries without such nestings.

In this paper, we take the first steps towards understanding the complexity
and especially feasibility of the query-by-example problems
$\mathsf{QBE}(\mathcal{L},\mathcal{Q})$ with $\mathcal{L}$ an ontology and
$\mathcal{Q}$ a query language. We are particularly interested in whether
there is a difference in complexity between path and branching queries and
whether it can be reduced by bounding the number of positive or negative
examples. Our results in the ontology-free case

$\mathsf{QBE}$ for | $\mathsf{b}+,\mathsf{b}-$ | $\mathsf{b}+$ |  $\mathsf{b}-$ or unbounded
---|---|---|---
$\mathcal{Q}_{p}[\Diamond]/\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$ | ${\small\leq}\textsc{P}$ | ${\small=}\textsc{NP}$ | ${\small=}\textsc{NP}$
$\mathcal{Q}[\Diamond]/\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$ | ${\small\leq}\textsc{P}$ | ${\small\leq}\textsc{P}$ | ${\small=}\textsc{NP}$
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$ | ${\small=}\textsc{NP}$
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ | ${\small\leq}\textsc{P}$ | ${\small\leq}\textsc{P}$ |  ${\small\geq}\textsc{NP}$, ${\small\leq}\textsc{PSpace}$
$\mathcal{Q}[\mathbin{\mathsf{U}}]$ | ${\small\leq}\textsc{PSpace}$
Table 1: Complexity in the ontology-free case.

are summarised in Table 1, where $\mathsf{b}+$ / $\mathsf{b}-$ indicate that
the number of positive / negative examples is bounded111We do not consider
queries with $\bigcirc$ only as separability is trivially in P and does not
detect any useful patterns.. Note that path queries are indeed harder than
branching ones when the number of positive examples is bounded but not in the
unbounded case. Our proof techniques range from reductions to common
subsequence existence problems Maier (1978); Fraser (1996) and dynamic
programming to mimicking separability by path and branching
$\mathbin{\mathsf{U}}$-queries in terms of containment and simulation of
transition systems Kupferman and Vardi (1996). The key to NP upper bounds is
the _polynomial separation property_ (PSP) of the respective languages: any
separable example set is separated by a polynomial-size query. The complexity
for $\mathcal{Q}_{p}[\Diamond]$, $\mathcal{Q}[\Diamond]$ can also be obtained
from Fijalkow and Lagarde (2021) who studied separability by
$\mathcal{Q}[\Diamond]$-queries of bounded size.

In the presence of ontologies, we distinguish between the combined complexity
of $\mathsf{QBE}(\mathcal{L},\mathcal{Q})$, when both data and ontology are
regarded as input, and the data complexity, when the ontology is deemed fixed
or negligibly small compared with the data. We obtain encouraging results:
$\mathcal{Q}_{p}[\Diamond]$\- and $\mathcal{Q}[\Diamond]$-queries mediated by
$\textsl{LTL}^{\smash{\Box\Diamond}}$-ontologies and all of our queries
mediated by
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontologies
enjoy the same data complexity as in Table 1. The combined complexity results
for queries with
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontologies
we have obtained so far are given in Table 2. Interestingly, QBE for query
classes with $\Diamond$ and $\bigcirc$ only is PSpace-complete—

$\mathcal{Q}[\Diamond]$ / $\mathcal{Q}_{p}[\Diamond]$ | = PSpace
---|---
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$ /
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ |  $\geq\textsc{PSpace}$, $\leq\textsc{ExpTime}$
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$ | $\geq\textsc{NExpTime},\leq\textsc{ExpSpace}$
$\mathcal{Q}[\mathbin{\mathsf{U}}]$ |  $\geq\textsc{PSpace}$, $\leq 2\textsc{ExpTime}$
Table 2: Combined complexity of
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q})$
in both bounded and unbounded cases.

not harder than satisfiability. The upper bound is proved by establishing the
_exponential separation property_ for all of these classes of queries and
using the canonical (aka minimal) model property of Horn LTL. The upper bounds
for $\mathbin{\mathsf{U}}$-queries are by reduction to the simulation and
containment problems for exponential-size transition systems. For arbitrary
LTL-ontologies, this technique only gives a $2\textsc{ExpTime}{}$ upper bound
for $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ and a $2\textsc{ExpSpace}{}$ one
for $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$. Separability by (path)
$\Diamond$-queries under $\textsl{LTL}^{\smash{\Box\Diamond}}$ ontologies
turns out to be $\Sigma_{2}^{p}$-complete, where the upper bound is shown by
establishing the PSP.

Compared with non-temporal QBE, our results are very encouraging: QBE is
coNExpTime-complete for conjunctive queries (CQs) over standard relational
databases Willard (2010); ten Cate and Dalmau (2015) and even undecidable for
CQs under $\mathcal{ELI}$ or $\mathcal{ALC}$ ontologies Funk et al. (2019);
Jung et al. (2020).

##  2 Further Related Work

We now briefly comment on a few other related research areas. One of them is
concept learning in description logic (DL), as proposed by Badea and Nienhuys-
Cheng (2000) who, inspired by inductive logic programming, used refinement
operators to construct a concept separating positive and negative examples in
a DL ABox. There has been significant interest in this approach Lehmann and
Haase (2009); Lehmann and Hitzler (2010); Lisi and Straccia (2015); Sarker and
Hitzler (2019); Lisi (2012); Rizzo et al. (2020). Prominent systems include
the DL Learner Bühmann et al. (2016), DL-Foil Fanizzi et al. (2018) and its
extension DL-Focl Rizzo et al. (2018), SPaCEL Tran et al. (2017), YinYang
Iannone et al. (2007), pFOIL-DL Straccia and Mucci (2015), and EvoLearner
Heindorf et al. (2022). However, this work has not considered the complexity
of separability. Also closely related is the work on the separability of two
formal (e.g., regular) languages using a weaker (e.g., FO-definable) language
Place and Zeitoun (2016); Hofman and Martens (2015); Place and Zeitoun (2022).
When translated into a logical separability problem, the main difference to
our results is that one demands
$\mathcal{O},\mathcal{D}\models\neg\boldsymbol{q}(\boldsymbol{d})$—and not
just $\mathcal{O},\mathcal{D}\not\models\boldsymbol{q}(\boldsymbol{d})$—for
all $(\mathcal{D},\boldsymbol{d})\in E^{-}$.

##  3 Preliminaries

LTL-_formulas_ are built from _atoms_ $A_{i}$, $i<\omega$, using the Booleans
and (future-time) temporal operators $\bigcirc$, $\Diamond$, $\Box$,
$\mathbin{\mathsf{U}}$, which we interpret under the _strict semantics_ Gabbay
et al. (2003); Demri et al. (2016). An LTL-_interpretation_ ${\mathcal{I}}$
identifies those atoms $A_{i}$ that are _true_ at each time instant
$n\in\mathbb{N}$, written ${\mathcal{I}},n\models A_{i}$. The truth-relation
for atoms is extended inductively to LTL-formulas by taking
${\mathcal{I}},n\models\varphi\mathbin{\mathsf{U}}\psi$ iff
${\mathcal{I}},m\models\psi$, for some $m>n$, and
${\mathcal{I}},k\models\varphi$ for all $k\in(n,m)$, and using the standard
clauses for the Booleans and equivalences
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varphi\equiv\bot\mathbin{\mathsf{U}}\varphi$,
$\Diamond\varphi\equiv\top\mathbin{\mathsf{U}}\varphi$ and
$\Box\varphi\equiv\neg\Diamond\neg\varphi$ with Boolean _constants_ $\bot$ and
$\top$ for ‘false’ and ‘true’.

An _LTL -ontology_, $\mathcal{O}$, is any finite set of LTL-formulas, called
the _axioms_ of $\mathcal{O}$. An interpretation ${\mathcal{I}}$ is a _model_
of $\mathcal{O}$ if all axioms of $\mathcal{O}$ are true at _all times_ in
${\mathcal{I}}$. As mentioned in the introduction, apart from full LTL we
consider its Prior $\Box\Diamond$-fragment
$\textsl{LTL}^{\smash{\Box\Diamond}}$ and
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
whose axioms take the form

$C_{1}\land\dots\land C_{k}~{}\to~{}C_{k+1}$ (3)

with $C_{i}$ given by $C::=A_{i}\mid\bot\mid\Box
C\mid{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}C$. In fact, we could
allow $\Diamond$ on the left-hand side of (3) as $\Diamond C\to C^{\prime}$
can be replaced by ${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}C\to
A$, ${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}A\to A$, $A\to
C^{\prime}$ with fresh $A$.

A _data instance_ is a finite set $\mathcal{D}$ of atoms $A_{i}(\ell)$ with a
_timestamp_ $\ell\in\mathbb{N}$; $\max\mathcal{D}$ is the maximal timestamp in
$\mathcal{D}$. We access data by means of LTL analogues of conjunctive
queries: our _queries_ , $\varkappa$, are constructed from atoms, $\bot$ and
$\top$ using $\land$, $\bigcirc$, $\Diamond$ and $\mathbin{\mathsf{U}}$. The
class of queries that only use operators from
$\Phi\subseteq\\{{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond,\mathbin{\mathsf{U}}\\}$
is denoted by $\mathcal{Q}[\Phi]$; $\mathcal{Q}_{p}[\Phi]$ is its subclass of
_path-queries_ , which take the form (1) or (2); and
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ comprises _simple queries_ in
$\mathcal{Q}[\mathbin{\mathsf{U}}]$ that do not contain subqueries
$\varkappa_{1}\mathbin{\mathsf{U}}\varkappa_{2}$ with an occurrence of
$\mathbin{\mathsf{U}}$ in $\varkappa_{1}$. Note that
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]\subseteq\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$.
The _temporal depth_ $\mathit{tdp}(\varkappa)$ of $\varkappa$ is the maximum
number of nested temporal operators in $\varkappa$.

An interpretation ${\mathcal{I}}$ is a _model_ of a data instance
$\mathcal{D}$ if ${\mathcal{I}},\ell\models A_{i}$ for all
$A_{i}(\ell)\in\mathcal{D}$. $\mathcal{O}$ and $\mathcal{D}$ are _consistent_
if they have a model. We call $k\leq\max\mathcal{D}$ a (_certain_) _answer_ to
the _ontology-mediated query_ $(\mathcal{O},\varkappa)$ over $\mathcal{D}$ and
write $\mathcal{O},\mathcal{D}\models\varkappa(k)$ if
${\mathcal{I}},k\models\varkappa$ in all models ${\mathcal{I}}$ of
$\mathcal{O}$ and $\mathcal{D}$.

Let $\mathcal{L}$ and $\mathcal{Q}$ be an ontology and query language defined
above. The _query-by-example problem_ $\mathsf{QBE}(\mathcal{L},\mathcal{Q})$
we are concerned with in this paper is formulated as follows:

given

an $\mathcal{L}$-ontology $\mathcal{O}$ and an _example set_ $E=(E^{+},E^{-})$
with finite sets $E^{+}$ and $E^{-}$ of _positive_ and, respectively,
_negative_ data instances,

decide

whether $E$ is $\mathcal{Q}$-_separable_ under $\mathcal{O}$ in the sense that
there is a $\mathcal{Q}$-query $\varkappa$ with
$\mathcal{O},\mathcal{D}\models\varkappa(0)$ for all $\mathcal{D}\in E^{+}$
and $\mathcal{O},\mathcal{D}\not\models\varkappa(0)$ for all $\mathcal{D}\in
E^{-}$.

If $\mathcal{L}=\emptyset$, we shorten $\mathsf{QBE}(\emptyset,\mathcal{Q})$
to $\mathsf{QBE}(\mathcal{Q})$. We also consider the $\mathsf{QBE}$ problems
with the input example sets having a _bounded_ number of positive and/or
negative examples, denoted
$\mathsf{QBE}^{\mathsf{b}\text{+}}(\mathcal{L},\mathcal{Q})$,
$\mathsf{QBE}_{\mathsf{b}\\!\text{--}}(\mathcal{L},\mathcal{Q})$, or
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{L},\mathcal{Q})$.
Notations like
$\mathsf{QBE}^{2\text{+}}_{1\text{--}}(\mathcal{L},\mathcal{Q})$ should be
self-explanatory. The size of $\mathcal{O}$, $E$, $\varkappa$, denoted
$|\mathcal{O}$, $|E|$, $|\varkappa|$, respectively, is the number of symbols
in it with the timestamps given in unary.

The next example illustrates the definitions and relative expressive power of
queries with different temporal operators.

######  Example 3.

(a) Let $E=(\\{\mathcal{D}_{1}\\},\\{\mathcal{D}_{2}\\})$ with
$\mathcal{D}_{1}=\\{A(1)\\}$, $\mathcal{D}_{2}=\\{A(2)\\}$. Then
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}A$ separates $E$ but no
$\mathcal{Q}[\Diamond]$-query does. $E$ is not separable under
$\mathcal{O}=\\{{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}A\to A\\}$
by any query $\varkappa$ as $\mathcal{O},\mathcal{D}_{1}\models\varkappa(0)$
implies $\mathcal{O},\mathcal{D}_{2}\models\varkappa(0)$.

(b) Let $E=(\\{\mathcal{D}_{1},\mathcal{D}_{2}\\},\\{\mathcal{D}_{3}\\})$ with
$\mathcal{D}_{1}=\\{A(1),B(2)\\}$, $\mathcal{D}_{2}=\\{A(2),B(3)\\}$,
$\mathcal{D}_{3}=\\{A(3),B(5)\\}$. Then the query
$\Diamond(A\wedge{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}B)$
separates $E$ but no query in $\mathcal{Q}[\Diamond]$ does.

(c) $A\mathbin{\mathsf{U}}B$ separates
$(\\{\\{B(1)\\},\\{A(1),B(2)\\}\\},\\{\\{B(2)\\}\\})$ but no
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$-query
does. $\dashv$

We now establish a few important _polynomial-time reductions_ , $\leq_{p}$,
among the $\mathsf{QBE}$-problems for various query classes, including
$\mathcal{Q}_{p}^{\circ}[\Diamond]$-_queries_ of the form

$\displaystyle\varkappa=\rho_{0}\land\Diamond(\rho_{1}\land\Diamond(\rho_{2}\land\dots\land\Diamond\rho_{n})),$
(4)

where each $\rho_{i}$ is a
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}]$-query
(i.e., $\Diamond$-free
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\\!\Diamond]$-query).

######  Theorem 4.

The following polynomial-time reductions hold:

(_i_.1)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q})\leq_{p}\mathsf{QBE}_{1\text{--}}(\mathcal{L},\mathcal{Q})$,
for any $\mathcal{Q}$ closed under $\land$, and any $\mathcal{L}$ (including
$\mathcal{L}=\emptyset$),

(_i_.2)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q})\leq_{p}\mathsf{QBE}^{2\text{+}}(\mathcal{L},\mathcal{Q})$,
for $\mathcal{L}\in\\{\textsl{LTL},\textsl{LTL}^{\smash{\Box\Diamond}}\\}$,

(_i_.3)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{L},\mathcal{Q}_{p}^{\circ}[\Diamond]))$
and
$\mathsf{QBE}(\mathcal{L},\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{L},\mathcal{Q}_{p}[\Diamond])$,
for any $\mathcal{L}$,

(_ii_.1)

$\mathsf{QBE}(\mathcal{Q}_{p}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
and
$\mathsf{QBE}(\mathcal{Q}_{p}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])\leq_{p}\mathsf{QBE}_{1\text{--}}(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$,

(_ii_.2)

$\mathsf{QBE}(\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])=_{p}\mathsf{QBE}(\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$.

Reductions $(i.1)$–$(i.3)$ work for combined complexity; $(i.1)$, $(i.3)$ also
work for data complexity. The reductions preserve boundedness of the number of
positive/negative examples.

###### Proof.

In (_i_.1), $(E^{+},E^{-})$ with
$E^{-}=\\{\mathcal{D}_{1},\dots,\mathcal{D}_{n}\\}$ is $\mathcal{Q}$-separable
under $\mathcal{O}$ iff each $(E^{+},\\{\mathcal{D}_{i}\\})$ is because if
$\varkappa_{i}$ separates $(E^{+},\\{\mathcal{D}_{i}\\})$, then
$\varkappa_{1}\land\dots\land\varkappa_{n}$ separates $(E^{+},E^{-})$.

In (_i_.2), $(E^{+},E^{-})$ with
$E^{+}=\\{\mathcal{D}_{1},\dots,\mathcal{D}_{n}\\}$, $n>1$, is
$\mathcal{Q}$-separable under $\mathcal{O}$ iff $(E^{\prime+},E^{-})$ is
$\mathcal{Q}$-separable under $\mathcal{O}^{\prime}$ that extends
$\mathcal{O}$ with the following axioms simulating $E^{+}$:

$\displaystyle S_{1}\to A_{1}\lor\dots\lor A_{n},\quad S_{2}\to
A_{1}\lor\dots\lor A_{n},$ $\displaystyle C_{i}\land\Diamond A_{j}\to X,\quad
D_{i}\land\Diamond A_{j}\to X,\ \ \text{for $X(i)\in\mathcal{D}_{j}$,}$

where $S_{1}$, $S_{2}$, $A_{k}$, $C_{l}$, $D_{l}$, for $l\leq
n^{\prime}=\max_{i}\max\mathcal{D}_{i}$, are fresh and $E^{\prime+}$ consists
of $\\{C_{0}(0),\dots,C_{k}(n^{\prime}),S_{1}(n^{\prime}+1)\\}$ and
$\\{D_{0}(0),\dots,D_{k}(n^{\prime}),S_{2}(n^{\prime}+1)\\}$.

(_i_.3) Using
$[\rho_{0}\wedge\Diamond(\rho_{1}\wedge\bigwedge_{i}\Diamond\varkappa_{i})]\equiv[\rho_{0}\wedge\bigwedge_{i}\Diamond(\rho_{1}\wedge\Diamond\varkappa_{i})]$,
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond\varkappa\equiv\Diamond{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa$
and
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}(\varkappa\land\varkappa^{\prime})\equiv({\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa^{\prime})$
we convert, in polytime, each
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$-query
to an equivalent conjunction of $\mathcal{Q}_{p}^{\circ}[\Diamond]$-queries.
Thus, there is
$\boldsymbol{q}\in\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
separating $(E^{+},E^{-})$ iff there are polysize
$\boldsymbol{q}_{\mathcal{D}}\in\mathcal{Q}_{p}^{\circ}[\Diamond]$ separating
$(E^{+},\\{\mathcal{D}\\})$, for each $\mathcal{D}\in E^{-}$.

(_ii_.1) The first two reductions are shown by adding to
$E^{+}\ni\mathcal{D}$, for some $\mathcal{D}$, the data instance
$\mathcal{D}^{\prime}=\\{A(mn)\mid A(n)\in\mathcal{D}\\}$ with
$m=\max\mathcal{D}+2$. Now, if $\mathcal{D}\models\varkappa(0)$ and
$\mathcal{D}^{\prime}\models\varkappa(0)$, for
$\varkappa\in\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$, then $\varkappa$ is
equivalent to a $\mathcal{Q}_{p}[\Diamond]$-query. The third reduction,
illustrated below for $E^{+}=\\{\mathcal{D}^{+}_{1},\mathcal{D}^{+}_{2}\\}$
and $E^{-}=\\{\mathcal{D}^{-}_{1},\mathcal{D}^{-}_{2}\\}$, transforms $E$ into
two positive and _one negative_ example using ‘pads’ of fresh atoms $B$, $C$.
We show

$\mathcal{D}^{\prime\prime+}_{1}$$\mathcal{D}_{1}^{+}$$0$$B$$1$$C$$2$$\ldots$$C$
$\mathcal{D}^{\prime+}_{2}$$\mathcal{D}_{2}^{+}$$0$$1$$B$$m$$C$$\ldots$$C$

$\mathcal{D}^{\prime-}$$\mathcal{D}_{1}^{-}$$\mathcal{D}^{-}_{2}$$0$$1$$B$$m$$C$$C$$2m$$B$$3m$$C$$C$$4m$

that $E$ is $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-separable iff
$(\\{\mathcal{D}^{\prime\prime+}_{1},\mathcal{D}^{\prime+}_{2}\\},\\{\mathcal{D}^{\prime-}\\})$
is.

(_ii_.2) The first reduction is established by modifying every $\mathcal{D}$
in the given $E$ as illustrated below using fresh atoms $A_{i}$ and $B_{j}$
that encode ${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{i}A$ and
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{j}B$, respectively:

$\mathcal{D}$$0$$A$$1$$2$$B$$3$
$A_{1},\\!B_{3}$$0$$A,B_{2}$$1$$B_{1}$$2$$B$$3$$\mathcal{D}^{\prime}$

Then $E$ is
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\\!\Diamond]$-separable
iff $E^{\prime}$ is $\mathcal{Q}[\Diamond]$-separable. The converse and the
second reduction are similar to (_ii_.1). ∎

##  4 QBE without Ontologies

We start investigating the complexity of the $\mathsf{QBE}$ problems for LTL
by considering queries without mediating ontologies.

######  Theorem 5.

The $\mathsf{QBE}$-problems for the classes of queries defined above (with the
empty ontology) belong to the complexity classes shown in Table 1.

We comment on the proof in the remainder of this section.

${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond$-queries. NP-
hardness is established by reduction of the consistent subsequence existence
problems (Fraser, 1996, Theorems 2.1, 2.2) in tandem with Theorem 4;
membership in NP follows from the fact that separating queries, if any, can
always be taken of polynomial size.

Tractability is shown using dynamic programming. We explain the idea for
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$,
$E^{+}=\\{\mathcal{D}_{1}^{+},\mathcal{D}_{2}^{+}\\}$ and
$E^{-}=\\{\mathcal{D}_{1}^{-},\mathcal{D}_{2}^{-}\\}$. Suppose $\varkappa$
takes the form (1) with $\rho_{n}\neq\top$. Then
$\mathcal{D}\models\varkappa(0)$ iff there is a strictly monotone map
$f\colon[0,n]\rightarrow[0,\max\mathcal{D}]$ with $f(0)=0$, $f(i+1)=f(i)+1$ if
${\boldsymbol{o}}_{i}={\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}$,
and $\rho_{i}\subseteq t_{\mathcal{D}}(f(i))=\\{A\mid
A(f(i))\in\mathcal{D}\\}$. We call such an $f$ a _satisfying assignment_ for
$\varkappa$ in $\mathcal{D}$. Let $S_{i,j}$ be the set of tuples
$(k,\ell_{1},\ell_{2},n_{1},n_{2})$ such that $\ell_{1}\leq
i\leq\max\mathcal{D}_{1}^{+}$, $\ell_{2}\leq j\leq\max\mathcal{D}_{2}^{+}$,
and there is
$\varkappa=\rho_{0}\land{\boldsymbol{o}}_{1}(\rho_{1}\land\dots\land{\boldsymbol{o}}_{k}\rho_{k})$
for which $(i)$ there are satisfying assignments $f_{1},f_{2}$ in
$\mathcal{D}_{1}^{+}$ and $\mathcal{D}_{2}^{+}$ with $f_{1}(k)=\ell_{1}$ and
$f_{2}(k)=\ell_{2}$, respectively, and $(ii)$ $n_{1}$ is minimal with a
satisfying assignment $f$ for $\varkappa$ in $\mathcal{D}_{1}^{-}$ having
$f(k)=n_{1}$, and $n_{1}=\infty$ if there is no such $f$; and similarly for
$n_{2}$, $\mathcal{D}_{2}^{-}$. It suffices to compute
$S_{\max\mathcal{D}_{1}^{+},\max\mathcal{D}_{2}^{+}}$ in polytime. This can be
done incrementally by initially observing that $S_{0,j}$ can only contain
$(0,0,0,0,0)$, which is the case if there is $\rho_{0}\subseteq
t_{\mathcal{D}_{1}^{+}}(0)$, $\rho_{0}\subseteq t_{\mathcal{D}_{2}^{+}}(0)$
and $\rho_{0}\not\subseteq t_{\mathcal{D}_{1}^{-}}(0)$, $\rho_{0}\not\subseteq
t_{\mathcal{D}_{2}^{-}}(0)$ (and similarly for $S_{i,0}$).

$\mathbin{\mathsf{U}}$-queries. NP-hardness for
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$,
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ follows from Theorem 4 $(ii.1)$,
$(ii.2)$ and NP-hardness for
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond$-queries.

The upper bounds are shown by reduction of
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$\- and
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separability to the simulation and
containment problems for transition systems Kupferman and Vardi (1996). A
_transition system_ , $S$, is a digraph each of whose nodes and edges is
labelled by some set of symbols from a node or, respectively, edge alphabet;
$S$ also has a designated set $S_{0}$ of _start nodes_. A _run_ of $S$ is a
path in digraph $S$, starting in $S_{0}$, together with all of its labels. The
_computation tree_ of $S$ is the tree unravelling $\mathfrak{T}_{S}$ of $S$.
For systems $S$ and $S^{\prime}$ over the same alphabets, we say that $S$ is
_contained_ in $S^{\prime}$ if, for every run $r$ of $S$, there is a run
$r^{\prime}$ of $S^{\prime}$ such that $r$ and $r^{\prime}$ have the same
length and the labels on the states and edges in $r$ are subsumed by the
corresponding labels in $r^{\prime}$. $S$ is _simulated_ by $S^{\prime}$ if
$\mathfrak{T}_{S}$ is _finitely embeddable_ into $\mathfrak{T}_{S^{\prime}}$
in the sense that every finite subtree222A _subtree_ is a convex subset of
$\mathfrak{T}_{S}$’s nodes with some start node. of $\mathfrak{T}_{S}$ can be
homomorphically mapped into $\mathfrak{T}_{S^{\prime}}$ preserving
(subsumption of) node and edge labels.

Now, let $E=(E^{+},E^{-})$ with $E^{\sigma}=\\{\mathcal{D}_{i}\mid i\in
I^{\sigma}\\}$, for $\sigma\in\\{+,-\\}$ and disjoint $I^{+}$ and $I^{-}$, and
let $\Sigma$ be the signature of $E$. For each $i\in I^{+}\cup I^{-}$, we take
a transition system $S^{i}$ with states
$0^{i},\dots,(\max\mathcal{D}_{i}+1)^{i}$, where $(\max\mathcal{D}_{i}+1)^{i}$
is labelled with $\emptyset$ and the remaining $j^{i}$ by $\\{A\mid
A(j)\in\mathcal{D}_{i}\\}$. Transitions are $j^{i}\to k^{i}$, for $0\leq
j<k\leq\max\mathcal{D}_{i}+1$, that are labelled by
$\\{A\in\Sigma\cup\\{\bot\\}\mid A(n)\in\mathcal{D}_{i},n\in(j,k)\\}$ and
$(\max\mathcal{D}_{i}+1)^{i}\to(\max\mathcal{D}_{i}+1)^{i}$ with label
$\Sigma^{\bot}=\Sigma\cup\\{\bot\\}$. Thus, $\mathcal{D}_{i}$ shown on the
left below gives rise to $S^{i}$ on the right:

$0$$A,\\!B$$1$$B,\\!C$$2$
$\emptyset$$\\{A,B\\}$$\Sigma^{\bot}$$\\{B,C\\}$$\Sigma^{\bot}$$\\{A,B\\}$$\emptyset$$\Sigma^{\bot}$$\\{B,C\\}$$\\{B\\}$$\Sigma^{\bot}$

We form the direct product (synchronous composition) $\mathfrak{P}$ of
$\\{S^{i}\mid i\in I^{+}\\}$, for $I^{+}=\\{1,\dots,l\\}$, whose states are
vectors $(s_{1},\dots,s_{l})$ of states $s_{i}\in S^{i}$, which are labelled
by the intersection of the labels of $s_{i}$ in $S^{i}$, with transitions
$(s_{1},\dots,s_{l})\to(p_{1},\dots,p_{l})$, if $s_{i}\to p_{i}$ in $S^{i}$
for all $i$, also labelled by the intersection of the component transition
labels. On the other hand, we take the disjoint union $\mathfrak{N}$ of
$S^{i}$, for $i\in I^{-}$, and establish the following separability criterion:

######  Theorem 6.

$(i)$ $E$ is not $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separable iff
$\mathfrak{P}$ is simulated by $\mathfrak{N}$. $(ii)$ $E$ is not
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-separable iff $\mathfrak{P}$ is
contained in $\mathfrak{N}$.

######  Example 7.

For the example set depicted below, in which the only negative instance is on
the right-hand side,

$0$$1$$2$$3$$A_{2},\\!B_{1}$$4$$B_{2}$$5$ $0$$1$$A_{1},\\!B_{2}$$2$$B_{1}$$3$
$0$$1$$B_{1}$$2$$3$$B_{2}$$4$

$\mathfrak{T}_{\mathfrak{P}}$ contains the subtree

$(0^{1},0^{2})$$(3^{1},1^{2})$$\emptyset$$(4^{1},3^{2})$$B_{1}$$A_{1},B_{2}$$(5^{1},2^{1})$$B_{2}$$A_{2},B_{1}$

where only the last $\mathfrak{P}$-node of a
$\mathfrak{T}_{\mathfrak{P}}$-node (a sequence) is indicated together with the
atoms that are true at nodes and on edges. Intuitively,
$\mathfrak{T}_{\mathfrak{P}}$ ‘represents’ all possible
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-queries and its paths represent
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-queries $\varkappa$ such that
$\mathcal{O},\mathcal{D}\models\varkappa(0)$ for all $\mathcal{D}\in E^{+}$.
The $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-query given by the subtree above
is $\varkappa=\Diamond\big{(}((A_{1}\land
B_{2})\mathbin{\mathsf{U}}B_{1})\land((A_{2}\land
B_{1})\mathbin{\mathsf{U}}B_{2})\big{)}$. The subtree is not embeddable into
$\mathfrak{T}_{\mathfrak{N}}$ (obtained for the negative instance), so
$\varkappa$ separates $E$. Observe that every path in
$\mathfrak{T}_{\mathfrak{P}}$ (and in the subtree above) is embeddable into
$\mathfrak{T}_{\mathfrak{N}}$.

By inspecting the structure of $\mathfrak{P}$ and $\mathfrak{N}$ we observe
that if $\mathfrak{P}$ has a run that is not embeddable into any run of
$\mathfrak{N}$, then we can find such a run of length $\leq
M=\min\\{\max\mathcal{D}_{i}\mid i\in I^{+}\\}$ (any longer run has
$\emptyset$-labels on its states after the $M$th one). Thus, we can guess the
required run and check in P if it is correct, establishing the NP upper bound
for $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$. To show the PSpace upper bound
for $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$, we notice that if there is a
finite subtree of $\mathfrak{T}_{\mathfrak{P}}$ that is not embeddable into
$\mathfrak{T}_{\mathfrak{N}}$, then the full subtree
$\smash{\mathfrak{T}_{\mathfrak{P}}^{M}}$ of depth $M$ is not embeddable into
$\mathfrak{T}_{\mathfrak{N}}$, which can be checked by constructing
$\smash{\mathfrak{T}_{\mathfrak{P}}^{M}}$ branch-by-branch while checking all
possible embeddings of these branches into $\mathfrak{T}_{\mathfrak{N}}$.
Finally, we have the P upper bound for $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$
with a bounded number of positive examples because $\mathfrak{P}$ is
constructible in polytime and checking simulation between transition systems
is P-complete Kupferman and Vardi (1996). Interestingly, the smallest
separating query we can construct in this case is of the same size as
$\smash{\mathfrak{T}_{\mathfrak{P}}^{M}}$, i.e., exponential in $|E^{+}|$;
however, we can check its existence in polytime.

The PSpace upper bound for $\mathcal{Q}[\mathbin{\mathsf{U}}]$ requires a more
sophisticated notion of simulation between transition systems.

######  Example 8.

The example set below, where only the rightmost instance is negative, is
separated by the $\mathcal{Q}[\mathbin{\mathsf{U}}]$-query

$0$$1$$B,C$$2$ $0$$1$$A$$2$$B$$3$$B,C$$4$ $0$$1$$A$$2$$B$$3$$4$$B,C$$5$

$(A\mathbin{\mathsf{U}}B)\mathbin{\mathsf{U}}C$ but is not
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separable by Theorem 6. $\dashv$

We prove a $\mathcal{Q}[\mathbin{\mathsf{U}}]$-inseparability criterion using
transition systems whose non-initial/sink states are _pairs_ of sets of
numbers, and transitions are of _two_ types. The picture below shows a data
instance and the induced transition system (where $z$ has incoming arrows
labelled by $\Sigma^{\bot}$ from all states

$0$$A$$1$$B$$2$$B,\\!C$$3$$0$$\emptyset\\{1\\}$$\\!\\!A$$\\{1\\}\\{2\\}$$\\!\\!B$$\emptyset\\{2\\}$$B$$\\{2\\}\\{3\\}$$B,C$$\emptyset\\{3\\}$$B,C$$\\{1,2\\}\\{3\\}$$B,C$$\emptyset\\{2,3\\}$$B$$u$$\\!\\!\\!\\!\\!\Sigma^{\bot}$$z$$\emptyset$$A$$\emptyset$$B$$B$

but $u$, which are all omitted). Each arrow from $0$ leads to a state
$\\{1,\dots,n-1\\}\\{n\\}$; it represents a formula
$\varphi\mathbin{\mathsf{U}}\psi$ that is true at $0$, with the arrow label
indicating the non-nested atoms of $\varphi$ and the state label indicating
the atoms of $\psi$. Each black (resp., red) arrow from
$\boldsymbol{s}_{1}\boldsymbol{s}_{2}$ to
$\boldsymbol{s}^{\prime}_{1}\boldsymbol{s}^{\prime}_{2}$ represents a
$\mathbin{\mathsf{U}}$-formula
$\alpha_{\boldsymbol{s}_{2}\to\boldsymbol{s}^{\prime}_{1}\boldsymbol{s}^{\prime}_{2}}$
(resp.,
$\alpha_{\boldsymbol{s}_{1}\to\boldsymbol{s}^{\prime}_{1}\boldsymbol{s}^{\prime}_{2}}$)
that is true at all points in $\boldsymbol{s}_{2}$ (resp.,
$\boldsymbol{s}_{1}$). The black and red transitions are arranged in such a
way that a transition from
$\boldsymbol{s}^{\prime\prime}_{1}\boldsymbol{s}^{\prime\prime}_{2}$ to
$\boldsymbol{s}_{1}\boldsymbol{s}_{2}$ with an arrow label $\lambda$ and
$\boldsymbol{s}_{1}\boldsymbol{s}_{2}$-label $\mu$ represents the
$\mathbin{\mathsf{U}}$-formula
$(\lambda\land\bigwedge\alpha_{\boldsymbol{s}_{1}\to\boldsymbol{s}^{\prime}_{1}\boldsymbol{s}^{\prime}_{2}})\mathbin{\mathsf{U}}(\mu\land\bigwedge\alpha_{\boldsymbol{s}_{2}\to\boldsymbol{s}^{\prime}_{1}\boldsymbol{s}^{\prime}_{2}})$
and similarly for the transitions from $0$. A version of Theorem 6 for
$\mathcal{Q}[\mathbin{\mathsf{U}}]$ and a PSpace-algorithm are given in the
full paper.

##  5 QBE with
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-Ontologies

Recall from Artale et al. (2021) that, for any
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology
$\mathcal{O}$ and data instance $\mathcal{D}$ consistent with $\mathcal{O}$,
there is a _canonical model_ $\mathcal{C}_{\mathcal{O},\mathcal{D}}$ of
$\mathcal{O}$ and $\mathcal{D}$ such that, for any query $\varkappa$ and any
$k\in\mathbb{N}$, we have $\mathcal{O},\mathcal{D}\models\varkappa(k)$ iff
$\mathcal{C}_{\mathcal{O},\mathcal{D}}\models\varkappa(k)$.

Let $\mathit{sub}_{\mathcal{O}}$ be the set of subformulas of the $C_{i}$ in
the axioms (3) of $\mathcal{O}$ and their negations. A _type for_
$\mathcal{O}$ is any maximal subset
$\textit{tp}\subseteq\mathit{sub}_{\mathcal{O}}$ consistent with
$\mathcal{O}$. Let ${\boldsymbol{T}}$ be the set of all types for
$\mathcal{O}$. Given an interpretation ${\mathcal{I}}$, we denote by
$\textit{tp}_{{\mathcal{I}}}(n)$ the type for $\mathcal{O}$ that holds at
$n\in\mathbb{N}$ in ${\mathcal{I}}$. For $\mathcal{O}$ consistent with
$\mathcal{D}$, we abbreviate
$\textit{tp}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$ to
$\textit{tp}_{\mathcal{O},\mathcal{D}}$. The canonical models have a periodic
structure in the following sense:

######  Proposition 9.

For any
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
ontology $\mathcal{O}$ and any data instance $\mathcal{D}$ consistent with
$\mathcal{O}$, there are $s_{\mathcal{O},\mathcal{D}}\leq 2^{|\mathcal{O}|}$
and $p_{\mathcal{O},\mathcal{D}}\leq 2^{2|\mathcal{O}|}$ such that
$\textit{tp}_{\mathcal{O},\mathcal{D}}(n)=\textit{tp}_{\mathcal{O},\mathcal{D}}(n+p_{\mathcal{O},\mathcal{D}})$,
for all $n\geq\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}$. Deciding
$\mathcal{C}_{\mathcal{O},\mathcal{D}}\models\xi(\ell)$, for a binary $\ell$
and a conjunction of atoms $\xi$, is in PSpace / P for combined / data
complexity.

We now show that the combined complexity of $\mathsf{QBE}$ with $\Diamond$\-
and ${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond$-queries is
PSpace-complete in both bounded and unbounded cases, i.e., as complex as
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
reasoning.

######  Theorem 10.

Let
$\mathcal{Q}\in\\{\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond],\mathcal{Q}[\Diamond],\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond],\mathcal{Q}_{p}[\Diamond]\\}$.
Then
$\mathsf{QBE}(\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q})$
and
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}\\!(\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q})$
are both PSpace-complete for combined complexity.

###### Proof.

PSpace-hardness is inherited from that of
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$.
We briefly sketch the proof of the matching upper bound for
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
using the reduction of Theorem 4 $(i.3)$. We can assume that $\mathcal{O}$ and
$\mathcal{D}$ are consistent for any $\mathcal{D}\in E^{+}\cup E^{-}$. For if
$\mathcal{O}$ and $\mathcal{D}\in E^{-}$ are inconsistent, then $E$ is not
$\mathcal{Q}$-separable under $\mathcal{O}$ as
$\mathcal{O},\mathcal{D}\models\varkappa(0)$ for all
$\varkappa\in\mathcal{Q}$; if $\mathcal{O}$ and $\mathcal{D}\in E^{+}$ are
inconsistent, then $E$ is separable iff
$(E^{+}\setminus\\{\mathcal{D}\\},E^{-})$ is. Checking consistency is known to
be PSpace-complete.

Given an
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology
$\mathcal{O}$ and an example set $E$, let

$k=\max_{\mathcal{D}\in E^{+}\cup
E^{-}}(\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}),\quad\textstyle
m=\prod_{\mathcal{D}\in E^{+}\cup E^{-}}p_{\mathcal{O},\mathcal{D}},$

where $s_{\mathcal{O},\mathcal{D}}$ and $p_{\mathcal{O},\mathcal{D}}$ in
$\mathcal{C}_{\mathcal{O},\mathcal{D}}$ are from Proposition 9. We show that
if $E$ is
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$-separable
under $\mathcal{O}$, then it is separated by a conjunction of $|E^{-}|$-many
$\varkappa\in\mathcal{Q}_{p}^{\circ}[\Diamond]$ of $\Diamond$-depth $\leq k+1$
and $\bigcirc$-depth $\leq k+m$ in (4). Indeed, in this case any
$(E^{+},\\{\mathcal{D}\\})$, for $\mathcal{D}\in E^{-}$, is separated under
$\mathcal{O}$ by some $\varkappa$ of the form (4) with the $\rho_{l}$ of
$\bigcirc$-depth $\leq k+m$ because
$\rho_{l}=\bigwedge_{i=0}^{\ell}{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{i}\lambda_{i}$
with $\ell>k+m$ can be replaced by

$\textstyle\bigwedge_{i=0}^{k}{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{i}\lambda_{i}\land\bigwedge_{j=1}^{m}{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{k+j}\bigwedge_{i\leq\ell,j=(i-k)\
\text{mod}\ m}\lambda_{i}.$

In addition, if $n>k$ in (4), then $(E^{+},\\{\mathcal{D}^{-}\\})$ is
separated by

$\textstyle\rho_{0}\land\Diamond(\rho_{1}\land\Diamond(\rho_{2}\land\dots\land\Diamond\rho_{k}))\land\bigwedge_{i=k+1}^{n}\Diamond^{k+1}\rho_{i},$

and so by some
$\rho_{0}\land\Diamond(\rho_{1}\land\dots\land\Diamond(\rho_{k}\wedge\Diamond\rho_{j}))$
with $k<j\leq n$. Our nondeterministic PSpace-algorithm incrementally guesses
the $\rho_{l}$ and checks if they are satisfiable in the relevant part of the
relevant $\mathcal{C}_{\mathcal{O},\mathcal{D}}$ bounded by $k+m$. ∎

The situation is quite different for queries with $\mathbin{\mathsf{U}}$:

######  Theorem 11.

$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$
is in ExpTime for combined complexity,
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$
is in ExpSpace, and
$\smash{\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$
is NExpTime-hard.

###### Proof.

For the upper bounds, we again assume that $\mathcal{O}$ and $\mathcal{D}$ are
consistent for all $\mathcal{D}\in E^{+}\cup E^{-}$. Observe that Theorem 6
continues to hold in the presence of
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
ontologies $\mathcal{O}$ but we need a different construction of transition
systems $S^{i}$ that represent all
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-queries mediated by $\mathcal{O}$ over
$\mathcal{D}_{i}$. We illustrate it for $\mathcal{O}=\\{A\to
C\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}B,\,B\to{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{2}B,\,B\to{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}C\\}$
and $\mathcal{D}_{i}=\\{A(0)\\}$ below, where the picture on the left shows
the canonical model of $\mathcal{O},\mathcal{D}_{i}$ (see Proposition 9) and
next to it is $S^{i}$ (the omitted labels on transitions are $\Sigma^{\bot}$).

$\mathbf{A},C$
$\mathbf{0}$$B$$1$$C$$2$$B$$3$$0$$A,C$$1$$B$$2$$C$$3$$B$$B$$\emptyset$$B$$B$$C$$\emptyset$$B,C$$\emptyset$

In general, the size of $S^{i}$ is $|\mathcal{D}_{i}|+O(2^{|\mathcal{O}|})$
and the product of $S^{i}$, $\mathcal{D}_{i}\in E^{+}$ is of size
$O(2^{|\mathcal{O}|+|E^{+}|})$. The upper bounds now follow from P and PSpace
completeness of checking simulation and containment for transition systems.

Now we sketch the proof of the lower bound. Let $\boldsymbol{M}$ be a non-
deterministic Turing machine that accepts $\Sigma$-words
$\boldsymbol{x}=x_{1}\dots x_{n}$ in $N=2^{\textit{poly}(|\boldsymbol{x}|)}$
steps and erases the tape after a successful computation. We represent
configurations $\mathfrak{c}$ of a computation of $\boldsymbol{M}$ on
$\boldsymbol{x}$ by an $N-1$-long word (with sufficiently many blanks at the
end), in which $y$ in the active cell is replaced by $(q,y)$ with the current
state $q\in Q$. An accepting computation of $\boldsymbol{M}$ on
$\boldsymbol{x}$ is encoded by the $N^{2}$-long word
$w=\sharp\mathfrak{c}_{1}\,\sharp\,\mathfrak{c}_{2}\,\sharp\,\dots\,\sharp\,\mathfrak{c}_{N-1}\,\sharp\,\mathfrak{c}_{N}$
over $\Xi=\Sigma\cup(Q\times\Sigma)\cup\\{\sharp\\}$. Thus, a word $w$ of
length $N^{2}$ encodes an accepting computation iff it starts with the initial
configuration $\mathfrak{c}_{1}$ preceded by $\sharp$, ends with the accepting
configuration $\mathfrak{c}_{\it acc}$, and every two length 3 subwords at
distance $N$ apart form a _legal tuple_ (Sipser, 1997, Theorem 7.37).

We define $\mathcal{O}$ and
$E=(\\{\mathcal{D}_{1}^{+},\mathcal{D}_{2}^{+}\\},\\{\mathcal{D}^{-}\\})$ so
that their canonical models look as follows, for
$\Xi=\\{a_{1},\ldots,a_{k}\\}$:

$\mathcal{C}_{\mathcal{O},{\mathcal{D}_{1}^{+}}}$$\mathfrak{c}_{1}$$\mathfrak{c}_{acc}$$0$$\sharp$$1$$N$${\Xi}$$N+1$${\Xi}$$N^{2}-N+1$$N^{2}$

$\mathcal{C}_{\mathcal{O},{\mathcal{D}_{2}^{+}}}$$0$$1$$a_{1}\\!,\\!\\!C$$N^{2}+1$$C$$a_{2}\\!,\\!\\!C$$C$$a_{k}\\!,\\!\\!C$$C$$N^{2}+2|\Sigma^{\prime}|$$a_{1}\\!,\\!\\!C$$C$$a_{k}\\!,\\!\\!C$$C$$N^{2}+2|\Sigma^{\prime}|N^{2}$

$\mathcal{C}_{\mathcal{O},{\mathcal{D}^{-}}}$$\mathcal{D}_{\mathfrak{t}_{i}}$$0$$1$$\Xi$$2$$\Xi$$N^{2}$$\Xi
C$$N^{2}+2$$C$$\Xi C$$C$$3N^{2}$$(2i+1)N^{2}$

where $\mathcal{D}_{\mathfrak{t}_{i}}\\!\\!=$$0$$\Xi C$$1$$\Xi
C$$a$$b$$c$$\Xi$$N^{2}-N$$\Xi$$d$$e$$f$$N^{2}$$\Xi$$\Xi$$2N^{2}-N-3$

and $\mathfrak{t}_{i}=(a,b,c,d,e,f)$ is the lexicographically $i$-th illegal
tuple. The parts of the canonical models shown above are of exponential size;
however, due to their repetitive nature, they can be described by a
polynomial-size
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$
ontology $\mathcal{O}$ as in Ryzhikov et al. (2021). We show that the
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-query

$\varkappa=\Diamond(\rho_{1}\land C\mathbin{\mathsf{U}}(\rho_{2}\land
C\mathbin{\mathsf{U}}(\dots(\rho_{N^{2}-1}\land(C\mathbin{\mathsf{U}}\rho_{N^{2}}))\dots))),$

where $\rho_{1}\dots\rho_{N^{2}}$ encodes an accepting computation of
$\boldsymbol{M}$ on $\boldsymbol{x}$, is the only type of query that can
separate $E$ under $\mathcal{O}$. ∎

As for _data_ complexity, we show that
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontologies
come essentially for free:

######  Theorem 12.

The results of Theorem 5 continue to hold for queries mediated by a fixed
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology.

Intuitively, the reason is that, given a fixed
$\textsl{LTL}_{\smash{\textit{horn}}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology
$\mathcal{O}$, we can compute the types of the canonical model
$\mathcal{C}_{\mathcal{O},\mathcal{D}}$, for consistent $\mathcal{O}$ and
$\mathcal{D}$, in polynomial time in $\mathcal{D}$ by Proposition 9, with the
length $M$ from Section 4 being polynomial in $E$. Checking consistency of
$\mathcal{D}$ and fixed $\mathcal{O}$ is known to be in P Artale et al.
(2021).

##  6 QBE with $\textsl{LTL}^{\smash{\Box\Diamond}}$-Ontologies

In this section, we investigate separability by $\Diamond$-queries under
$\textsl{LTL}^{\smash{\Box\Diamond}}$-ontologies. Remarkably, we show that,
for data complexity, $\textsl{LTL}^{\smash{\Box\Diamond}}$-ontologies also
come for free despite admitting arbitrary Boolean operators; cf., Schaerf
(1993).

######  Theorem 13.

Let $\mathcal{Q}\in\\{\mathcal{Q}_{p}[\Diamond],\mathcal{Q}[\Diamond]\\}$. If
$E$ is $\mathcal{Q}$-separable under an
$\textsl{LTL}^{\smash{\Box\Diamond}}$-ontology $\mathcal{O}$, then $E$ can be
separated under $\mathcal{O}$ by a $\mathcal{Q}$-query of polysize in $E$ and
$\mathcal{O}$. $\mathsf{QBE}(\textsl{LTL}^{\smash{\Box\Diamond}},\mathcal{Q})$
and
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\textsl{LTL}^{\smash{\Box\Diamond}},\mathcal{Q})$
are $\Sigma_{2}^{p}$-complete for combined complexity. The presence of
$\textsl{LTL}^{\smash{\Box\Diamond}}$-ontologies has no effect on the data
complexity, which remains the same as in Theorem 5.

We comment on the proof of this theorem for $\mathcal{Q}_{p}[\Diamond]$.
Taking into account NP-completeness of checking if $\mathcal{O}$ is consistent
with $\mathcal{D}$ and tractability of this problem for a fixed $\mathcal{O}$
Artale et al. (2021), we can assume, as in Theorem 10, that $\mathcal{O}$ and
$\mathcal{D}$ are consistent for each $\mathcal{D}\in E^{+}\cup E^{-}$.
Observe first that if $E$ is separated by
$\varkappa\in\mathcal{Q}_{p}[\Diamond]$ of the form (1) under an
$\textsl{LTL}^{\smash{\Box\Diamond}}$-ontology $\mathcal{O}$, then, as follows
from Ono and Nakamura (1980), for any $\mathcal{D}\in E^{-}$, there is a model
$\mathcal{J}_{\mathcal{D}}\not\models\varkappa(0)$ of $\mathcal{O}$ and
$\mathcal{D}$ whose types form a sequence

$\\!\textit{tp}_{0},\dots,\textit{tp}_{k},\textit{tp}_{k+1},\dots,\textit{tp}_{k+l},\dots,\textit{tp}_{k+1},\dots,\textit{tp}_{k+l},\dots$
(5)

with $\max\mathcal{D}\leq k\leq\max\mathcal{D}+|\mathcal{O}|$ and
$l\leq|\mathcal{O}|$. This allows us to find a separating $\varkappa$ of
polysize in $E$, $\mathcal{O}$. Indeed, let $K$ be the maximal $k$ in (5) over
all $\mathcal{D}\in E^{-}$. If the depth $n$ of $\varkappa$ is $\leq K$, we
are done. If $n>K$, we shorten $\varkappa$ as follows. Consider the prefix
$\varkappa^{\prime}$ of $\varkappa$ formed by $\rho_{0},\dots,\rho_{K}$. If
$\mathcal{J}_{\mathcal{D}}\not\models\varkappa^{\prime}(0)$ for all
$\mathcal{D}\in E^{-}$, we are done. Otherwise, for each $\mathcal{D}\in
E^{-}$, we pick a $\rho_{i}$, $i>K$, with
$\rho_{i}\not\subseteq\textit{tp}_{k+j}$ for any $j\leq l$; it must exist as
$\mathcal{J}_{\mathcal{D}}\not\models\varkappa(0)$. Then we construct
$\varkappa^{\prime\prime}$ by omitting from $\varkappa$ all $\rho_{l}$ that
are different from those in $\varkappa^{\prime}$ and the chosen $\rho_{i}$
with $i>K$. Clearly, $\varkappa^{\prime\prime}$ is as required.

A $\Sigma_{2}^{p}$-algorithm guesses $\varkappa$ and
${\mathcal{J}}_{\mathcal{D}}$, for $\mathcal{D}\in E^{-}$, and checks in
polytime that ${\mathcal{J}}_{\mathcal{D}}\models\mathcal{O},\mathcal{D}$ and
${\mathcal{J}}_{\mathcal{D}}\not\models\varkappa(0)$ and in coNP Ono and
Nakamura (1980) that $\mathcal{O},\mathcal{D}\models\varkappa(0)$ for all
$\mathcal{D}\in E^{+}$. The lower bound is shown by reduction of the validity
problem for fully quantified Boolean formulas
$\exists\boldsymbol{p}\,\forall\boldsymbol{q}\,\psi$, where
$\boldsymbol{p}=p_{1},\dots,p_{k}$ and $\boldsymbol{q}=q_{1},\dots,q_{m}$ are
all propositional variables in $\psi$. We can assume that $\psi$ is not a
tautology and $\lnot\psi\not\models x$ for $x\in\\{p_{i},\lnot
p_{i},q_{j},\lnot q_{j}\mid i\leq k,j\leq m\\}$. Let $E=(E^{+},E^{-})$ with
$E^{+}=\\{\mathcal{D}_{1},\mathcal{D}_{2}\\}$, $E^{-}=\\{\mathcal{D}_{3}\\}$,
where

$\mathcal{D}_{1}=\\{B_{1}(0)\\},\ \mathcal{D}_{2}=\\{B_{2}(0)\\},\
\mathcal{D}_{3}=\\{q_{1}(0),\dots,q_{m}(0)\\},$

and let $\mathcal{O}$ contain the following axioms with fresh atoms
$B_{1},B_{2},A_{i},\bar{A}_{i}$, for $i=1,\dots,k$:

$\displaystyle B_{1}\lor B_{2}\rightarrow\neg\psi,\quad$
$\displaystyle\textstyle
p_{i}\rightarrow\Diamond\big{(}\bar{A}_{i}\wedge\bigwedge_{j\not=i}(A_{j}\wedge\bar{A}_{j})\big{)},$
$\displaystyle\textstyle\neg
p_{i}\rightarrow\Diamond\big{(}A_{i}\wedge\bigwedge_{j\not=i}(A_{j}\wedge\bar{A}_{j})\big{)}.$

Then $\exists\boldsymbol{p}\,\forall\boldsymbol{q}\,\psi$ is valid iff $E$ is
$\mathcal{Q}_{p}[\Diamond]$-separable under $\mathcal{O}$.

We obtain the NP upper bounds in data complexity using the same argument as
for the $\Sigma_{2}^{p}$-upper bound and observing that checking
$\mathcal{O},\mathcal{D}\models\varkappa(0)$ is in P in data complexity. The
NP lower bounds are inherited from the ontology-free case. The proof of the P
upper bounds is more involved. We illustrate the idea for $\mathcal{O}$ with
arbitrary Boolean but without temporal operators. In this case, one can show
(which is non-trivial) that $\mathcal{O},\mathcal{D}\models\varkappa(0)$ iff
${\mathcal{I}}_{\mathcal{O},\mathcal{D}}\models\varkappa(0)$, where
${\mathcal{I}}_{\mathcal{O},\mathcal{D}}$ is the _completion_ of
$\mathcal{D}$: it contains $A(\ell)$ iff $\mathcal{O}\cup\\{B\mid
B(\ell)\in\mathcal{D}\\}\models A$. For example, if $\mathcal{O}=\\{A\vee
B\\}$ and $\mathcal{D}=\\{A(1),B(1),A(3),B(3)\\}$, the completion
${\mathcal{I}}_{\mathcal{O},\mathcal{D}}$ is just $\mathcal{D}$ regarded as an
interpretation (so ${\mathcal{I}}_{\mathcal{O},\mathcal{D}}$ does not have to
be a model of $\mathcal{O}$). It can be constructed in polytime in
$\mathcal{D}$ and, due to the equivalence above, used to prove the P upper
bounds using dynamic programming. That equivalence does not hold for
$\textsl{LTL}^{\smash{\Box\Diamond}}$, but the technique can be extended by
applying it to data sets enriched by certain types.

Note that the completion technique does not work for
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\\!\Diamond$-queries.
For example,
$\mathcal{O},\mathcal{D}\models\Diamond(A\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}B)$
for $\mathcal{D}$ and $\mathcal{O}$ defined above, and so the equivalence does
not hold. In fact, the complexity of separability by
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond$-queries remains
open.

##  7 QBE with LTL-Ontologies

For ontologies with arbitrary LTL-axioms, we obtain:

######  Theorem 14.

$(i)$ $\mathsf{QBE}(\textsl{LTL},\mathcal{Q})$ is in $2\textsc{ExpTime}{}$,
for any
$\mathcal{Q}\in\\{\,\mathcal{Q}[\Diamond],\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond],\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]\,\\}$.
$(ii)$ $\mathsf{QBE}(\textsl{LTL},\mathcal{Q})$ is in $2\textsc{ExpSpace}{}$,
for any
$\mathcal{Q}\in\\{\,\mathcal{Q}_{p}[\Diamond],\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond],\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]\,\\}$.

The proof requires a further modification of the transition systems $S^{i}$ in
Theorem 6. We illustrate it by an example. Let $\mathcal{O}=\\{A\to\Diamond
B,\,\top\to A\lor B,\,A\land B\to\bot\\}$ with the set of $\mathcal{O}$-types
$\boldsymbol{T}_{\mathcal{O}}=\\{\textit{tp}_{1},\textit{tp}_{2},\textit{tp}_{3}\\}$,
where $\textit{tp}_{1}=\\{A,\neg B,\Diamond B\\}$, $\textit{tp}_{2}=\\{\neg
A,B,\neg\Diamond B\\}$, $\textit{tp}_{3}=\\{A,\neg B,\neg\Diamond B\\}$, and
$\textit{tp}_{4}=\\{\neg A,B,\Diamond B\\}$, from which we omitted subformulas
such as $A\lor B$ that are true or false in all types. For non-empty sets
$\boldsymbol{T}_{1},\boldsymbol{T}_{2}\subseteq\boldsymbol{T}_{\mathcal{O}}$
and $\Gamma\subseteq\Sigma^{\bot}$, we take the relation
$\boldsymbol{T}_{1}\to_{\Gamma}\boldsymbol{T}_{2}$, which, intuitively, says
that if there are instants $n_{\mathcal{I}}$ in all models ${\mathcal{I}}$ of
$\mathcal{O},\mathcal{D}$ such that
$\\{\textit{tp}_{\mathcal{I}}(n_{\mathcal{I}})\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}=\boldsymbol{T}_{1}$,
then there exist $m_{\mathcal{I}}>n_{\mathcal{I}}$ with
$\\{\textit{tp}_{\mathcal{I}}(m_{\mathcal{I}})\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}=\boldsymbol{T}_{2}$
and $\Gamma=\\{A\in\Sigma^{\bot}\mid{\mathcal{I}},m\models A\text{ for all
}{\mathcal{I}}\text{ and }n_{\mathcal{I}}<m<m_{\mathcal{I}}\\}$. In our
example, we have
$\\{\textit{tp}_{1},\textit{tp}_{3}\\}\to_{\Sigma^{\bot}}\\{\textit{tp}_{1},\textit{tp}_{2},\textit{tp}_{3},\textit{tp}_{4}\\}$
and
$\\{\textit{tp}_{1},\textit{tp}_{3}\\}\to_{\\{B\\}}\\{\textit{tp}_{1},\textit{tp}_{3},\textit{tp}_{4}\\}$
(among others). Then we construct the following transition system $S^{i}$ for,
say, $\mathcal{D}_{i}=\\{A(0)\\}$, which reflects all
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-queries over
$\mathcal{O},\mathcal{D}_{i}$ using
$\boldsymbol{T}^{\prime}\subseteq\boldsymbol{T}_{\mathcal{O}}$ as states (the
initial state is $\\{\textit{tp}_{1},\textit{tp}_{3}\\}$ since
$A(0)\in\mathcal{D}_{i}$):

$\\{t_{1},t_{3}\\}$$A$$\\{t_{1},t_{3},t_{4}\\}$$\emptyset$$\\{t_{1},t_{2},t_{3},t_{4}\\}$$\emptyset$$B$$B$

The $S^{i}$ can be constructed in $2\textsc{ExpTime}{}$ in
$|\mathcal{D}_{i}|+|\mathcal{O}|$ (checking
$\boldsymbol{T}_{1}\to_{\Gamma}\boldsymbol{T}_{2}$, for given
$\boldsymbol{T}_{1}$, $\boldsymbol{T}_{2}$ and $\Gamma$, can be done in
ExpSpace). Also, the product of the $S^{i}$, for $\mathcal{D}_{i}\in E^{+}$,
can be constructed in $2\textsc{ExpTime}{}$ in $|\mathcal{D}_{i}|+|E^{+}|$.

##  8 Conclusions

We have started an investigation of the computational complexity of query-by-
example for principal classes of LTL-queries, both with and without mediating
ontologies. Our results are encouraging as we exhibit important cases that are
tractable for data complexity and not harder than satisfiability for combined
complexity. Many interesting and technically challenging problems remain open.
Especially intriguing are queries with $\mathbin{\mathsf{U}}$. For example, we
still need to pinpoint the size of minimal separating
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$\- and
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-queries under a Horn ontology. The
tight complexity of QBE for unrestricted $\mathbin{\mathsf{U}}$-queries is
also open. In general, such queries could be too perplexing for applications;
however, they can express useful disjunctive patterns such as ‘in at most $n$
moments of time’. Note also that sparse data instances with large gaps
between timestamps may require binary representations thereof, for which the
proofs of some of our results do not go through.

Our results and techniques provide a good starting point for studying QBE with
(ontology-mediated) queries over temporal databases with a full relational
component Chomicki et al. (2001); Chomicki and Toman (2018); Artale et al.
(2022) and also for the construction of separating queries satisfying
additional conditions such as being a longest/shortest separator Blum et al.
(2021); Fijalkow and Lagarde (2021) or a most specific/general one ten Cate et
al. (2022).

## Acknowledgements

This work was supported by EPSRC UK grants EP/S032207, EP/S032282, and
EP/W025868.

## References

  * Arenas et al. [2016] M. Arenas, G. I. Diaz, and E. Kostylev.  Reverse engineering SPARQL queries.  In Proc. of WWW, pages 239–249, 2016.
  * Artale et al. [2021] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Zakharyaschev.  First-order rewritability of ontology-mediated queries in linear temporal logic.  Artif. Intell., 299:103536, 2021.
  * Artale et al. [2022] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, and M. Zakharyaschev.  First-order rewritability and complexity of two-dimensional temporal ontology-mediated queries.  J. Artif. Intell. Res., 75:1223–1291, 2022.
  * Badea and Nienhuys-Cheng [2000] L. Badea and S. Nienhuys-Cheng.  A refinement operator for description logics.  In Proc. of ILP, pages 40–59, 2000.
  * Barceló and Romero [2017] P. Barceló and M. Romero.  The complexity of reverse engineering problems for conjunctive queries.  In Proc. of ICDT, pages 7:1–7:17, 2017.
  * Bergroth et al. [2000] L. Bergroth, H. Hakonen, and T. Raita.  A survey of longest common subsequence algorithms.  In Proc. of SPIRE, pages 39–48, 2000.
  * Blum et al. [2021] C. Blum, M. Djukanovic, A. Santini, H. Jiang, C. Li, F. Manyà, and G. Raidl.  Solving longest common subsequence problems via a transformation to the maximum clique problem.  Comput. Oper. Res., 125:105089, 2021.
  * Bühmann et al. [2016] L. Bühmann, J. Lehmann, and P. Westphal.  DL-learner - A framework for inductive learning on the semantic web.  J. Web Sem., 39:15–24, 2016.
  * Camacho and McIlraith [2019] A. Camacho and S. McIlraith.  Learning interpretable models expressed in linear temporal logic.  In Proc. of ICAPS, pages 621–630, 2019.
  * Chen and Lin [1994] C.-C. Chen and I-Peng Lin.  The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics.  Theor. Comp. Sci., 129(1):95–121, 1994.
  * Chomicki and Toman [2018] J. Chomicki and D. Toman.  Temporal logic in database query languages.  In Encyclopedia of Database Systems. Springer, 2018.
  * Chomicki et al. [2001] J. Chomicki, D. Toman, and M. Böhlen.  Querying ATSQL databases with temporal logic.  ACM Trans. Database Syst., 26(2):145–178, 2001.
  * Chowdhury et al. [2010] R. Chowdhury, H.-S. Le, and V. Ramachandran.  Cache-oblivious dynamic programming for bioinformatics.  IEEE/ACM Transactions on Computational Biology and Bioinformatics, 7(3):495–510, 2010.
  * Cima et al. [2021] G. Cima, F. Croce, and M. Lenzerini.  Query definability and its approximations in ontology-based data management.  In Proc. of CIKM, pages 271–280. ACM, 2021.
  * Cohen and Weiss [2016] S. Cohen and Y. Weiss.  The complexity of learning tree patterns from example graphs.  ACM Trans. Database Syst., 41(2):14:1–14:44, 2016.
  * Demri et al. [2016] S. Demri, V. Goranko, and M. Lange.  Temporal Logics in Computer Science.  Cambridge University Press, 2016.
  * Deutch and Gilad [2019] D. Deutch and A. Gilad.  Reverse-engineering conjunctive queries from provenance examples.  In Proc. of EDBT, pages 277–288, 2019.
  * Fanizzi et al. [2018] N. Fanizzi, G. Rizzo, C. d’Amato, and F. Esposito.  DLFoil: Class expression learning revisited.  In Proc. of EKAW, pages 98–113, 2018.
  * Fijalkow and Lagarde [2021] N. Fijalkow and G. Lagarde.  The complexity of learning linear temporal formulas from examples.  In Proc. of 15th Int. Conf. on Grammatical Inference, volume 153 of PMLR, pages 237–250, 2021.
  * Fortin et al. [2022] M. Fortin, B. Konev, V. Ryzhikov, Y. Savateev, F. Wolter, and M. Zakharyaschev.  Unique characterisability and learnability of temporal instance queries.  In Proc. of KR, 2022.
  * Fraser [1996] C. Fraser.  Consistent subsequences and supersequences.  Theor. Comput. Sci., 165(2):233–246, 1996.
  * Funk et al. [2019] M. Funk, J. C. Jung, C. Lutz, H. Pulcini, and F. Wolter.  Learning description logic concepts: When can positive and negative examples be separated?  In Proc. of IJCAI, pages 1682–1688, 2019.
  * Gabbay et al. [2003] D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev.  Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic.  Elsevier, 2003.
  * Gutiérrez-Basulto et al. [2018] V. Gutiérrez-Basulto, J. Ch. Jung, and L. Sabellek.  Reverse engineering queries in ontology-enriched systems: The case of expressive Horn description logic ontologies.  In Proc. of IJCAI, 2018.
  * Heindorf et al. [2022] S. Heindorf, L. Blübaum, N. Düsterhus, T. Werner, V. N. Golani, C. Demir, and A.-C. Ngonga Ngomo.  Evolearner: Learning description logics with evolutionary algorithms.  In Proc. of WWW, pages 818–828. ACM, 2022.
  * Hofman and Martens [2015] P. Hofman and W. Martens.  Separability by short subsequences and subwords.  In Proc. of ICDT, volume 31 of LIPIcs, pages 230–246, 2015.
  * Iannone et al. [2007] L. Iannone, I. Palmisano, and N. Fanizzi.  An algorithm based on counterfactuals for concept learning in the Semantic Web.  Appl. Intell., 26(2):139–159, 2007.
  * Jung et al. [2020] J. Ch. Jung, C. Lutz, and F. Wolter.  Least General Generalizations in Description Logic: Verification and Existence.  In Proc. of AAAI, 2020.
  * Jung et al. [2021] J. Ch. Jung, C. Lutz, H. Pulcini, and F. Wolter.  Separating data examples by description logic concepts with restricted signatures.  In Proc. of KR, 2021.
  * Jung et al. [2022] J. Ch. Jung, C. Lutz, H. Pulcini, and F. Wolter.  Logical separability of labeled data examples under ontologies.  Artif. Intell., 313 (2022).
  * Kalashnikov et al. [2018] D. Kalashnikov, L. Lakshmanan, and D. Srivastava.  Fastqre: Fast query reverse engineering.  In Proc. of SIGMOD, pages 337–350, 2018.
  * Kupferman and Vardi [1996] O. Kupferman and M. Vardi.  Verification of fair transisiton systems.  In Proc. of CAV, volume 1102 of LNCS, pages 372–382. Springer, 1996.
  * Kurtonina and de Rijke [1997] N. Kurtonina and M. de Rijke.  Bisimulations for temporal logic.  J. Log. Lang. Inf., 6(4):403–425, 1997.
  * Lehmann and Haase [2009] J. Lehmann and Ch. Haase.  Ideal downward refinement in the $\mathcal{EL}$ description logic.  In Proc. of ILP, pages 73–87, 2009.
  * Lehmann and Hitzler [2010] J. Lehmann and P. Hitzler.  Concept learning in description logics using refinement operators.  Machine Learning, 78:203–250, 2010.
  * Lemieux et al. [2015] C. Lemieux, D. Park, and I. Beschastnikh.  General LTL specification mining (T).  In Proc. of ASE, pages 81–92. IEEE, 2015.
  * Lisi and Straccia [2015] F. Lisi and U. Straccia.  Learning in description logics with fuzzy concrete domains.  Fundamenta Informaticae, 140(3-4):373–391, 2015.
  * Lisi [2012] F. Lisi.  A formal characterization of concept learning in description logics.  In Proc. of DL, 2012.
  * Maier [1978] D. Maier.  The complexity of some problems on subsequences and supersequences.  J. ACM, 25(2):322–336, 1978.
  * Martins [2019] D. Martins.  Reverse engineering database queries from examples: State-of-the-art, challenges, and research opportunities.  Inf. Syst., 83:89–100, 2019.
  * Neider and Gavran [2018] D. Neider and I. Gavran.  Learning linear temporal properties.  In Proc. of FMCAD, pages 1–10. IEEE, 2018.
  * Ono and Nakamura [1980] H. Ono and A. Nakamura.  On the size of refutation Kripke models for some linear modal and tense logics.  Studia Logica, pages 325–333, 1980.
  * Ortiz [2019] M. Ortiz.  Ontology-mediated queries from examples: a glimpse at the DL-Lite case.  In Proc. of GCAI, pages 1–14, 2019.
  * Place and Zeitoun [2016] T. Place and M. Zeitoun.  Separating regular languages with first-order logic.  Log. Methods Comput. Sci., 12(1), 2016.
  * Place and Zeitoun [2022] T. Place and M. Zeitoun.  A generic polynomial time approach to separation by first-order logic without quantifier alternation.  In Proc. of FSTTCS, volume 250 of LIPIcs, pages 43:1–43:22, 2022.
  * Prior [1956] A. Prior.  Time and Modality.  OUP, 1956.
  * Raha et al. [2022] R. Raha, R. Roy, N. Fijalkow, and D. Neider.  Scalable anytime algorithms for learning fragments of linear temporal logic.  In Proc. of TACAS, volume 13243 of LNCS, pages 263–280. Springer, 2022.
  * Rizzo et al. [2018] G. Rizzo, N. Fanizzi, C. d’Amato, and F. Esposito.  A framework for tackling myopia in concept learning on the web of data.  In Proc. of EKAW, pages 338–354. Springer, 2018.
  * Rizzo et al. [2020] G. Rizzo, N. Fanizzi, and C. d’Amato.  Class expression induction as concept space exploration: From DL-FOIL to DL-FOCL.  Future Gener. Comput. Syst., 108:256–272, 2020.
  * Ryzhikov et al. [2021] V. Ryzhikov, Y. Savateev, and M. Zakharyaschev.  Deciding FO-rewritability of ontology-mediated queries in linear temporal logic.  In Proc. of TIME, volume 206 of LIPIcs, pages 10:1–10:15, 2021.
  * Sarker and Hitzler [2019] Md. K. Sarker and P. Hitzler.  Efficient concept induction for description logics.  In Proc. of AAAI, pages 3036–3043, 2019.
  * Schaerf [1993] A. Schaerf.  On the complexity of the instance checking problem in concept languages with existential quantification.  J. Intel. Inf. Sys., 2:265–278, 1993.
  * Sipser [1997] M. Sipser.  Introduction to the theory of computation.  PWS Publishing Company, 1997.
  * Staworko and Wieczorek [2012] S. Staworko and P. Wieczorek.  Learning twig and path queries.  In Proc. of ICDT, pages 140–154, 2012.
  * Straccia and Mucci [2015] U. Straccia and M. Mucci.  pFOIL-DL: Learning (fuzzy) $\mathcal{EL}$ concept descriptions from crisp OWL data using a probabilistic ensemble estimation.  In Proc. of SAC, pages 345–352, 2015.
  * ten Cate and Dalmau [2015] B. ten Cate and V. Dalmau.  The product homomorphism problem and applications.  In Proc. of ICDT, pages 161–176, 2015.
  * ten Cate et al. [2022] B. ten Cate, V. Dalmau, M. Funk, and C. Lutz.  Extremal fitting problems for conjunctive queries.  CoRR, abs/2206.05080, 2022.
  * Tran et al. [2017] An C. Tran, J. Dietrich, H. W. Guesgen, and S. Marsland.  Parallel symmetric class expression learning.  J. Mach. Learn. Res., 18:64:1–64:34, 2017.
  * Vardi [2007] M. Vardi.  Automata-theoretic techniques for temporal reasoning.  In Handbook of Modal Logic, pages 971–989. North-Holland, 2007.
  * Weiss and Cohen [2017] Y. Weiss and S. Cohen.  Reverse engineering SPJ-queries from examples.  In Proc. of PODS, pages 151–166, 2017.
  * Willard [2010] R. Willard.  Testing expressibility is hard.  In Proc. of CP, vol. 6308 of LNCS, pp. 9–23. Springer, 2010.
  * Zhang et al. [2013] M. Zhang, H. Elmeleegy, C. Procopiuc, and D. Srivastava.  Reverse engineering complex join queries.  In Proc. of SIGMOD, pages 809–820, 2013.
  * Zloof [1977] M. Zloof.  Query-by-example: A data base language.  IBM Syst. J., 16(4):324–343, 1977.

Appendix: Proofs

##  Appendix A Proofs for Section 3

Theorem 4. The following polynomial-time reductions hold:

(_i_.1)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q})\leq_{p}\mathsf{QBE}_{1\text{--}}(\mathcal{L},\mathcal{Q})$,
for any $\mathcal{Q}$ closed under $\land$, and any $\mathcal{L}$ (including
$\mathcal{L}=\emptyset$),

(_i_.2)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q})\leq_{p}\mathsf{QBE}^{2\text{+}}(\mathcal{L},\mathcal{Q})$,
for $\mathcal{L}\in\\{\textsl{LTL},\textsl{LTL}^{\smash{\Box\Diamond}}\\}$,

(_i_.3)

$\mathsf{QBE}(\mathcal{L},\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{L},\mathcal{Q}_{p}^{\circ}[\Diamond]))$
and
$\mathsf{QBE}(\mathcal{L},\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{L},\mathcal{Q}_{p}[\Diamond])$,
for any $\mathcal{L}$,

(_ii_.1)

$\mathsf{QBE}(\mathcal{Q}_{p}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
and
$\mathsf{QBE}(\mathcal{Q}_{p}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])\leq_{p}\mathsf{QBE}_{1\text{--}}(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$

(_ii_.2)

$\mathsf{QBE}(\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])=_{p}\mathsf{QBE}(\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$.

Reductions $(i.1)$–$(i.3)$ work for combined complexity and $(i.1)$ and
$(i.3)$ also work for data complexity. The reductions preserve boundedness of
the number of positive/negative example.

###### Proof.

(_i_.1) Observe that if $\mathcal{Q}$ is closed under $\land$,
$E=(E^{+},E^{-})$ and
$E^{-}=\\{\mathcal{D}_{1}^{-},\dots,\mathcal{D}_{n}^{-}\\}$, then $E$ is
$\mathcal{Q}$-separable under $\mathcal{O}$ iff each
$(E^{+},\\{\mathcal{D}_{i}^{-}\\})$, $1\leq i\leq n$, is. Indeed, if
$\varkappa_{i}$ separates $(E^{+},\\{\mathcal{D}_{i}^{-}\\})$, then
$\varkappa_{1}\land\dots\land\varkappa_{n}$ separates $E$. For such
$\mathcal{Q}$, we can thus assume that $E^{-}$ consists of a single data
instance. Note that
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
and $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$ are not closed under $\land$.

(_i_.2) Let $E^{+}=\\{\mathcal{D}_{1},\dots,\mathcal{D}_{n}\\}$ and let
$k=\max_{i}\max\mathcal{D}_{i}$. We construct an ontology
$\mathcal{O}^{\prime}$ by taking the fresh atoms $A_{1},\ldots,A_{n}$,
$C_{0},\ldots,C_{k}$, $D_{0},\ldots,D_{k}$, $S_{1},S_{2}$ and adding the
following axioms to the given ontology $\mathcal{O}$:

$\displaystyle S_{1}\to A_{1}\lor\dots\lor A_{n},\quad S_{2}\to
A_{1}\lor\dots\lor A_{n},$ $\displaystyle C_{i}\land\Diamond A_{j}\to X,\quad
D_{i}\land\Diamond A_{j}\to X,\ \ \text{for $X(i)\in\mathcal{D}_{j}$.}$

Let $E^{\prime+}$ consist of
$\mathcal{D}^{\prime}_{1}=\\{C_{0}(0),\dots,C_{k}(n^{\prime}),S_{1}(n^{\prime}+1)\\}$
and
$\mathcal{D}^{\prime}_{2}=\\{D_{0}(0),\dots,D_{k}(n^{\prime}),S_{2}(n^{\prime}+1)\\}$.
Then every model of $\mathcal{O}^{\prime},\mathcal{D}^{\prime}_{1}$ or
$\mathcal{O}^{\prime},\mathcal{D}^{\prime}_{2}$ contains a model of at least
one of the $\mathcal{O},\mathcal{D}_{i}$ and, conversely, every model of any
$\mathcal{O},\mathcal{D}_{i}$ can be converted into a model of
$\mathcal{O}^{\prime},\mathcal{D}_{1}^{\prime}$ or
$\mathcal{O}^{\prime},\mathcal{D}_{2}^{\prime}$ by adding only the newly
introduced symbols. So, if there is a separating query for $(E^{+},E^{-})$
under the ontology $\mathcal{O}$, then the same query separates
$(E^{\prime+},E^{-})$ under the ontology $\mathcal{O}^{\prime}$. And if there
is a separating query for $(E^{\prime+},E^{-})$ under the ontology
$\mathcal{O}^{\prime}$, then it cannot contain any symbols from
$\mathsf{sig}(\mathcal{O}^{\prime})\setminus\mathsf{sig}(\mathcal{O})$, and so
it separates $(E^{+},E^{-})$ under the ontology $\mathcal{O}$.

(_i_.3) Recall from the main part of the paper that
$[\rho_{0}\wedge\Diamond(\rho_{1}\wedge\bigwedge_{i}\Diamond\varkappa_{i})]\equiv[\rho_{0}\wedge\bigwedge_{i}\Diamond(\rho_{1}\wedge\Diamond\varkappa_{i})]$,
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond\varkappa\equiv\Diamond{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa$
and
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}(\varkappa\land\varkappa^{\prime})\equiv({\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa\land{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\varkappa^{\prime})$,
and so each
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$-query
can be equivalently transformed in polynomial time into a conjunction of
$\mathcal{Q}_{p}^{\circ}[\Diamond]$-queries. If $E^{-}$ is a singleton, then a
conjunction of queries in $\mathcal{Q}_{p}^{\circ}[\Diamond]$ separates
$(E^{+},E^{-})$ under an ontology $\mathcal{O}$ iff a single conjunct
separates $(E^{+},E^{-})$ under $\mathcal{O}$. Thus, there is
$\boldsymbol{q}\in\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
separating an arbitrary $(E^{+},E^{-})$ under $\mathcal{O}$ iff there are
polysize $\boldsymbol{q}_{\mathcal{D}}\in\mathcal{Q}_{p}^{\circ}[\Diamond]$
separating $(E^{+},\\{\mathcal{D}\\})$ under $\mathcal{O}$, for each
$\mathcal{D}\in E^{-}$. The second reduction is obtained by dropping
$\bigcirc$ from the argument above.

In (_ii_.1), the first two reductions are proved by adding to
$E^{+}\ni\mathcal{D}$, for some $\mathcal{D}$, the data instance
$\mathcal{D}^{\prime}=\\{A(mn)\mid A(n)\in\mathcal{D}\\}$ with
$m=\max\mathcal{D}+2$. Now, if $\mathcal{D}\models\varkappa(0)$ and
$\mathcal{D}^{\prime}\models\varkappa(0)$, for
$\varkappa\in\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$, then $\varkappa$ is
equivalent to a $\mathcal{Q}_{p}[\Diamond]$-query.

For the third reduction, we observe first that without loss of generality one
can assume that the positive examples do not contain atoms of the form $X(0)$.
Indeed, suppose $E=(E^{+},E^{-})$,
$E^{+}=\\{\mathcal{D}^{+}_{1},\ldots,\mathcal{D}^{+}_{n}\\}$, and
$E^{-}=\\{\mathcal{D}^{-}_{1},\dots,\mathcal{D}^{-}_{k}\\}$. Let
$\rho=\bigcap_{i=1}^{n}\\{X\mid X(0)\in\mathcal{D}^{+}_{i}\\}$,
$E^{\prime-}=\\{\mathcal{D}\in E^{-}\mid\mathcal{D}\not\models\rho\\}$, and
let $D=(D^{+},D^{-})$, where $D^{+}=\\{\mathcal{D}\setminus\\{X(0)\mid
X\in\mathsf{sig}(E)\\}\mid\mathcal{D}\in E^{+}\\}$ and
$D^{-}=\\{\mathcal{D}\setminus\\{X(0)\mid
X\in\mathsf{sig}(E)\\}\mid\mathcal{D}\in E^{\prime-}\\}$. If
$\varphi=\rho_{0}\land\lambda_{1}\mathbin{\mathsf{U}}(\rho_{1}\land\lambda_{2}\mathbin{\mathsf{U}}(\dots(\rho_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots))$
separates $E$ then $\varphi^{\prime}$, which is $\varphi$ with $\rho_{0}$
replaced by $\emptyset$, separates $D$. If
$\psi=\rho_{0}\land\lambda_{1}\mathbin{\mathsf{U}}(\rho_{1}\land\lambda_{2}\mathbin{\mathsf{U}}(\dots(\rho_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots))$
separates $D$, then $\rho_{0}=\emptyset$ and $\psi^{\prime}$, which is $\psi$
with $\rho_{0}$ replaced by $\rho$, separates $E$.

Now, suppose $E=(E^{+},E^{-})$,
$E^{+}=\\{\mathcal{D}^{+}_{1},\ldots,\mathcal{D}^{+}_{n}\\}$, $n>1$, and
$E^{-}=\\{\mathcal{D}^{-}_{1},\dots,\mathcal{D}^{-}_{k}\\}$, and
$X(0)\notin\mathcal{D}_{i}^{+}$, for any $X$ and $i$. Let $B,C$ be fresh atoms
and $m=\max_{\mathcal{D}\in E^{+}\cup E^{-}}(\max(\mathcal{D}))+2$. We set
$E^{\prime+}=\\{\mathcal{D}^{\prime\prime+}_{1},\mathcal{D}_{2}^{\prime+},\dots,\mathcal{D}^{\prime+}_{n}\\}$,
where

$\displaystyle\mathcal{D}_{i}^{\prime+}=\\{X(j+m)\mid
X(j)\in\mathcal{D}^{+}_{i}\\}\cup\\{B(m)\\}\cup\\{C(j)\mid
m<j<m+\max(\mathcal{D}_{i}^{+})\\},$
$\displaystyle\mathcal{D}_{1}^{\prime\prime+}=\\{X(j+1)\mid
X(j)\in\mathcal{D}^{+}_{1}\\}\cup\\{B(1)\\}\cup\\{C(j)\mid
1<j<1+\max(\mathcal{D}_{1}^{+})\\}.$

We also set $E^{\prime-}=\\{\mathcal{D}^{\prime-}\\}$ with

$\mathcal{D}^{\prime-}=\\{X((2i-1)m+j)\mid
X(j)\in\mathcal{D}_{i}^{-},i\in[1,k]\\}\cup\\{B((2i-1)m)\mid
i\in[1,k]\\}\cup\\{C(i)\mid(2i-1)m<i<2im,i\in[1,k]\\}.$

See the picture below for an illustration.

$\mathcal{D}^{\prime\prime+}_{1}$$\mathcal{D}_{1}^{+}$$0$$B$$1$$C$$2$$\ldots$$C$
$\mathcal{D}^{\prime+}_{i}$$\mathcal{D}_{i}^{+}$$0$$1$$B$$m$$C$$\ldots$$C$

$\mathcal{D}^{\prime-}$$\mathcal{D}_{1}^{-}$$\mathcal{D}^{-}_{k}$$0$$1$$B$$m$$C$$C$$2m$$B$$(2k\\!-\\!\\!1)m$$C$$C$$2km$

Let $E=(E^{\prime+},E^{\prime-})$. We prove equiseparability of $E$ and
$E^{\prime}$.

($\Rightarrow$) Suppose
$\varphi=\rho_{0}\land\lambda_{1}\mathbin{\mathsf{U}}(\rho_{1}\land\lambda_{2}\mathbin{\mathsf{U}}(\dots(\rho_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots))$
with $l<m$ separates $E$. Then $\rho_{0}=\top$ (since
$X(0)\notin\mathcal{D}_{i}^{+}$, for any $X$). Consider the query
$\Diamond\varphi^{\prime}$, where $\varphi^{\prime}$ is $\varphi$ in which
$\rho_{0}$ is replaced by $B$ and $\lambda_{i}\neq\bot$ are replaced with
$\lambda_{i}\land C$. Since $\mathcal{D}^{+}_{j}\models\varphi$ we have
$\mathcal{D}\models\varphi^{\prime}$ for all $\mathcal{D}\in E^{\prime+}$. If
$\mathcal{D}^{\prime-}\models\Diamond\varphi^{\prime}$, then
$\mathcal{D}^{\prime-}\models\varphi^{\prime}((2j-1)m)$ for some $j$. Since
all $\lambda^{\prime}$s contain $C$ and $l<m$, we have
$\mathcal{D}^{-}_{j}\models\varphi$, which is impossible. Therefore,
$\Diamond\varphi^{\prime}$ separates $E^{\prime}$.

($\Leftarrow$) Suppose that
$\psi=\rho_{0}\land\lambda_{1}\mathbin{\mathsf{U}}(\rho_{1}\land\lambda_{2}\mathbin{\mathsf{U}}(\dots(\rho_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots))$
with $\rho_{l}\neq\top$ separates $E^{\prime}$. Since
$\mathcal{D}^{\prime\prime+}_{1}\models\psi$, we have $l<m$. Find the smallest
$i$ such that $\rho_{i}\neq\top$. As $\mathcal{D}^{\prime+}_{2}\models\psi$,
there is $i^{\prime}\leq i$ with $\lambda_{i^{\prime}}=\top$.

If $B\in\rho_{i}$ then, since $\mathcal{D}^{\prime\prime+}_{1}\models\psi$, we
have $i=1$ and $\lambda_{1}=\top$. Let
$\psi^{\prime}=\lambda^{\prime}_{2}\mathbin{\mathsf{U}}(\rho^{\prime}_{2}\land\lambda^{\prime}_{3}\mathbin{\mathsf{U}}(\dots(\rho^{\prime}_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots))$
where $\rho^{\prime}_{j}=\rho_{j}\setminus\\{C\\}$ and
$\lambda^{\prime}_{j}=\lambda_{j}\setminus\\{C\\}$. We see that in this case
$\mathcal{D}^{\prime+}_{j}\models\psi^{\prime}(m)$, and so
$\mathcal{D}^{+}_{j}\models\psi^{\prime}$ for all $j$. Also since
$\mathcal{D}^{\prime-}\not\models\psi$, we have
$\mathcal{D}^{-}_{j}\not\models\psi^{\prime}$, and so $\psi^{\prime}$
separates $E$.

If $B\notin\rho_{i}$, let
$\psi^{\prime}=\Diamond(\rho_{i}\land\lambda_{i+1}\mathbin{\mathsf{U}}(\rho_{i+1}\land\lambda_{i+2}\mathbin{\mathsf{U}}(\dots(\rho_{l-1}\land(\lambda_{l}\mathbin{\mathsf{U}}\rho_{l}))\dots)))$.
Then $\mathcal{D}^{+}\models\psi^{\prime}$ for all $\mathcal{D}^{+}\in
E^{\prime+}$. If $\mathcal{D}^{\prime-}\models\psi^{\prime}$, then we have
$\mathcal{D}^{\prime-}\models\psi$ as $\lambda_{i^{\prime}}=\top$, and so
$\psi^{\prime}$ also separates $E^{\prime}$. Consider the instance
$\mathcal{D}_{l}^{\prime-}$ (corresponding to some $\mathcal{D}^{-}_{l}$)
shown below:

$\mathcal{D}_{l}^{\prime-}=\\{X((2l-1)m+j)\mid
X(j)\in\mathcal{D}_{l}^{-}\\}\cup\\{B((2l-1)m)\\}\cup\\{C(j)\mid(2l-1)m<j<2lm\\}.$

$\mathcal{D}_{k}^{\prime-}$$\mathcal{D}_{l}^{-}$$0$$1$$B$$(2l-1)m$$C$$C$$2lm$

Since $\mathcal{D}_{l}^{\prime-}\subseteq\mathcal{D}^{\prime-}$, we have
$\mathcal{D}_{l}^{\prime-}\not\models\psi^{\prime}$, and so
$\mathcal{D}_{l}^{-}\not\models\psi^{\prime\prime}$, where
$\psi^{\prime\prime}$ is $\psi^{\prime}$ with the $\rho_{j}$ replaced by
$\rho_{j}\setminus\\{C\\}$ and $\lambda_{j}$ replaced by
$\lambda_{j}\setminus\\{B,C\\}$, for $\lambda_{j}\neq\emptyset$. Clearly,
$\mathcal{D}^{+}\models\psi^{\prime\prime}$ for all $\mathcal{D}^{+}\in
E^{+}$, and so $\psi^{\prime\prime}$ separates $E$.

$(ii.2)$ To show
$\mathsf{QBE}(\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}[\Diamond])$,
suppose that $E=(E^{+},E^{-})$ is given. Let $m$ be the maximum over all
$\max\mathcal{D}$ with $\mathcal{D}\in E^{+}$. Introduce, for every $A$ such
that $A(\ell)\in\mathcal{D}$ for some $\mathcal{D}\in E^{+}$, a fresh atom
$A_{k}$, $0<k\leq m$, and extend any $\mathcal{D}\in E^{+}\cup E^{-}$ to a
data instance $\mathcal{D}^{\prime}$ by adding $A_{k}(\ell)$ to $\mathcal{D}$
if $A(k+\ell)\in\mathcal{D}$. Let
$F^{+}=\\{\mathcal{D}^{\prime}\mid\mathcal{D}\in E^{+}\\}$ and
$F^{-}=\\{\mathcal{D}^{\prime}\mid\mathcal{D}\in E^{-}\\}$. Then clearly $E$
is
$\mathcal{Q}[\Diamond{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}]$-separable
iff $F$ is $\mathcal{Q}[\Diamond]$-separable.

The converse reduction and
$\mathsf{QBE}(\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}(\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$
are proved similarly to (_ii_.1). ∎

##  Appendix B Proofs for Section 4

We show the complexity results in Table 1. To this end, we first introduce
some notation for sequence problems. Let $\Sigma$ be an alphabet of symbols. A
_word over $\Sigma$_ is a finite sequence of symbols from $\Sigma$. A word
$\alpha$ is a _subsequence_ of a word $\beta$ if $\alpha$ can be obtained from
$\beta$ by removing zero or more symbols anywhere in $\beta$. For a set $S$ of
words, we call a word $\alpha$ a _common subsequence of $S$_ if it is a
subsequence of every word in $S$. The _consistent subsequence problem (CSSP)_
is formulated as follows:

Given:

sets $S^{+}$ and $S^{-}$ of words over an alphabet $\Sigma$.

Problem:

decide whether there exists a common subsequence of $S^{+}$ that is a not
subsequence of any word in $S^{-}$.

The following is shown in Fraser [1996]:

######  Theorem 15.

$(i)$ CSSP is NP-hard even if both the alphabet and $S^{+}$ have cardinality
two.

$(ii)$ CSSP is NP-hard even if $S^{-}$ is a singleton.

Another problem of interest for us is the following _common subsequence
problem (KsubS)_ :

Given:

a set $S$ of words over an alphabet $\Sigma$ and a number $k$.

Problem:

decide whether there exists a common subsequence of $S$ of length at least
$k$.

The following is shown in Maier [1978]:

######  Theorem 16.

KsubS is NP-hard even if the alphabet has cardinality $2$.

We are now in a position to prove the results for
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\Diamond$-queries in
Table 1. We start by proving the NP-lower bounds for
$\mathcal{Q}_{p}[\Diamond]$. We actually show a slightly stronger result than
in the table.

######  Lemma 17.

QBE$(\mathcal{Q}_{p}[\Diamond])$ with two positive examples or a single
negative example is NP-hard.

###### Proof.

The proof by polynomial-time reduction of CSSP (as formulated in Theorem 15)
is trivial. It is also of interest to give a proof of the second claim (a
single negative example) via a polynomial-time reduction of KsubS. The proof
also works directly for $\mathcal{Q}_{p}^{\circ}[\Diamond]$-queries. Suppose
that an instance $S,k$ of KsubS over alphabet $\\{A,B\\}$ is given. We define
$E$ of the form $(E^{+},\\{\mathcal{D}^{-}\\})$ such that the following
conditions are equivalent:

  * •

there exists a common subsequence of $S$ of length $k$;

  * •

there exists $\boldsymbol{q}\in\mathcal{Q}_{p}[\Diamond]$ that separates
$(E^{+},\\{\mathcal{D}^{-}\\})$;

  * •

there exists $\boldsymbol{q}\in\mathcal{Q}_{p}^{\circ}[\Diamond]$ that
separates $(E^{+},\\{\mathcal{D}^{-}\\})$.

We represent each word $w\in S$ as a data instance $\mathcal{D}_{w}$ starting
at time point $1$ (for example, the word $w=ABBA$ is represented as
$\mathcal{D}_{w}=\\{A(1),B(2),B(3),A(4)\\}$). Now let

$\mathcal{D}^{+}=\\{A(i(k+2)),B(i(k+2))\mid 1\leq i\leq k\\}$

and

$\mathcal{D}^{-}=\mathcal{D}^{+}\setminus\\{A(k(k+2)),B(k(k+2))\\}$

and let $E^{+}=\\{\mathcal{D}_{w}\mid w\in S\\}\cup\\{\mathcal{D}^{+}\\}$.
Assume first that there exists a common subsequence $C_{1}\cdots C_{k}$ of $S$
of length $k$. Then
$\Diamond(C_{1}\wedge\Diamond(C_{2}\wedge\cdots\wedge\Diamond C_{k}))$
separates $(E^{+},\\{\mathcal{D}^{-}\\})$. Now assume that a query

$\displaystyle\varkappa$
$\displaystyle=\rho_{0}\land\Diamond(\rho_{1}\land\Diamond(\rho_{2}\land\dots\land\Diamond\rho_{n})),$

where every $\rho_{i}$ is a
$\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}]$-query,
separates $(E^{+},\\{\mathcal{D}^{-}\\})$. As
$\mathcal{D}_{w}\models\varkappa(0)$ for some $w\in S$, we have that $n\leq k$
and all $\rho_{i}$ have depth bounded by $k$. Then $\rho_{0}=\top$ and also,
as there are ‘gaps’ of length $k+1$ between any two entries in
$\mathcal{D}^{+}$ and since $\mathcal{D}^{+}\models\varkappa(0)$ we may assume
that each $\rho_{i}$, $i>0$, is of the form
${\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}^{m_{i}}\rho_{i}^{\prime}$
with $0\leq m_{i}\leq k$ and $\rho_{i}^{\prime}$ a conjunction of atoms.
Observe that we can satisfy, in $\mathcal{D}^{+}$,

  * •

$\rho_{1}$ in the interval $\\{1,\ldots,k+2\\}$;

  * •

$\rho_{2}$ in the interval $\\{(k+1)+1,\ldots,2(k+2)\\}$;

  * •

and so on, with $\rho_{n}$ satisfied in the interval
$\\{(n-1)(k+2)+1,\ldots,n(k+2)\\}$.

In particular, if $\rho_{i}$ is a conjunction of atoms, then it can be
satisfied in $i(k+2)$. If $n<k$, then it follows directly that
$\mathcal{D}^{-}\models\varkappa(0)$, and we have derived a contradiction.
Hence $n=k$. Then, as the depth of $\varkappa$ is bounded by $k$, $\rho_{k}$
is a conjunction of atoms. In fact, one can now show by induction starting
with $\rho_{k-1}$ that all $\rho_{i}$, $i>0$, are nonempty conjunctions of
atoms. Otherwise a shift to the left shows that
$\mathcal{D}^{-}\models\varkappa(0)$ and we have derived a contradiction. Thus
$\varkappa$ takes the form
$\Diamond(\rho_{1}\land\Diamond(\rho_{2}\land\dots\land\Diamond\rho_{k}))$
with all $\rho_{i}$ non-empty. It follows from
$\mathcal{D}_{w}\models\varkappa(0)$ for all $w\in S$ that $\varkappa$ defines
a common subsequence of $S$ of length $k$, as required. ∎

The NP-lower bound for
QBE$(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
with a bounded number of positive examples or a single negative example
follows from Lemma 17 and Theorem 4 $(ii.1)$.

We next obtain the NP-lower bound for QBE$(\mathcal{Q}[\Diamond])$ with a
single negative example from Lemma 17 by observing that it follows from the
proof of the first part of Theorem 4 $(i.3)$ that any $(E^{+},E^{-})$ with
$E^{-}$ a singleton is $\mathcal{Q}_{p}[\Diamond]$-separable if, and only if,
it is $\mathcal{Q}[\Diamond]$-separable. The NP-lower bound for
QBE$(\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
with a single negative example follows from the NP-lower bound for
QBE$(\mathcal{Q}[\Diamond])$ with a single negative example using Theorem 4
$(ii.2)$.

We come to the NP-upper bounds. Recall that a query language $\mathcal{Q}$ has
the _polynomial separation property (PSP) under an ontology language
$\mathcal{L}$_ if any $\mathcal{Q}$-separable example is separated by a query
in $\mathcal{Q}$ of polynomial size. The NP-upper bounds for query languages
using $\Diamond$ (and $\bigcirc$) in Table 1 follow trivially from the
following result.

######  Lemma 18.

Let
$\mathcal{Q}\in\\{\mathcal{Q}_{p}[\Diamond],\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond],\mathcal{Q}[\Diamond],\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]\\}$.
Then $\mathcal{Q}$ has the PSP under the empty ontology.

###### Proof.

The proof for
$\mathcal{Q}\in\\{\mathcal{Q}_{p}[\Diamond],\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]\\}$
is trivial: if $\mathcal{D}\models\varkappa(0)$ for some
$\varkappa\in\mathcal{Q}$, then $\varkappa$ is clearly equivalent to a query
in $\mathcal{Q}$ whose temporal depth does not exceed the maximal timestamp in
$\mathcal{D}$, and so is of linear size in $\mathcal{D}$.

For
$\mathcal{Q}\in\\{\mathcal{Q}[\Diamond],\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]\\}$,
the argument is as follows. Assume that $\varkappa$ separates $(E^{+},E^{-})$.
We may assume that $\varkappa$ is a conjunction of at most $|E^{-}|$-many
queries in $\mathcal{Q}_{p}^{\circ}[\Diamond]$ of the form

$\displaystyle\varkappa$
$\displaystyle=\rho_{0}\land\Diamond(\rho_{1}\land\Diamond(\rho_{2}\land\dots\land\Diamond\rho_{n})),$

where every $\rho_{i}$ is a query in
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}]$. Then
the conjuncts of $\varkappa$ are equivalent to queries in which $n$ does not
exceed the maximal timestamps in data instances in $E^{+}$ and each $\rho_{i}$
is a query in
$\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}]$ whose
temporal depth also does not exceed the maximal timestamps in data instances
in $E^{+}$. ∎

We next complete the description of the polynomial-time algorithm solving
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
for $E^{+}=\\{\mathcal{D}_{1}^{+},\mathcal{D}_{2}^{+}\\}$ and
$E^{-}=\\{\mathcal{D}_{1}^{-},\mathcal{D}_{2}^{-}\\}$. The extension to
arbitrary $E^{+},E^{-}$ is straightforward. Recall that we assume that
$\varkappa$ takes the form (1) with $\rho_{n}\neq\top$. Also recall that
$S_{i,j}$ is the set of tuples $(k,\ell_{1},\ell_{2},n_{1},n_{2})$ such that

  1. 1.

$\ell_{1}\leq i\leq\max\mathcal{D}_{1}^{+}$,

  2. 2.

$\ell_{2}\leq j\leq\max\mathcal{D}_{2}^{+}$,

and there is
$\varkappa=\rho_{0}\land{\boldsymbol{o}}_{1}(\rho_{1}\land\dots\land{\boldsymbol{o}}_{k}\rho_{k})$
for which

  1. 1.

there are satisfying assignments $f_{1},f_{2}$ in $\mathcal{D}_{1}^{+}$ and
$\mathcal{D}_{2}^{+}$ with $f_{1}(k)=\ell_{1}$ and $f_{2}(k)=\ell_{2}$,
respectively, and

  2. 2.

$n_{1}$ is minimal with a satisfying assignment $f$ for $\varkappa$ in
$\mathcal{D}_{1}^{-}$ such that $f(k)=n_{1}$, and $n_{1}=\infty$ if there is
no such $f$; $n_{2}$ is minimal with a satisfying assignment $f$ for
$\varkappa$ in $\mathcal{D}_{2}^{-}$ such that $f(k)=n_{2}$, and
$n_{2}=\infty$ if there is no such $f$.

Then clearly there is a
$\varkappa\in\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond]$
separating $(E^{+},E^{-})$ if there are $k,\ell_{1},\ell_{2}$ such that
$(k,\ell_{1},\ell_{2},\infty,\infty)\in
S_{\max\mathcal{D}_{1}^{+},\max\mathcal{D}_{2}^{+}}$.

So it suffices to compute
$S_{\max\mathcal{D}_{1}^{+},\max\mathcal{D}_{2}^{+}}$ in polytime
incrementally, starting with $S_{0,0}$. We have computed $S_{0,j}$ and
$S_{i,0}$ already. Recall that $t_{\mathcal{D}}(i)=\\{A\mid
A(i)\in\mathcal{D}\\}$. To obtain $S_{i+1,j+1}$, we add to $S_{i+1,j}\cup
S_{i,j+1}$ any tuple $(k,\ell_{1},\ell_{2},n_{1},n_{2})$ for which there is
$(k^{\prime},\ell_{1}^{\prime},\ell_{2}^{\prime},n_{1}^{\prime},n_{2}^{\prime})\in
S_{i+1,j}\cup S_{i,j+1}$ with $k^{\prime}<k$, $\ell_{1}^{\prime}<\ell_{1}\leq
i+1$, $\ell_{2}^{\prime}<\ell_{2}\leq j+1$ such that $\ell_{1}=i+1$ or
$\ell_{2}=j+1$ and, for $m=k-k^{\prime}+1\geq 0$, we have
$\ell_{1}-m>\ell_{1}^{\prime}$, $\ell_{2}-m>\ell_{2}^{\prime}$ and some sets
of atoms $\rho_{1},\ldots,\rho_{m}$ with

$\rho_{1}\subseteq t_{\mathcal{D}_{1}^{+}}(\ell_{1}-m)\cap
t_{\mathcal{D}_{2}^{+}}(\ell_{2}-m),\dots,\rho_{m}\subseteq
t_{\mathcal{D}_{1}^{+}}(\ell_{1})\cap t_{\mathcal{D}_{2}^{+}}(\ell_{2})$

such that

  * •

either $n_{1}$ is minimal with $n_{1}-n_{1}^{\prime}>m$ and

$\rho_{1}\subseteq t_{\mathcal{D}_{1}^{-}}(n_{1}-m),\dots,\rho_{m}\subseteq
t_{\mathcal{D}_{1}^{-}}(n_{1})$

or, if no such $n_{1}$ exists, $n_{1}=\infty$, and

  * •

either $n_{2}$ is minimal with $n_{2}-n_{2}^{\prime}>m$ and

$\rho_{1}\subseteq t_{\mathcal{D}_{2}^{-}}(n_{2}-m),\dots,\rho_{m}\subseteq
t_{\mathcal{D}_{2}^{-}}(n_{2})$

or, if no such $n_{2}$ exists, $n_{2}=\infty$.

Thus, we obtain $S_{i+1,j+1}$ from $S_{i+1,j}\cup S_{i,j+1}$ by adding any
tuple that describes a query obtained from a query $\varkappa$ described by a
tuple in $S_{i+1,j}\cup S_{i,j+1}$ by attaching the query
$\Diamond(\rho_{1}\wedge{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}(\rho_{2}\wedge\cdots\wedge{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}}\rho_{m}))$
with $m\geq 0$ to it. Clearly $S_{i+1,j+1}$ can be computed in polynomial time
from $S_{i+1,j}$ and $S_{i,j+1}$. This finishes the proof for
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}_{p}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$.

The proof for
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}_{p}[\Diamond])$
is obtained by dropping $\bigcirc$ from the proof above. The P-upper bound for
QBE$(\mathcal{Q}[\Diamond])$ with a bounded number of positive examples can be
proved in two steps: (1) by Theorem 4 $(i.1)$ it suffices to prove the P-upper
bound for
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}[\Diamond])$;
(2) by Theorem 4 $(i.3)$,
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}[\Diamond])\leq_{p}\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\mathcal{Q}_{p}[\Diamond])$.
Finally, the P-upper bound for
QBE$(\mathcal{Q}[{\raisebox{1.07639pt}{\text{\scriptsize$\bigcirc$}}},\Diamond])$
with a bounded number of positive examples follows from the P-upper bound for
QBE$(\mathcal{Q}[\Diamond])$ with a bounded number of positive examples by
Theorem 4 $(ii.2)$).

We now prove the results for query languages with $\mathbin{\mathsf{U}}$ in
Table 1. We start with the NP-lower bounds. The NP-lower bound for
QBE$(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$ with a bounded number of positive
and negative examples follows from the NP-lower bound for
QBE$(\mathcal{Q}_{p}[\Diamond])$ with a bounded number of positive examples
(shown above) and the second part of Theorem 4 $(ii.1)$ which reduces the
number of negative examples from unbounded to a singleton. The NP-lower bound
for QBE$(\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$ with a bounded number of
negative examples follows from the NP-lower bound for
QBE$(\mathcal{Q}[\Diamond])$ with a bounded number of negative examples (shown
above) and Theorem 4 $(ii.2)$. This completes the proof of the NP-lower
bounds.

The NP-upper bound for QBE$(\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$ follows
from its PSP under the empty ontology which is proved in the same way as Lemma
18:

######  Lemma 19.

$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$ has the PSP under the empty ontology.

###### Proof.

If $\mathcal{D}\models\varkappa(0)$ for some
$\varkappa\in\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$, then $\varkappa$ is
clearly equivalent to a $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-query whose
temporal depth does not exceed the maximal timestamp in $\mathcal{D}$, and so
is of linear size in $\mathcal{D}$. ∎

To obtain the P and PSpace upper bounds for queries with
$\mathbin{\mathsf{U}}$, we require the machinery and separability criterion
that will be developed in the next section.

##  Appendix C Separability Criteria for
$\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$,
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$, and
$\mathcal{Q}[\mathbin{\mathsf{U}}]$

A _transition system_ is a tuple $S=(\Sigma_{1},\Sigma_{2},W,L,R,W_{0})$,
where $\Sigma_{1}$ (respectively, $\Sigma_{2}$) is a _state_ (respectively,
_transition_) _label alphabet_ , $W$ is a set of _states_ and $W_{0}\subseteq
W$ is a set of _initial_ states. A _state labelling_ , $L$, is a map
$W\to\Sigma_{1}$; a _transition labelling_ , $R$, is a _partial_ map $W\times
W\to\Sigma_{2}$. We write $s\to_{b}s^{\prime}$, for $s,s^{\prime}\in W$, if
$R(s,s^{\prime})=b$ and we write $s\to s^{\prime}$ if $R(s,s^{\prime})$ is
defined. A _run_ or _computation_ on $S$ is a finite sequence
$\mathfrak{s}=s_{0}\to s_{1}\to\dots\to s_{n}$, for $n\geq 0$, such that
$s_{i-1}\to s_{i}$ for all $i$ and $s_{0}\in W_{0}$. A computation tree
$\mathfrak{T}_{S}$ of $S$ is (an infinite) tree—forest, to be more precise—in
which the vertices are runs $\mathfrak{s}$ on $S$ and the successor relation
is $\mathfrak{s}\to\mathfrak{s}^{\prime}$ for all
$\mathfrak{s}=s_{0}\to\dots\to s_{n}$ and
$\mathfrak{s}^{\prime}=s_{0}\to\dots\to s_{n}\to s_{n+1}$. The vertices
$\mathfrak{s}$ of the tree are labelled with $L(s_{n})$, while the edges
$\mathfrak{s}\to\mathfrak{s}^{\prime}$ are labelled with $b$ such that
$s_{n}\to_{b}s_{n+1}$. A tree $\mathfrak{T}$ is a _subtree_ of
$\mathfrak{T}_{S}$ if the set of vertices of $\mathfrak{T}$ is a _convex_
subset of the set of vertices of $\mathfrak{T}_{S}$ containing a root (from
$W_{0}$).

Let $S$ be a transition system such that $\Sigma_{1}=2^{\Sigma}$ and
$\Sigma_{2}=2^{\Sigma\cup\\{\bot\\}}$ for some signature $\Sigma$. We then say
that $S$ is a transition system _over the signature_ $\Sigma$. For a pair
$S,T$ of transition systems over $\Sigma$, we say that $S$ is _simulated by_
$T$ if every finite subtree $\mathfrak{T}^{\prime}$ of $\mathfrak{T}_{S}$ is
homomorphically embeddable into $\mathfrak{T}_{T}$, i.e., there is a map $h$
from the set of vertices of $\mathfrak{T}^{\prime}$ to the set of vertices of
$\mathfrak{T}_{T}$ such that $(i)$ $\mathfrak{s}$ is labelled by $a$ implies
$h(\mathfrak{s})$ is labelled by $a^{\prime}\supseteq a$, $(ii)$
$\mathfrak{s}\to\mathfrak{s}^{\prime}$ in $\mathfrak{T}^{\prime}$ labelled by
$b$ implies $h(\mathfrak{s})\to h(\mathfrak{s}^{\prime})$ is in
$\mathfrak{T}_{T}$ and labelled by $b^{\prime}\supseteq b$. We say that $S$ is
_contained_ in $T$ if every finite path in $\mathfrak{T}_{S}$, (i.e., a run in
$S$) is homomorphically embeddable into $\mathfrak{T}_{T}$.

Let
$T=(\Sigma_{1},\Sigma_{2},W^{\prime},L^{\prime},R^{\prime},W_{0}^{\prime})$.
We define the _direct product_ (aka synchronous composition) of $S$ and $T$ as
a transition system $S\times
T=(\Sigma_{1},\Sigma_{2},W^{\prime\prime},L^{\prime\prime},R^{\prime\prime},W_{0}^{\prime\prime})$
with $W^{\prime\prime}=W\times W^{\prime}$, $W_{0}^{\prime\prime}=W_{0}\times
W_{0}^{\prime}$, $L^{\prime\prime}((s,s^{\prime}))=L(s)\cap
L^{\prime}(s^{\prime})$ for all $(s,s^{\prime})\in W^{\prime\prime}$. Then
$R^{\prime\prime}((s,s^{\prime}),(t,t^{\prime}))$ is defined iff both $R(s,t)$
and $R^{\prime}(s^{\prime},t^{\prime})$ are defined, in which case
$R^{\prime\prime}((s,s^{\prime}),(t,t^{\prime}))=R(s,t)\cap
R^{\prime}(s^{\prime},t^{\prime})$. The _disjoint union_ of $S$ and $T$ is a
transition system $S\uplus
T=(\Sigma_{1},\Sigma_{2},W^{\prime\prime},L^{\prime\prime},R^{\prime\prime},W_{0}^{\prime\prime})$
that is obtained by renaming states in $T$ if necessary to make $W$ and
$W^{\prime}$ disjoint, and then taking $W^{\prime\prime}=W\cup W^{\prime}$,
$L^{\prime\prime}=L\cup L^{\prime}$, $R^{\prime\prime}=R\cup R^{\prime}$, and
$W_{0}^{\prime\prime}=W\cup W^{\prime}$. The definitions of the product and
disjoint union are straightforwardly extended to a collection of transition
systems $S_{1},\dots,S_{n}$.

###  C.1 Representations for $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$

Let $\varkappa$ be a $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-query over a
signature $\Sigma$. We can naturally associate $\varkappa$ with a tree
$\mathfrak{T}_{\varkappa}$ as follows. Let
$\varkappa=\varrho_{0}^{\prime}\land\bigwedge_{i}(\varrho_{i}\mathbin{\mathsf{U}}\psi_{i})$,
where $\varrho_{0}^{\prime},\varrho_{i}$ is a conjunction of $\Sigma$-atoms,
$\psi_{i}=\varrho^{\prime}_{i}\land\bigwedge_{j}(\varrho_{j}\mathbin{\mathsf{U}}\psi_{j})$,
and $\varrho_{i}^{\prime}$ is a conjunction of $\Sigma$-atoms. We do not
distinguish between a conjunction and a set of atoms. The root of the tree is
$r$ and the tree has $r\to(\varrho_{i}\mathbin{\mathsf{U}}\psi_{i})$ for each
$i$, i.e., there are vertices $\varrho_{i}\mathbin{\mathsf{U}}\psi_{i}$. The
root $r$ is labelled with $\varrho^{\prime}_{0}$ and each
$\varrho_{i}\mathbin{\mathsf{U}}\psi_{i}$ is labelled with
$\varrho_{i}^{\prime}$. Each edge
$r\to(\varrho_{i}\mathbin{\mathsf{U}}\psi_{i})$ is labelled with
$\varrho_{i}$. The tree then contains
$(\varrho_{i}\mathbin{\mathsf{U}}\psi_{i})\to(\varrho_{j}\mathbin{\mathsf{U}}\psi_{j})$
for each $j$, where each such edge is labelled with ${\varrho_{j}}$ and
$(\varrho_{j}\mathbin{\mathsf{U}}\psi_{j})$ is labelled with the set of atoms
of $\psi_{j}$, and so on. Thus, we will treat any
$\varkappa\in\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$ as a tree. The other way
round, every finite tree $\mathfrak{T}$ with vertices labelled with subsets of
$\Sigma$ and edges labelled with subsets of $\Sigma\cup\\{\bot\\}$ corresponds
to a $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-query. Indeed, let $x$ be any
leaf of $\mathfrak{T}$. Then we define a
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-query
$\varkappa_{x}=\bigwedge\varrho$, where $\varrho$ is a label of $x$. Suppose
now we have $x\to y_{i}$, for $i\in I$ in $\mathfrak{T}$, and the label of $x$
is $\varrho$ while the label of $x\to y_{i}$ is $\varrho_{i}$. We define
$\varkappa_{x}=(\bigwedge\varrho)\land\bigwedge_{i\in
I}((\bigwedge\varrho_{i})\mathbin{\mathsf{U}}\varkappa_{y_{i}})$. The query
$\varkappa_{r}$, where $r$ is the root of $\mathfrak{T}$, is the required
query representing $\mathfrak{T}$. We denote it by $\varkappa_{\mathfrak{T}}$.

Let $\mathcal{D}$ be a data instance and $\mathcal{O}$ an LTL-ontology over a
signature $\Sigma$. Let $S$ be a transition system over $\Sigma$. We say that
$S$ _represents_ $\mathcal{O},\mathcal{D}$ if the following conditions hold:
$(i)$ $\mathcal{O},\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ for
every finite subtree $\mathfrak{T}^{\prime}$ of $\mathfrak{T}_{S}$; $(ii)$
$\mathfrak{T}_{\varkappa}$ is homomorphically embeddable into
$\mathfrak{T}_{S}$ for each $\varkappa$ with
$\mathcal{O},\mathcal{D}\models\varkappa$.

######  Lemma 20.

Let $E=(E^{+},E^{-})$, $E^{+}=\\{\mathcal{D}_{i}\mid i\in I^{+}\\}$,
$E^{-}=\\{\mathcal{D}_{i}\mid i\in I^{-}\\}$, and let $\mathcal{O}$ be an LTL
ontology. Let $S^{i}$ represent $\mathcal{O},\mathcal{D}_{i}$, for $i\in
I^{+}\cup I^{-}$. Then $(i)$ $E$ is not
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separable under $\mathcal{O}$ iff
$\prod_{i\in I^{+}}S^{i}$ is simulated by $\uplus_{i\in I^{-}}S^{i}$; $(ii)$
$E$ is not $\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]$-separable under
$\mathcal{O}$ iff $\prod_{i\in I^{+}}S^{i}$ is contained in $\uplus_{i\in
I^{-}}S^{i}$.

###### Proof.

We show $(i)$. For $(\Rightarrow)$, suppose $S^{+}=\prod_{i\in I^{+}}S^{i}$ is
not simulated by $S^{-}=\uplus_{i\in I^{-}}S^{i}$. It follows that there
exists a finite subtree $\mathfrak{T}$ of $\mathfrak{T}_{S^{+}}$ that is not
homomorphically embeddable into $\mathfrak{T}_{S^{-}}$. We claim that
$\varkappa_{\mathfrak{T}}$ separates $E$ under $\mathcal{O}$. First, we show
that $\mathcal{O},\mathcal{D}_{i}\models\varkappa_{\mathfrak{T}}$ for each
$i\in I^{+}$. Indeed, for any such $i$, let $\mathfrak{T}^{i}$ be a projection
of $\mathfrak{T}$ to the runs of $S^{i}$. Clearly, $\mathfrak{T}^{i}$ is a
finite subtree of $\mathfrak{T}_{S^{i}}$ and
$\varkappa_{\mathfrak{T}^{i}}\models\varkappa_{\mathfrak{T}}$ ($\mathfrak{T}$
is homomorphically embeddable into $\mathfrak{T}_{i}$). Because $S^{i}$
represents $\mathcal{O},\mathcal{D}_{i}$, we obtain
$\mathcal{O},\mathcal{D}_{i}\models\varkappa_{\mathfrak{T}}$. Second, we show
that $\mathcal{O},\mathcal{D}_{i}\not\models\varkappa_{\mathfrak{T}}$ for each
$i\in I^{-}$. For the sake of contradiction, suppose
$\mathcal{O},\mathcal{D}_{i}\models\varkappa_{\mathfrak{T}}$ for some such
$i$. Because $S^{i}$ represents $\mathcal{O},\mathcal{D}_{i}$, it follows that
$\mathfrak{T}$ is homomorphically embeddable into $\mathfrak{T}_{S^{i}}$, and
so $\mathfrak{T}$ is homomorphically embeddable into $\mathfrak{T}_{S^{-}}$,
which is a contradiction. The proofs of $(\Rightarrow)$ and $(ii)$ are
similar. ∎

#### Constructing representations for queries without an ontology.

Given $\mathcal{D}$, we construct a transition system $S$ with the states
$0,\dots,(\max\mathcal{D}+1)$, where $(\max\mathcal{D}+1)$ is labelled with
$\emptyset$ and the remaining $j$ by $\\{A\mid A(j)\in\mathcal{D}\\}$.
Transitions are $j\to k$, for $0\leq j<k\leq\max\mathcal{D}+1$, that are
labelled by $\\{A\in\Sigma\cup\\{\bot\\}\mid A(n)\in\mathcal{D},n\in(j,k)\\}$
and $(\max\mathcal{D}+1)\to(\max\mathcal{D}+1)$ with label
$\Sigma^{\bot}=\Sigma\cup\\{\bot\\}$.

######  Lemma 21.

$S$ represents $\emptyset,\mathcal{D}$.

###### Proof.

First, we show that $\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ for
every finite subtree $\mathfrak{T}^{\prime}$ of $\mathfrak{T}_{S}$. Let
${\mathcal{I}}_{\mathcal{D}}$ be an LTL interpretation such that
${\mathcal{I}}_{\mathcal{D}},n\models A$ iff $A(n)\in\mathcal{D}$, for any
atom $A$. We observe that any LTL interpretation ${\mathcal{I}}$ can be viewed
as a transition system with the states $n\in\mathbb{N}$ that are labelled with
(sets of) atoms $A$ holding at $n$. The transitions hold between any pair of
states $n<m$ and each such transition is labelled with atoms $A$ or $\bot$
that hold at each $i\in(n,m)$. It is clear that
$\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ iff
$\mathfrak{T}^{\prime}$ is homomorphically embeddable into
$\mathfrak{T}_{{\mathcal{I}}_{\mathcal{D}}}$. We define an embedding $h$ of
$\mathfrak{T}^{\prime}$ into ${\mathcal{I}}_{\mathcal{D}}$ as follows. We set
$h(0)=0$. Suppose $h(\mathfrak{s})$ for $\mathfrak{s}=0\to s_{1}\to\dots\to
s_{n}$ has been defined and let $\mathfrak{s}^{\prime}=0\to s_{1}\to\dots\to
s_{n+1}$. If $s_{n+1}<\max\mathcal{D}+1$, then we set
$h(\mathfrak{s}^{\prime})=s_{n+1}$. If $s_{n+1}=\max\mathcal{D}+1$, then we
set $h(\mathfrak{s}^{\prime})=h(\mathfrak{s}^{\prime})+1$. Clearly, $h$ is a
homomorphism. Therefore, $\mathfrak{T}^{\prime}$ is homomorphically embeddable
into $\mathfrak{T}_{{\mathcal{I}}_{\mathcal{D}}}$ and
$\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$.

Second, we show that $\mathfrak{T}_{\varkappa}$ is homomorphically embeddable
into $\mathfrak{T}_{S}$ for each $\varkappa$ such that
$\mathcal{D}\models\varkappa$. Take any $\varkappa$ such that
$\mathcal{D}\models\varkappa$. It follows that $\mathfrak{T}_{\varkappa}$ is
homomorphically embeddable into $\mathfrak{T}_{{\mathcal{I}}_{\mathcal{D}}}$.
It remains to observe that $\mathfrak{T}_{{\mathcal{I}}_{\mathcal{D}}}$ is
homomorphically embeddable into $\mathfrak{T}_{S}$ (the definition of $h$ is
left to the reader). ∎

The criterion of Theorem 6 now follows immediately from the two previous
lemmas. The remaining P and PSpace upper bounds from Table 1 are explained in
the main part of the paper.

#### Constructing representations for queries with an
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology.

Let $\mathcal{D}$ be a data instance and $\mathcal{O}$ an
$\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}}$-ontology.
Let $\mathcal{C}_{\mathcal{O},\mathcal{D}}$ be the canonical model of
$\mathcal{O},\mathcal{D}$ and $s_{\mathcal{O},\mathcal{D}}$,
$p_{\mathcal{O},\mathcal{D}}$ the numbers from Proposition 9. We define $S$
with the states
$\\{0,\dots,\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}+p_{\mathcal{O},\mathcal{D}}-1\\}$.
The label of each state $n$ is
$\\{A\in\Sigma\mid\mathcal{C}_{\mathcal{O},\mathcal{D}},n\models A\\}$. There
are transitions from $n$ to $m$, for each pair of states $n<m$ labelled with
$\\{A\in\Sigma\cup\\{\bot\\}\mid\mathcal{C}_{\mathcal{O},\mathcal{D}},k\models
A\text{ for all }k\in(n,m)\\}$. Moreover, there are transitions from $n$ to
$m$, for
$n,m\in[\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}},\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}+p_{\mathcal{O},\mathcal{D}})$
such that $n\geq m$. A label for such a transition is
$\\{A\in\Sigma\cup\\{\bot\\}\mid\mathcal{C}_{\mathcal{O},\mathcal{D}},k\models
A\text{ for all
}k\in(n,\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}+p_{\mathcal{O},\mathcal{D}})\cup[\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}},m)\\}$.

######  Lemma 22.

$S$ represents $\mathcal{O},\mathcal{D}$.

###### Proof.

First, we show that $\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ for
every finite subtree $\mathfrak{T}^{\prime}$ of $\mathfrak{T}_{S}$. It is
clear from the properties of $\mathcal{C}_{\mathcal{O},\mathcal{D}}$ (see
Section 5) that $\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ iff
$\mathfrak{T}^{\prime}$ is homomorphically embeddable into
$\mathfrak{T}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$. We define an embedding
$h$ of $\mathfrak{T}^{\prime}$ into $\mathcal{C}_{\mathcal{O},\mathcal{D}}$ as
follows. We set $h(0)=0$. Suppose $h(\mathfrak{s})$ for $\mathfrak{s}=0\to
s_{1}\to\dots\to s_{n}$ has been defined and let $\mathfrak{s}^{\prime}=0\to
s_{1}\to\dots\to s_{n+1}$. If $s_{n+1}>s_{n}$, we set
$h(\mathfrak{s}^{\prime})=h(\mathfrak{s})+(s_{n+1}-s_{n})$. Otherwise, we set
$h(\mathfrak{s}^{\prime})=h(\mathfrak{s})+p_{\mathcal{O},\mathcal{D}}-(s_{n}-s_{n+1})$.
It is readily verified that $h$ is a homomorphism. Therefore,
$\mathfrak{T}^{\prime}$ is homomorphically embeddable into
$\mathfrak{T}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$ and
$\mathcal{O},\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$.

Second, we show that $\mathfrak{T}_{\varkappa}$ is homomorphically embeddable
into $\mathfrak{T}_{S}$ for each $\varkappa$ such that
$\mathcal{O},\mathcal{D}\models\varkappa$. Take any $\varkappa$ such that
$\mathcal{O},\mathcal{D}\models\varkappa$. It follows that
$\mathfrak{T}_{\varkappa}$ is homomorphically embeddable into
$\mathfrak{T}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$. It remains to show
that $\mathfrak{T}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$ is homomorphically
embeddable into $S$. To this end, we define a map
$r\colon\mathbb{N}\to[0,\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}+p_{\mathcal{O},\mathcal{D}})$
by setting $r(n)=n$ if
$n\in[0,\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}+p_{\mathcal{O},\mathcal{D}})$
and $r(n)=((n-\max\mathcal{D}-s_{\mathcal{O},\mathcal{D}})\text{ mod
}p_{\mathcal{O},\mathcal{D}})+\max\mathcal{D}+s_{\mathcal{O},\mathcal{D}}$,
otherwise. Now, we define $h(\mathfrak{s})$ for $\mathfrak{s}=0\to
s_{1}\to\dots\to s_{n}$ (note that $s_{i}\in\mathbb{N}$ and $s_{i+1}>s_{i}$)
to be equal to $r(s_{n})$. It is readily verified that $h$ is a homomorphism
from $\mathfrak{T}_{\mathcal{C}_{\mathcal{O},\mathcal{D}}}$ into $S$. ∎

Now we can explain the data complexity upper bounds from Theorem 12 (the upper
bounds from Theorem 11 are explained in the main paper) for
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q})$
with
$\mathcal{Q}\in\\{\mathcal{Q}[\mathbin{\mathsf{U}}_{s}],\mathcal{Q}_{p}[\mathbin{\mathsf{U}}]\\}$.
The result for
$\mathsf{QBE}^{\mathsf{b}\text{+}}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$
(and so for
$\mathsf{QBE}^{\mathsf{b}\text{+}}_{\mathsf{b}\text{-}}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$)
follows from the fact that $\mathfrak{P}=\prod_{i\in I^{+}}S^{i}$ and
$\mathfrak{U}=\uplus_{i\in I^{-}}S^{i}$ are constructible in P in the size of
$E$. This is not the case for
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$;
here, we use the observation that if there exists a finite subtree
$\mathfrak{T}$ of $\mathfrak{T}_{\mathfrak{P}}$ that is not homomorphically
embeddable into $\mathfrak{U}$, then there exists such $\mathfrak{T}$
satisfying the property that every $s$ from $\mathfrak{P}$ occurs on each path
of $\mathfrak{T}$ at most $|\mathfrak{U}|$-many times. Let $N^{+}=\prod_{i\in
I^{+}}p_{\mathcal{O},\mathcal{D}_{i}}$. We claim that $\mathfrak{T}$ is a
subtree of $\mathfrak{T}_{\mathfrak{P}}^{M}$ for $M=\max_{i\in
I^{+}}\\{\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}}\\}+N^{+}|\mathfrak{U}|$.
Indeed, in the required $\mathfrak{T}$, if there is a path that is longer than
$M$, the property above would be violated. By our construction of $S^{i}$, any
$n$-th element, for $n\geq\max_{i\in
I^{+}}\\{\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}}\\}$, of any path
of $\mathfrak{T}_{\mathfrak{P}}$ is of the form $(t_{1},\dots,t_{|I^{+}|})$,
where
$t_{i}\in[\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}},\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}}+p_{\mathcal{O},\mathcal{D}_{i}})$.
Observe that $(t_{1},\dots,t_{|I^{+}|})\to(s_{1},\dots,s_{|I^{+}|})$ in
$\mathfrak{P}$, for $(t_{1},\dots,t_{|I^{+}|})$ as above, implies
$s_{i}\in[\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}},\max\mathcal{D}_{i}+s_{\mathcal{O},\mathcal{D}_{i}}+p_{\mathcal{O},\mathcal{D}_{i}})$
and any sequence
$(t_{1},\dots,t_{|I^{+}|})\to\dots\to(s_{1},\dots,s_{|I^{+}|})$ as above in
$\mathfrak{P}$ longer than $N^{+}|\mathfrak{U}|$ will have some
$(t_{1},\dots,t_{|I^{+}|})$ repeated more than $|\mathfrak{U}|$ times. Thus,
in order to decide
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}[\mathbin{\mathsf{U}}_{s}])$,
we need to check if $\mathfrak{T}_{\mathfrak{P}}^{M}$ is homomorphically
embeddable into $\mathfrak{U}$. The latter can be checked by constructing
$\smash{\mathfrak{T}_{\mathfrak{P}}^{M}}$ branch-by-branch while checking all
possible embeddings of these branches into $\mathfrak{U}$. Since $M$ is
polynomial in $E$, this algorithm works in PSpace in the size of $E$.

It remains to explain the NP upper bound for
$\mathsf{QBE}(\textsl{LTL}_{\textit{horn}}^{\smash{\Box\raisebox{1.0pt}{$\scriptscriptstyle\bigcirc$}}},\mathcal{Q}_{p}[\mathbin{\mathsf{U}}])$.
From Lemma 20 and the argument above, it follows that $E$ is separable under
$\mathcal{O}$ iff there exists a path in $\mathfrak{T}_{\mathfrak{P}}^{M}$
that is not embeddable into $\mathfrak{U}$. Such a path (if exists) is of the
size polynomial in $E$. Embeddability of such a path into $\mathfrak{U}$ can
be checked in P from $E^{-}$ and the size of the path.

#### Constructing representations for queries with an LTL-ontology.

Let $\mathcal{D}$ be a data instance and $\mathcal{O}$ an LTL-ontology. We can
assume that $\max\mathcal{D}=0$. Indeed, for a given $\mathcal{O}$ and $E$, we
can construct in polytime an LTL-ontology $\mathcal{O}^{\prime}$ and
$E^{\prime}$ such that $\max\mathcal{D}^{\prime}=0$ for each
$\mathcal{D}^{\prime}$ in $E^{\prime}$ and $E$ is
$\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separable under $\mathcal{O}$ iff
$E^{\prime}$ is $\mathcal{Q}[\mathbin{\mathsf{U}}_{s}]$-separable under
$\mathcal{O}^{\prime}$. Let $\boldsymbol{T}_{\mathcal{O}}$ be the set of
$\mathcal{O}$-types. For
$\boldsymbol{T}\subseteq\boldsymbol{T}_{\mathcal{O}}$, we say that
$\boldsymbol{T}$ is _realisable in_ $\mathcal{O},\mathcal{D}$ if there are
instants $n_{\mathcal{I}}$ in all models ${\mathcal{I}}$ of
$\mathcal{O},\mathcal{D}$ such that
$\\{\textit{tp}_{\mathcal{I}}(n_{\mathcal{I}})\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}=\boldsymbol{T}$.
For
$\boldsymbol{T}_{1},\boldsymbol{T}_{2}\subseteq\boldsymbol{T}_{\mathcal{O}}$
realisable in $\mathcal{O},\mathcal{D}$ and
$\Gamma\subseteq\Sigma\cup\\{\bot\\}$, we define
$\boldsymbol{T}_{1}\to_{\Gamma}\boldsymbol{T}_{2}$ if there are instants
$n_{\mathcal{I}}<m_{\mathcal{I}}$ in all models ${\mathcal{I}}$ of
$\mathcal{O},\mathcal{D}$ such that $(i)$
$\\{\textit{tp}_{\mathcal{I}}(n_{\mathcal{I}})\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}=\boldsymbol{T}_{1}$,
$(ii)$
$\\{\textit{tp}_{\mathcal{I}}(m_{\mathcal{I}})\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}=\boldsymbol{T}_{2}$,
$(iii)$
$\\{\textit{tp}_{\mathcal{I}}(k)\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D},n_{\mathcal{I}}<k<m_{\mathcal{I}}\\}\cap\boldsymbol{T}_{2}=\emptyset$,
$(iv)$ $\Gamma=\\{A\in\Sigma^{\bot}\mid{\mathcal{I}},k\models A\text{ for all
}{\mathcal{I}}\models\mathcal{O},\mathcal{D},n_{\mathcal{I}}<k<m_{\mathcal{I}}\\}$.
We observe that condition $(iii)$ ensures that there exists at most one
$\Gamma$ for given $\boldsymbol{T}_{1},\boldsymbol{T}_{2}$ such that
$\boldsymbol{T}_{1}\to_{\Gamma}\boldsymbol{T}_{2}$. We define $S$ with the
states $\boldsymbol{T}\subseteq\boldsymbol{T}_{\mathcal{O}}$ realisable in
$\mathcal{O},\mathcal{D}$. A single initial state of $S$ is
$\boldsymbol{T}_{0}=\\{\textit{tp}_{\mathcal{I}}(0)\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}$.
The states $\boldsymbol{T}$ are labelled with $\\{A\in\Sigma\mid
A\in\textit{tp}\text{ for all }\textit{tp}\in\boldsymbol{T}\\}$. There are
transitions from $\boldsymbol{T}_{1}$ to $\boldsymbol{T}_{2}$ where
$\boldsymbol{T}_{1}\to_{\Gamma}\boldsymbol{T}_{2}$ holds for some $\Gamma$,
labelled with $\Gamma$.

######  Lemma 23.

$S$ represents $\mathcal{O},\mathcal{D}$.

###### Proof.

Let
$\boldsymbol{{\mathcal{I}}}=\\{{\mathcal{I}}\mid{\mathcal{I}}\models\mathcal{O},\mathcal{D}\\}$.
We treat every ${\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}$ as a transition
system as we did above. Take the product
$\prod_{{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}}{\mathcal{I}}$ and denote
it (slightly abusing notation) by $\boldsymbol{{\mathcal{I}}}$. Note that the
states $s$ of $\boldsymbol{{\mathcal{I}}}$ are maps
$s\colon\boldsymbol{{\mathcal{I}}}\to\mathbb{N}$.

First, we show that
$\mathcal{O},\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$ for every
finite subtree $\mathfrak{T}^{\prime}$ of $\mathfrak{T}_{S}$. It should be
clear that $\mathcal{O},\mathcal{D}\models\varkappa_{\mathfrak{T}^{\prime}}$
iff $\mathfrak{T}^{\prime}$ is homomorphically embeddable into
$\mathfrak{T}_{\boldsymbol{{\mathcal{I}}}}$. We define an embedding $h$ of
$\mathfrak{T}^{\prime}$ into $\boldsymbol{{\mathcal{I}}}$ as follows. We set
$h(\boldsymbol{T}_{0})=s_{0}$, where $s_{0}$ is the initial state of
$\boldsymbol{{\mathcal{I}}}$ satisfying $s_{0}({\mathcal{I}})=0$ for every
${\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}$. Suppose $h(\mathfrak{s})$ for
$\mathfrak{s}=\boldsymbol{T}_{0}\to\boldsymbol{T}_{1}\to\dots\to\boldsymbol{T}_{n}$
has been defined equal to $s$. Our induction hypothesis will be that
$\boldsymbol{T}_{n}=\\{\textit{tp}_{\mathcal{I}}(s({\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}$.
It can be readily verified that it holds for
$\mathfrak{s}=\boldsymbol{T}_{0}$. Let
$\mathfrak{s}^{\prime}=\boldsymbol{T}_{0}\to\boldsymbol{T}_{1}\to\dots\to\boldsymbol{T}_{n+1}$
and $\boldsymbol{T}_{n}\to_{\Gamma}\boldsymbol{T}_{n+1}$. For each
${\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}$, we select
$m_{\mathcal{I}}>s({\mathcal{I}})$ such that
$\boldsymbol{T}_{n+1}=\\{\textit{tp}_{\mathcal{I}}(m_{\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}$
and $\Gamma=\\{A\in\Sigma^{\bot}\mid{\mathcal{I}},k\models A\text{ for all
}{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}},s({\mathcal{I}})<k<m_{\mathcal{I}}\\}$.
That this selection is always possible follows from the IH. We then set
$h(\mathfrak{s}^{\prime})=s^{\prime}$ such that
$s^{\prime}({\mathcal{I}})=m_{\mathcal{I}}$ for
${\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}$.

Now, we show that $\mathfrak{T}_{\varkappa}$ is homomorphically embeddable
into $\mathfrak{T}_{S}$ for each $\varkappa$ such that
$\mathcal{O},\mathcal{D}\models\varkappa$. Take any $\varkappa$ such that
$\mathcal{O},\mathcal{D}\models\varkappa$. It follows that
$\mathfrak{T}_{\varkappa}$ is homomorphically embeddable into
$\mathfrak{T}_{\boldsymbol{{\mathcal{I}}}}$. It remains to show that
$\mathfrak{T}_{\boldsymbol{{\mathcal{I}}}}$ is homomorphically embeddable into
$S$. We define $h$ so that $h(s_{0})=\boldsymbol{T}_{0}$. Consider now
$\mathfrak{s}_{1}=s_{0}\to s_{1}$. Instead of $s_{1}$, we can always select
$s_{1}^{\prime}$ such that $s_{0}\to s_{1}^{\prime}$,
$\\{\textit{tp}_{\mathcal{I}}(s_{1}^{\prime}({\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}\subseteq\\{\textit{tp}_{\mathcal{I}}(s_{1}({\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}$,
$\\{\textit{tp}_{\mathcal{I}}(k)\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}},s_{0}({\mathcal{I}})<k<s_{1}^{\prime}({\mathcal{I}})\\}\cap\\{\textit{tp}_{\mathcal{I}}(s_{1}^{\prime}({\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}=\emptyset$
and, finally,
$\\{\textit{tp}_{\mathcal{I}}(k)\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}},s_{0}({\mathcal{I}})<k<s_{1}^{\prime}({\mathcal{I}})\\}\subseteq\\{\textit{tp}_{\mathcal{I}}(k)\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}},s_{0}({\mathcal{I}})<k<s_{1}({\mathcal{I}})\\}$.
We define
$h(\mathfrak{s}_{1})=\\{\textit{tp}_{\mathcal{I}}(s_{1}^{\prime}({\mathcal{I}}))\mid{\mathcal{I}}\in\boldsymbol{{\mathcal{I}}}\\}$.
It can be readily verified, given the subsumptions above, that (subsumption of
the) label of the edge from $s_{0}$ to $\mathfrak{s}_{1}$ is preserved under
$h$ and (subsumption of) the node $\mathfrak{s}_{1}$ is preserved under $h$.

Consider now $\mathfrak{s}_{2}=s_{0}\to s_{1}\to s_{2}$. We can always select
$s_{2}^{\prime}$ so that $s_{1}^{\prime}\to s_{2}^{\prime}$,