Reverse Engineering of Temporal Queries 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´o 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´errez-Basulto et al., 2018; Ortiz, 2019; Cima et al., 2021; Jung et al., 2021; Jung et al., 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 (D, d) with a database instance D and a tuple d in D, a (possibly empty) ontology O, and a query language Q.

Problem: decide whether there exists a query q ∈ Q separating (E+,E-) in the sense that O,D |= q(d) for all (D, d) ∈ E+ and O, D ̸|= q(d) for all (D, d) ∈ E-.

If such a q exists, then (E+,E-) is often called satisfiable w.r.t. Q under O, and the construction of 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 queryby-example by focusing on the basic but very useful case where data D is a set of timestamped atomic propositions. Our query languages are positive fragments of linear temporal logic LTL with the temporal operators ✸ (eventually), ⃝ (next), and U (until) interpreted under the strict semantics [Demri et al., 2016]. To enforce generalisation, we do not admit ∨. Our most expressive query language Q[U] is thus defined as the set of formulas constructed from atoms using ∧ and U (via which ⃝ and ✸ are expressible); the fragments Q[✸] and Q[⃝,✸] are defined analogously. Ontologies can be given in full LTL or its fragments LTL ✷✸ (known as the Prior logic [Prior, 1956]), which only uses the operators ✷ (always in the future) and ✸, and the Horn fragment LTL ✷⃝ horn containing axioms of the formC1∧· · ·∧Ck → Ck+1, where the Ci are atoms possibly prefixed by ✷ and ⃝ for i ≤ k + 1, and also by ✸ for i ≤ 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 realworld 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.

Within this 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;

Omitted details and proofs are available in [Fortin et al., 2023].

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 D+ 1 and D+ 2 below but did not stop after the runs D1 , D2 , D3 , where we assume the runs to start at 0 and measurements to be recorded at moments 0, 1, 2, . . . :

The ✸-query q = ✸(T ∧✸✸V ) is true at 0 in the D+ i , false in Di , and so gives a possible explanation of what could cause the engine failure. The example set ({D+ 3 ,D+ 4 }, {D4 }) with

is explained by the U-query T UV . Using background knowledge, we can compensate for sensor failures resulting in incomplete data. To illustrate, suppose E + 1 = {H(3), V (4)}, where H means 'heater is on'. If an ontology O has the axiom ⃝H → T saying that a heater can only be triggered by the low temperature at the previous moment, then the same q separates {E + 1 ,D+ 2 } from {D1 ,D2 ,D3 } under O. ⊣

Query 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' ✸T ∧✸V . More precisely, path ⃝✸-queries in the class Qp[⃝,✸] take the form

where oi ∈ {⃝,✸} and ρi is a conjunction of atoms; Qp[✸] restricts oi to {✸}; and path U-queries Qp[U] look like

where λi is a conjunction of atoms or ⊥. 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 ∨, multiple negative examples become redundant: if qD separates (E+, {D}), for each D ∈ E-, then ∧D∈E- qD 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 Qp[✸]-query with ρ0 = ⊤ and ρi ̸= ⊤ 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✸(ρ1∧⃝(ρ2∧· · ·∧⃝ρ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 Q[✸]-query ✸T ∧✸V while no path query is capable of doing this. ⊣

Branching Q[⃝,✸]-queries express transparent existential conditions and can be regarded as LTL CQs. However, branching Q[U]-queries with nestings of U on the left-hand side correspond to complex first-order formulas with multiple alternations of quantifiers ∃ and ∀, which are hard to comprehend. So we also consider the language Q[Us] ⊇ Qp[U] of 'simple' Q[U]-queries without such nestings.

In this paper, we take the first steps towards understanding the complexity and especially feasibility of the queryby-example problems QBE(L, Q) with L an ontology and 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 are summarised in Table 1, where

b+ / b- indicate that the number of positive / negative examples is bounded 1 . 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 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 Qp[✸], Q[✸] can also be obtained from [Fijalkow and Lagarde, 2021] who studied separability by Q[✸]-queries of bounded size.

In the presence of ontologies, we distinguish between the combined complexity of QBE(L, 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: Qp[✸]- and Q[✸]-queries mediated by LTL ✷✸ -ontologies and all of our queries mediated by LTL ✷⃝ horn -ontologies enjoy the same data complexity as in Table 1. The combined complexity results for queries with LTL ✷⃝ horn -ontologies we have obtained so far are given inTable 2. Interestingly, QBE for query classeswith ✸ and ⃝ only is PSPACE-complete- 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 U-queries are by reduction to the simulation and containment problems for exponentialsize transition systems. For arbitrary LTL-ontologies, this technique only gives a 2EXPTIME upper bound for Q[Us] and a 2EXPSPACE one for Qp[U]. Separability by (path) ✸- queries under LTL ✷✸ ontologies turns out to be Σp2 -complete, where the upper bound is shown by establishing the PSP.

1 We do not consider queries with ⃝ only as separability is trivially in P and does not detect any useful patterns.

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 ELI or ALC ontologies [Funk et al., 2019; Jung et al., 2020].

2 Further RelatedWork

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¨uhmann et al., 2016], DL-FOIL [Fanizzi et al., 2018] and its extension DLFOCL [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 O, D |= ¬q(d)-and not just O, D ̸|= q(d)-for all (D, d) ∈ E-.

3 Preliminaries

LTL-formulas are built from atoms Ai, i < ω, using the Booleans and (future-time) temporal operators ⃝, ✸, ✷, U, which we interpret under the strict semantics [Gabbay et al., 2003; Demri et al., 2016]. An LTL-interpretation I identifies those atoms Ai that are true at each time instant n ∈ N, written I, n |= Ai. The truth-relation for atoms is extended inductively to LTL-formulas by taking I, n |= φ U ψ iff I, m |= ψ, for some m > n, and I, k |= φ for all k ∈ (n, m), and using the standard clauses for the Booleans and equivalences ⃝φ ≡ ⊥ U φ, ✸φ ≡ ⊤ U φ and ✷φ ≡ ¬✸¬φ with Boolean constants ⊥ and ⊤ for 'false' and 'true'.

An LTL-ontology, O, is any finite set of LTL-formulas, called the axioms of O. An interpretation I is a model of O if all axioms of O are true at all times in I. As mentioned in the introduction, apart from full LTL we consider its Prior ✷✸- fragment LTL ✷✸ and LTL ✷⃝ horn whose axioms take the form

with Ci given by C ::= Ai | ⊥ | ✷C | ⃝C. In fact, we could allow ✸ on the left-hand side of (3) as ✸C → C ′ can be replaced by ⃝C → A, ⃝A → A, A → C ′ with fresh A.

A data instance is a finite set D of atoms Ai(ℓ) with a timestamp ℓ ∈ N; maxD is the maximal timestamp in D. We access data by means of LTL analogues of conjunctive queries: our queries, κ, are constructed from atoms, ⊥ and ⊤ using ∧, ⃝, ✸ and U. The class of queries that only use operators from Φ ⊆ {⃝, ✸, U} is denoted by Q[Φ]; Qp[Φ] is its subclass of path-queries, which take the form (1) or (2); and Q[Us] comprises simple queries in Q[U] that do not contain subqueries κ1 U κ2 with an occurrence of U in κ1. Note that Qp[U] ⊆ Q[Us]. The temporal depth tdp(κ) of κ is the maximum number of nested temporal operators in κ.

An interpretation I is a model of a data instance D if I, ℓ |= Ai for all Ai(ℓ) ∈ D. O and D are consistent if they have a model. We call k ≤ maxD a (certain) answer to the ontology-mediated query (O, κ) over D and write O, D |= κ(k) if I, k |= κ in all models I of O and D.

Let L and Q be an ontology and query language defined above. The query-by-example problem QBE(L,Q) we are concerned with in this paper is formulated as follows:

given an L-ontology 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 Q-separable under O in the sense that there is a Q-query κ with O, D |= κ(0) for all D ∈ E+ and O, D ̸|= κ(0) for all D ∈ E-.

If L = ∅, we shorten QBE(∅,Q) to QBE(Q). We also consider the QBE problems with the input example sets having a bounded number of positive and/or negative examples, denoted QBE b+ (L,Q), QBEb-(L,Q), or QBE b+ b- (L,Q). Notations like QBE2+ 1- (L,Q) should be self-explanatory. The size of O, E, κ, denoted |O, |E|, |κ|, 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 = ({D1}, {D2}) with D1 = {A(1)}, D2 = {A(2)}. Then ⃝A separates E but no Q[✸]-query does. E is not separable under O = {⃝A → A} by any query κ as O,D1 |= κ(0) implies O,D2 |= κ(0).

(b) Let E = ({D1, D2}, {D3}) with D1 = {A(1), B(2)}, D2 = {A(2),B(3)}, D3 = {A(3),B(5)}. Then the query ✸(A ∧ ⃝B) separates E but no query in Q[✸] does.

(c) AUB separates ({{B(1)}, {A(1), B(2)}}, {{B(2)}}) but no Q[⃝, ✸]-query does. ⊣

We now establish a few important polynomial-time reductions, ≤p, among the QBE-problems for various query classes, including Q◦p [✸]-queries of the form

where each ρi is a Qp[⃝]-query (i.e., ✸-free Qp[⃝,✸]-query). Theorem 4. The following polynomial-time reductions hold: (i.1) QBE(L,Q) ≤p QBE1-(L,Q), for any Q closed under ∧, and any L (including L = ∅),

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- = {D1, . . . ,Dn} is Qseparable under O iff each (E+, {Di}) is because if κi separates (E+, {Di}), then κ1 ∧ · · · ∧ κn separates (E+, E-). In (i.2), (E+,E-) with E+ = {D1, . . . ,Dn}, n > 1, is Q-separable under O iff (E′+, E-) is Q-separable under O′ that extends O with the following axioms simulating E+:

where S1, S2, Ak, Cl, Dl, for l ≤ n′ = maxi maxDi, are fresh and E′+ consists of {C0(0), . . . , Ck(n′ ), S1(n′ + 1)} and {D0(0), . . . , Dk(n′ ), S2(n′ + 1)}.

(i.3) Using [ρ0∧✸(ρ1∧∧i ✸κi)] ≡ [ρ0∧∧i ✸(ρ1∧✸κi)], ⃝✸κ ≡ ✸⃝κ and ⃝(κ ∧ κ′ ) ≡ (⃝κ ∧ ⃝κ′ ) we convert, in polytime, each Q[⃝,✸]-query to an equivalent conjunction of Q◦p [✸]-queries. Thus, there is q ∈ Q[⃝,✸] separating (E+,E-) iff there are polysize qD ∈ Q◦p [✸] separating (E+, {D}), for each D ∈ E-.

(ii.1) The first two reductions are shown by adding to E+ ∋ D, for some D, the data instance D′ = {A(mn) | A(n) ∈ D} with m = maxD + 2. Now, if D |= κ(0) and D′ |= κ(0), for κ ∈ Qp[U], then κ is equivalent to a Qp[✸]-query. The third reduction, illustrated below for E+ = {D+ 1 ,D+ 2 } and E- = {D1 ,D2 }, transforms E into two positive and one negative example using 'pads' of fresh atoms B, C. We show

that E is Qp[U]-separable iff ({D′′+ 1 ,D′+ 2 }, {D′-}) is.

(ii.2) The first reduction is established by modifying every D in the given E as illustrated below using fresh atoms Ai and Bj that encode ⃝iA and ⃝j B, respectively:

Then E is Q[⃝,✸]-separable iff E′ is Q[✸]-separable. The converse and the second reduction are similar to (ii.1). ⊣

4 QBE without Ontologies

We start investigating the complexity of the QBE problems for LTL by considering queries without mediating ontologies.

Theorem 5. The 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. ⃝✸-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 QBE b+ b- (Qp[⃝,✸]), E+ = {D+ 1 ,D+ 2 } and E- = {D1 ,D2 }. Suppose κ takes the form (1) with ρn ̸= ⊤. Then D |= κ(0) iff there is a strictly monotone map f : [0, n] → [0,maxD] with f(0) = 0, f(i+1) = f(i)+1 if oi = ⃝, and ρi ⊆ tD(f(i)) = {A | A(f(i)) ∈ D}. We call such an f a satisfying assignment for κ in D. Let Si,j be the set of tuples (k, ℓ1, ℓ2, n1, n2) such that ℓ1 ≤ i ≤ maxD+ 1 , ℓ2 ≤ j ≤ maxD+ 2 , and there is κ = ρ0∧o1(ρ1∧· · ·∧okρk) for which (i) there are satisfying assignments f1, f2 in D+ 1 and D+ 2 with f1(k) = ℓ1 and f2(k) = ℓ2, respectively, and (ii) n1 is minimal with a satisfying assignment f for κ in D1 having f(k) = n1, and n1 = ∞ if there is no such f; and similarly for n2, D2 . It suffices to compute SmaxD+ 1 ,maxD+ 2 in polytime. This can be done incrementally by initially observing that S0,j can only contain (0, 0, 0, 0, 0), which is the case if there is ρ0 ⊆ tD+ 1 (0), ρ0 ⊆ tD+ 2 (0) and ρ0 ̸⊆ tD1 (0), ρ0 ̸⊆ tD2 (0) (and similarly for Si,0).

U-queries. NP-hardness for Qp[U], Q[Us] follows from Theorem 4 (ii.1), (ii.2) and NP-hardness for ⃝✸-queries.

The upper bounds are shown by reduction of Qp[U]- and Q[Us]-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 S0 of start nodes. A run of S is a path in digraph S, starting in S0, together with all of its labels. The computation tree of S is the tree unravelling TS of S. For systems S and S′ over the same alphabets, we say that S is contained in S′ if, for every run r of S, there is a run r′ of S′ such that r and r′ have the same length and the labels on the states and edges in r are subsumed by the corresponding labels in r′ . S is simulated by S′ if TS is finitely embeddable into TS′ in the sense that every finite subtree 2 of TS can be homomorphically mapped into TS′ preserving (subsumption of) node and edge labels.

Now, let E = (E+,E-) with Eσ = {Di | i ∈ I σ }, for σ ∈ {+,-} and disjoint I + and I -, and let Σ be the signature of E. For each i ∈ I + ∪ I -, we take a transition system Si with states 0i , . . . , (maxDi + 1)i , where (maxDi + 1)i is labelled with ∅ and the remaining j i by {A | A(j) ∈ Di}. Transitions are j i → ki , for 0 ≤ j < k ≤ maxDi + 1, that are labelled by {A ∈ Σ ∪ {⊥} | A(n) ∈ Di, n ∈ (j, k)} and (max Di + 1)i → (max Di + 1)i with label Σ⊥ = Σ ∪ {⊥}. Thus, Di shown on the left below gives rise to Si on the right:

2 A subtree is a convex subset of TS's nodes with some start node.

We form the direct product (synchronous composition) P of {Si | i ∈ I +}, for I + = {1, . . . , l}, whose states are vectors (s1, . . . , sl) of states si ∈ Si , which are labelled by the intersection of the labels of si in Si , with transitions (s1, . . . , sl) → (p1, . . . , pl), if si → pi in Si for all i, also labelled by the intersection of the component transition labels. On the other hand, we take the disjoint union N of Si , for i ∈ I -, and establish the following separability criterion:

Theorem 6. (i) E is not Q[Us]-separable iff P is simulated by N. (ii) E is not Qp[U]-separable iff P is contained in N. Example 7. For the example set depicted below, in which the only negative instance is on the right-hand side,

where only the last P-node of a TP-node (a sequence) is indicated together with the atoms that are true at nodes and on edges. Intuitively, TP 'represents' all possible Q[Us]- queries and its paths represent Qp[U]-queries κ such that O, D |= κ(0) for all D ∈ E+. The Q[Us]-query given by the subtree above is κ = ✸(((A1∧B2)UB1)∧((A2∧B1)UB2)). The subtree is not embeddable into TN (obtained for the negative instance), so κ separates E. Observe that every path in TP (and in the subtree above) is embeddable into TN.

By inspecting the structure of P and N we observe that if P has a run that is not embeddable into any run of N, then we can find such a run of length ≤ M = min{maxDi | i ∈ I +} (any longer run has ∅-labels on its states after the Mth one). Thus, we can guess the required run and check in P if it is correct, establishing the NP upper bound for Qp[U]. To show the PSPACE upper bound for Q[Us], we notice that if there is a finite subtree of TP that is not embeddable into TN, then the full subtree TMP of depth M is not embeddable into TN, which can be checked by constructing TMP branch-by-branch while checking all possible embeddings of these branches into TN. Finally, we have the P upper bound for Q[Us] with a bounded number of positive examples because 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 TMP , i.e., exponential in |E+|; however, we can check its existence in polytime.

The PSPACE upper bound for Q[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 Q[U]-query We prove a Q[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 Σ⊥ from all states but u, which are all omitted). Each arrow from 0 leads to a state {1, . . . , n - 1}{n}; it represents a formula φ U ψ that is true at 0, with the arrow label indicating the non-nested atoms of φ and the state label indicating the atoms of ψ. Each black (resp., red) arrow from s1s2 to s′1s′2 represents a U-formula αs2→s′1 s′2 (resp., αs1→s′1 s′2 ) that is true at all points in s2 (resp., s1). The black and red transitions are arranged in such a way that a transition from s′′ 1 s′′ 2 to s1s2 with an arrow label λ and s1s2-label µ represents the U-formula (λ ∧ ∧ αs1→s′1 s′2 ) U (µ ∧ ∧ αs2→s′1 s′2 ) and similarly for the transitions from 0. A version of Theorem 6 for Q[U] and a PSPACE-algorithm are given in the full paper.

5 QBE with LTL ✷⃝ horn -Ontologies

Recall from [Artale et al., 2021] that, for any LTL ✷⃝ horn - ontology O and data instance D consistent with O, there is a canonical model CO,D of O and D such that, for any query κ and any k ∈ N, we have O, D |= κ(k) iff CO,D |= κ(k).

Let subO be the set of subformulas of the Ci in the axioms (3) of O and their negations. A type for O is any maximal subset tp ⊆ subO consistent with O. Let T be the set of all types for O. Given an interpretation I, we denote by tpI (n) the type for O that holds at n ∈ N in I. For O consistent with D, we abbreviate tpCO,D to tpO,D . The canonical models have a periodic structure in the following sense:

Proposition 9. For any LTL ✷⃝ horn ontology O and any data instance D consistent with O, there are sO,D ≤ 2|O| and pO,D ≤ 22|O| such that tpO,D (n) = tpO,D (n + pO,D), for all n ≥ maxD + sO,D. Deciding CO,D |= ξ(ℓ), for a binary ℓ and a conjunction of atoms ξ, is in PSPACE / P for combined / data complexity.

We now show that the combined complexity of QBE with ✸- and ⃝,✸-queries is PSPACE-complete in both bounded and unbounded cases, i.e., as complex as LTL ✷⃝ horn reasoning.

Theorem 10. Let Q ∈ {Q[⃝,✸],Q[✸],Qp[⃝,✸],Qp[✸]}. Then QBE(LTL ✷⃝ horn ,Q) and QBE b+ b- (LTL ✷⃝ horn ,Q) are both PSPACE-complete for combined complexity.

Proof. PSPACE-hardness is inherited from that of LTL ✷⃝ horn . We briefly sketch the proof of the matching upper bound for Q[⃝, ✸] using the reduction of Theorem 4 (i.3). We can assume that O and D are consistent for any D ∈ E+ ∪E-. For if O and D ∈ E- are inconsistent, then E is not Q-separable under O as O, D |= κ(0) for all κ ∈ Q; if O and D ∈ E+ are inconsistent, then E is separable iff (E+ \ {D},E-) is. Checking consistency is known to be PSPACE-complete.

Given an LTL ✷⃝ horn -ontology O and an example set E, let

where sO,D and pO,D in CO,D are from Proposition 9. We show that if E is Q[⃝,✸]-separable under O, then it is separated by a conjunction of |E-|-many κ ∈ Q◦p [✸] of ✸-depth ≤ k + 1 and ⃝-depth ≤ k +m in (4). Indeed, in this case any (E+, {D}), for D ∈ E-, is separated under O by some κ of the form (4) with the ρl of ⃝-depth ≤ k +m because ρl = ∧ℓi=0 ⃝iλi with ℓ > k + m can be replaced by

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

and so by some ρ0 ∧ ✸(ρ1 ∧ · · · ∧ ✸(ρk ∧ ✸ρj)) with k < j ≤ n. Our nondeterministic PSPACE-algorithm incrementally guesses the ρl and checks if they are satisfiable in the relevant part of the relevant CO,D bounded by k +m. ⊣

The situation is quite different for queries with U:

Theorem11. QBE(LTL ✷⃝ horn ,Q[Us]) is in EXPTIME for combined complexity, QBE(LTL ✷⃝ horn ,Qp[U]) is in EXPSPACE, and QBE b+ b- (LTL ✷⃝ horn ,Qp[U]) is NEXPTIME-hard.

Proof. For the upper bounds, we again assume that O and D are consistent for all D ∈ E+ ∪E-. Observe that Theorem 6 continues to hold in the presence of LTL ✷⃝ horn ontologies O but we need a different construction of transition systems Si that represent all Q[Us]-queries mediated by O over Di. We illustrate it for O = {A → C ∧⃝B, B → ⃝2B, B → ⃝C} and Di = {A(0)} below, where the picture on the left shows the canonical model of O,Di (see Proposition 9) and next to it is Si (the omitted labels on transitions are Σ⊥).

In general, the size of Si is |Di|+O(2|O| ) and the product of Si , Di ∈ E+ is of size O(2|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 M be a non-deterministic Turing machine that accepts Σ-words x = x1 . . . xn in N = 2poly(|x|) steps and erases the tape after a successful computation. We represent configurations c of a computation of M on 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 ∈ Q. An accepting computation of M on x is encoded by the N 2 -long word w = ♯c1 ♯ c2 ♯ . . . ♯ cN-1 ♯ cN over Ξ = Σ ∪ (Q × Σ) ∪ {♯}. Thus, a word w of length N 2 encodes an accepting computation iff it starts with the initial configuration c1 preceded by ♯, ends with the accepting configuration cacc, and every two length 3 subwords at distance N apart form a legal tuple [Sipser, 1997, Theorem 7.37].

We define O and E = ({D+ 1 ,D+ 2 }, {D-}) so that their canonical models look as follows, for Ξ = {a1, . . . , ak}:

and ti = (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 LTL ✷⃝ horn ontology O as in [Ryzhikov et al., 2021]. We show that the Qp[U]-query

where ρ1 . . . ρN 2 encodes an accepting computation of M on x, is the only type of query that can separate E under O. ⊣

As for data complexity, we show that LTL ✷⃝ horn -ontologies come essentially for free:

Theorem 12. The results of Theorem 5 continue to hold for queries mediated by a fixed LTL ✷⃝ horn -ontology.

Intuitively, the reason is that, given a fixed LTL ✷⃝ horn - ontology O, we can compute the types of the canonical model CO,D, for consistent O and D, in polynomial time in D by Proposition 9, with the length M from Section 4 being polynomial in E. Checking consistency of D and fixed O is known to be in P [Artale et al., 2021].

6 QBE with LTL ✷✸ -Ontologies

In this section, we investigate separability by ✸-queries under LTL ✷✸ -ontologies. Remarkably, we show that, for data complexity, LTL ✷✸ -ontologies also come for free despite admitting arbitrary Boolean operators; cf., [Schaerf, 1993].

Theorem 13. Let Q ∈ {Qp[✸],Q[✸]}. If E is Q-separable under an LTL ✷✸ -ontology O, then E can be separated under O by a Q-query of polysize in E and O. QBE(LTL ✷✸, Q) and QBE b+ b- (LTL ✷✸,Q) are Σp2 -complete for combined complexity. The presence of LTL ✷✸ -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 Qp[✸]. Taking into account NP-completeness of checking if O is consistent with D and tractability of this problem for a fixed O [Artale et al., 2021], we can assume, as in Theorem 10, that O and D are consistent for each D ∈ E+ ∪ E-. Observe first that if E is separated by κ ∈ Qp[✸] of the form (1) under an LTL ✷✸ -ontology O, then, as follows from [Ono and Nakamura, 1980], for any D ∈ E-, there is a model JD ̸|= κ(0) of O and D whose types form a sequence

with maxD ≤ k ≤ maxD + |O| and l ≤ |O|. This allows us to find a separating κ of polysize in E, O. Indeed, let K be the maximal k in (5) over all D ∈ E-. If the depth n of κ is ≤ K, we are done. If n > K, we shorten κ as follows. Consider the prefix κ′ of κ formed by ρ0, . . . , ρK. If JD ̸|= κ′ (0) for all D ∈ E-, we are done. Otherwise, for each D ∈ E-, we pick a ρi, i > K, with ρi ̸⊆ tpk+j for any j ≤ l; it must exist as JD ̸|= κ(0). Then we construct κ′′ by omitting from κ all ρl that are different from those in κ′ and the chosen ρi with i > K. Clearly, κ′′ is as required.

A Σp2 -algorithm guesses κ and JD, for D ∈ E-, and checks in polytime that JD |= O,D and JD ̸|= κ(0) and in CONP [Ono and Nakamura, 1980] that O,D |= κ(0) for all D ∈ E+. The lower bound is shown by reduction of the validity problem for fully quantified Boolean formulas ∃p ∀q ψ, where p = p1, . . . , pk and q = q1, . . . , qm are all propositional variables in ψ. We can assume that ψ is not a tautology and ¬ψ ̸|= x for x ∈ {pi, ¬pi, qj, ¬qj | i ≤ k, j ≤ m}. Let E = (E+, E-) with E+ = {D1, D2}, E- = {D3}, where D1 = {B1(0)}, D2 = {B2(0)}, D3 = {q1(0), . . . , qm(0)}, and let O contain the following axioms with fresh atoms B1,B2,Ai, ¯ Ai, for i = 1, . . . , k:

Then ∃p ∀q ψ is valid iff E is Qp[✸]-separable under O.

We obtain the NP upper bounds in data complexity using the same argument as for the Σp2 -upper bound and observing that checking O,D |= κ(0) is in P in data complexity. The NP lower bounds are inherited from the ontologyfree case. The proof of the P upper bounds is more involved. We illustrate the idea for O with arbitrary Boolean but without temporal operators. In this case, one can show (which is non-trivial) that O,D |= κ(0) iff IO,D |= κ(0), where IO,D is the completion of D: it contains A(ℓ) iff O∪{B | B(ℓ) ∈ D} |= A. For example, if O = {A∨B} and D = {A(1),B(1),A(3),B(3)}, the completion IO,D is just D regarded as an interpretation (so IO,D does not have to be a model of O). It can be constructed in polytime in D and, due to the equivalence above, used to prove the P upper bounds using dynamic programming. That equivalence does not hold for LTL ✷✸ , 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 ⃝,✸- queries. For example, O,D |= ✸(A ∧ ⃝B) for D and O defined above, and so the equivalence does not hold. In fact, the complexity of separability by ⃝✸-queries remains open.

7 QBE with LTL-Ontologies

For ontologies with arbitrary LTL-axioms, we obtain:

Theorem 14. (i) QBE(LTL,Q) is in 2EXPTIME, for any Q ∈ {Q[✸],Q[⃝,✸],Q[Us] }. (ii) QBE(LTL,Q) is in 2EXPSPACE, for any Q ∈ { Qp[✸], Qp[⃝, ✸], Qp[U] }.

The proof requires a further modification of the transition systems Si in Theorem 6. We illustrate it by an example. Let O = {A → ✸B, ⊤ → A ∨ B, A ∧ B → ⊥} with the set of O-types TO = {tp1 , tp2 , tp3 }, where tp1 = {A, ¬B,✸B}, tp2 = {¬A,B, ¬✸B}, tp3 = {A, ¬B, ¬✸B}, and tp4 = {¬A,B,✸B}, from which we omitted subformulas such as A ∨ B that are true or false in all types. For non-empty sets T 1, T 2 ⊆ T O and Γ ⊆ Σ⊥, we take the relation T 1 →Γ T 2, which, intuitively, says that if there are instants nI in all models I of O,D such that {tpI (nI) | I |= O,D} = T1, then there exist mI > nI with {tpI (mI) | I |= O, D} = T 2 and Γ = {A ∈ Σ⊥ | I,m |= A for all I and nI < m < mI}. In our example, we have {tp1 , tp3 } →Σ⊥ {tp1 , tp2 , tp3 , tp4 } and {tp1 , tp3 } →{B} {tp1 , tp3 , tp4 } (among others). Then we construct the following transition system Si for, say, Di = {A(0)}, which reflects all Q[Us]-queries over O,Di using T ′ ⊆ TO as states (the initial state is {tp1 , tp3 } since A(0) ∈ Di):

The Si can be constructed in 2EXPTIME in |Di| + |O| (checking T1 →Γ T2, for given T1, T2 and Γ, can be done in EXPSPACE). Also, the product of the Si , for Di ∈ E+, can be constructed in 2EXPTIME in |Di| + |E+|.

8 Conclusions

We have started an investigation of the computational complexity of query-by-example for principal classes of LTLqueries, 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 U. For example, we still need to pinpoint the size of minimal separating Q[Us]- and Qp[U]-queries under a Horn ontology. The tight complexity of QBE for unrestricted 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'.

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.