We investigate the computational complexity of the containment problem for conjunctive queries given in linear temporal logic LTL with the operators 'eventually' and 'next-time'. We show that this problem is coNP-complete and identify a few restricted query classes for which containment is tractable (in LogSpace). Our concern in this paper is the containment problem for very basic temporal conjunctive queries that are built from atoms-propositional variables representing atomic events and ⊤-using conjunction and the temporal operators ○ (at the next moment) and ◇ (sometime later) from the linear temporal logic LTL. Such queries are supposed to be evaluated over data instances that consist of facts of the form (ℓ) stating that atomic proposition is true at time ℓ, for ℓ ∈ N. This setting is relevant to applications in numerous areas ranging from temporal databases and streams to temporal ontology-based data access, pattern matching and learning; see the Motivation and Related Work section below for some details and references. Using the fact that our queries correspond to tree-shaped conjunctive queries, it is readily seen that the query evaluation problem-given a query , a data instance , and a timestamp ℓ from the temporal domain of , decide whether is true at ℓ in the model determined by -is decidable in polynomial time (in the size of and ). The containment problem for these queries turns out to be more interesting. Recall that the query containment problem is to decide, given any queries and ′, whether, for every data instance , the answers to over are contained in the answers to ′ over . Our main result in this paper proves that query containment for our most expressive query language is non-tractable and coNP-complete. It is the hardness part of the result that is of interest while the upper bound is more or less straightforward. We also show that, for queries without ○ , containment is in the complexity class L (LogSpace); it is also in L for path queries with both ○ and ◇. As we are only considering queries that are existential LTL-formulas (without the operator 'always in the future'), the containment problem is equivalent to the validity of formulas of the form → ′ in finite or infinite temporal models. So, our results also contribute directly to the research problem of classifying fragments of LTL according to their computational complexity; see, e.g., [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]. Motivation and Related Work. Temporal data is ubiquitous in the digital world, and there are numerous applications having our non-relational propositional LTL-queries as a core. For example, temporal variants of SQL tailored to efectively retrieve information from temporal databases rely on LTL-operators [11, 12]. In ontology-based data access (OBDA), temporal conjunctive formulas are often
utilised as a core user-friendly language to formulate both queries and ontology rules; see, e.g., [13] and further references therein as well as more recent [14, 15, 16]. Another recent application of LTL-queries is extraction of (or learning) patterns from temporal data examples [17]. In this setting, conjunctive
studied in [18, 19, 20, 21]. Note also that there is a close link between evaluating path queries and algorithms for finding patterns in strings [ 22, 23], a problem having multiple applications such as DNA analysis in bioinformatics.
Query containment was shown to be NP-complete for standard database conjunctive queries by reduction to query evaluation in the seminal work [24]. Since then query containment has been studied for numerous query languages. Most closely related is work on containment for fragments of XPath [25] and query containment over trees [26]. In these languages, similar to our work, queries can refer to nodes reachable along the transitive closure of a successor relation. Very diferent techniques are used, however, since we assume a linear order instead of a tree. Our results are also closely related to the work on subsumption in extensions of ℰ ℒ. Observe that our queries are notational variants of ℰ ℒ-concepts with two roles (one corresponding to ○ and the other to ◇). Hence, subsumption between ℰ ℒ concepts over interpretations, in which one role is interpreted as the transitive closure of another role, corresponds exactly to query containment in our language, except that arbitrary interpretations (equivalently, by unfolding, tree-shaped ones) are considered, and not linear orders. In [27], coNPhardness is shown for subsumption in ℰ ℒ with transitive closure using the technique introduced for
Temporal data instances. By a temporal data instance we mean here any finite set ̸= ∅ of facts of
the form (ℓ), where is a propositional variable, henceforth called an atom, and ℓ ∈ N. Intuitively,
(ℓ) says that event happened at time instant ℓ. The signature sig() of is the set of atoms
occurring in it. The maximal time ℓ in is denoted by max . Where convenient, we also write
as the word 0 . . . max over the alphabet 2sig() with = { | () ∈ } for each ≤ max . By
definition, max ̸= ∅. For example, the data instance = {(
0
1
,
2
3
4
Temporal conjunctive queries. To query data instances, we employ LTL-formulas that are built
from atoms and the logical constant ⊤ using conjunction ∧ and the unary temporal operators ○ (next
time) and ◇ (sometime in the future). We consider the following classes of queries:
[○ ◇]: all ○ ◇-queries (that is, all queries in our language);
[◇]: all ◇-queries (that is, ○ ◇-queries not containing ○ );
[○ ◇]: path ○ ◇-queries, that is, ○ ◇-queries of the form
= 0 ∧ 1(︀ 1 ∧ 2( 2 ∧ · · · ∧ −1 ( −1 ∧ )))︀ ,
(
The truth-relation , ℓ |= , saying that a query is true in at any moment ℓ ∈ N, is defined as usual in temporal logic under the strict semantics; see, e.g., [28, 29] and further references therein: , ℓ |= ⊤, , ℓ |= ○ ′ if , ℓ + 1 |= ′, , ℓ |= if (ℓ) ∈ , , ℓ |= ◇′ if , |= ′, for some > ℓ.
, ℓ |= ′ ∧ ′′ if , ℓ |= ′ and , ℓ |= ′′, An answer to a query over a data instance is any ℓ such that 0 ≤ ℓ ≤ max and , ℓ |= . The temporal depth tdp() of is the maximum number of nested temporal operators in ; the size || of is the number of symbols in it.
Note that there is a close link between evaluating path queries and algorithms for finding patterns in
strings [23]. A sequence is a data instance = 0 . . . with 0 = ∅ and | | = 1, for 0 < ≤ . A
sequence query is a path query of the form (
We write |= ′ if , 0 |= implies , 0 |= ′ for all , and ≡ ′ if |= ′ and ′ |= , in which
case and ′ are called equivalent. For example, for any query , we have ◇○ ≡ ○ ◇ ≡ ◇◇ ≡
◇(⊤ ∧ ◇). It follows that every [○ ◇]-query is equivalent to a query of the form (
A query ∈ [◇] is in normal form if = ∧ 1 ∧ · · · ∧ , where is a conjunction of atoms and each , for = 1, . . . , , is a [◇]-query (in normal form) that starts with ◇. Again, every ∈ [◇] can be converted to normal form in L using the equivalence
0 ∧ ◇( 1 ∧ ⋀︁ ◇) ≡ =1
0 ∧ ⋀︁ ◇( 1 ∧ ◇).
=1 For example, ◇( ∧ ◇ ∧ ◇) ≡ ◇( ∧ ◇) ∧ ◇( ∧ ◇).
A query ∈ [○ ◇] is in normal form if = ∧ 1 ∧ · · · ∧ , where is a [○ ]-query—that is, a ◇free [○ ,◇]-query—and each takes the form ◇(1, ∧◇(2, ∧· · ·∧◇ ,)) with [○ ]-queries ,, for = 1, . . . , . Each ∈ [○ ◇] can be converted to normal form in polytime using the equivalence above, ○ ◇ ≡ ◇ ○ and ○ ( ∧ ′) ≡ ( ○ ∧ ○ ′). For example, ○ (○ ∧ ◇○ ( ∧ ◇○ ∧ ◇)) ≡ ○ 2 ∧ ◇(○ 2 ∧ ◇○ 3 ∧ ◇○ 2)) ≡ ○ 2 ∧ ◇(○ 2 ∧ ◇○ 3) ∧ ◇(○ 2 ∧ ◇○ 2).
1 = ◇( ∧ ∧ ○ ), 2 = ◇( ∧ ∧ ○ ), ′ = ◇︀( ∧ ◇( ∧ ))︀ .
It is readily seen that 1 ̸|= ′ (as the data instance ∅{, }{} makes 1 true at 0 but not ′) and 2 ̸|= ′. However, for the [○ ◇]-query 1 ∧ 2, we have 1 ∧ 2 |= ′. To show this, we observe that any data instance = 0 . . . satisfying 1 ∧ 2 at has ⊇ {, } , +1 ⊇ {} , ⊇ {, } , +1 ⊇ {} , for some < , < . In each of the three cases, < , = , and > , we have , |= ′.
Theorem 1. The query containment problems for [○ ◇], [◇] and their subclasses are all in L.
takes the form (
For any ∈ N, we denote by [] the closed interval [0, ] ⊆ N . A function ℎ : [] → [] is monotone if ℎ() < ℎ() whenever < . A monotone function ℎ : [] → [] is called a containment witness for and ′ if the following conditions hold:
ℎ(), for all ∈ []; – if < and ′+1 = ○ , then ℎ(+1) = ○ and ℎ( + 1) = ℎ() + 1.
Note that checking the existence of a containment witness can be done in L in || and |′|. Indeed, consider first the case of [◇]-queries. It is easily seen that a containment witness for and ′ exists if there is a sequence of pairs (0, 0), . . . , (, ), where 0 = 0 and +1 is the minimal number > such that ′+1 ⊆ . For [○ ◇]-queries, we need a more involved procedure that relies, however, on the same idea. Let 0′ ≥ 0 be the minimal index such that ′0′+1 = ◇ (it follows that ′1 = · · · = ′′ = ○ ). If no such 0′ exists, we set 0′ = . We check if 1 = · · · = 0′ = ○ and 0 ′0 ⊆ 0, . . . , ′0′ ⊆ 0′ . If this is not the case, a containment witness does not exist. If this is the case and 0′ = , a containment witness exists. Otherwise, let 1′ ≥ 0 be the minimal number such that ′0′+1+1′+1 = ◇. If no such 1′ exists, we chose 1′ such that 0′ + 1 + 1′ = . We find the minimal 0 > 0′ such that 0+1 = · · · = 0+1′ = ○ and ′0′+1 ⊆ 0 , . . . , ′0′+1+1′ ⊆ 0+1′ . If such 0 does not exist, a containment witness does not exist. If such 0 exists and 0′ + 1 + 1′ = , a containment witness exists. Otherwise, we proceed to find 2′ ≥ 0 and 1 > 0 that satisfy the conditions analogous to the above. We proceed until we either decide that a containment witness does not exist, or there ipsroacneidtuerraetsiotonps wathtehniswiteercahtoioons.e ′ ≥ 0 such that 0′ + 1 + 1′ + 1 + · · · + ′−1 + 1 + ′ = . Our
Lemma 1. For any , ′ ∈ [○ ◇] in normal form, we have |= ′ if there is a containment witness for and ′.
function : [] → [max ] such that, for all ∈ [], we have (0) = 0, ⊆ { | ( ()) ∈ } , and if +1 = ○ , then ( + 1) = () + 1. It follows directly from the definition of the truth-relation that , 0 |= if there exists a satisfying function for in .
Suppose ℎ is a containment witness for and ′. Take any data instance with , 0 |= . Let be a satisfying function for in . Then it is readily checked that the composition ℎ : [] → [max ] is a satisfying function for ′ in , and so , 0 |= ′. It follows that |= ′.
Conversely, suppose |= ′. We define a containment witness for and ′ by induction on the temporal depth tdp(′) of ′. If tdp(′) = 0, then ′ = ′0 and ′0 ⊆ . It follows that ℎ(0) = 0 is the required containment witness. As an induction hypothesis (IH), we assume next that there is a containment witness for any queries 1 and 2 such that 1 |= 2 and tdp(2) < tdp(′). Two cases are possible.
Case 1: ′1 = ○ . Let > 0 be the maximal index such that ′1 = · · · = ′ = ○ . Then ′ ̸= ⊤ (because ′ is in normal form) and ′+1 = ◇ if > . Let be the minimal index such that 0 ∧ 1(︀ 1 ∧ 2( 2 ∧ · · · ∧ )︀) |= ′0 ∧ ′1(︀ ′1 ∧ ′2(︀ ′2 ∧ · · · ∧ ′ ′)︀) .
We claim that, for all ≤ , we have = ○ , ⊇ ′, and so = . Indeed, if there is ≤ with = ◇, then we take the data instance = 0 . . . −1 ∅ . . . and obtain , 0 |= and , 0 ̸|= ′, contrary to |= ′. And if there is ≤ with ̸⊇ ′, then we take the data instance = 0 . . . and again obtain , 0 |= and , 0 ̸|= ′.
+1 = +1( +1 ∧ · · · ∧ ), ′+1 = ′+1( ′+1 ∧ . . . ′ ′) and observe that |= ′ implies +1 |= ′+1. As tdp(′+1) < tdp(′), the IH gives a containment witness ℎ′ for +1 and ′+1. Using it, we define the required containment witness ℎ for and ′ by taking ℎ() = , for all ≤ , and ℎ( + ) = ℎ ′() + , for all with 1 ≤ ≤ − .
Case 2: ′1 = ◇. Suppose first that there is a minimal initial subquery
¯′ = ′0 ∧ ′1( ′1 ∧ · · · ∧ ′ ′) of ′ such that ′ ̸= ⊤, ′+1 = ◇ and > 0. Let ¯ = 0 ∧ 1( 1 ∧ · · · ∧ ) be the minimal initial subquery of with ¯ |= ¯′. As tdp(¯′ ) < tdp(′), the IH gives a containment witness ℎ0 for ¯ and ¯′.
As ′ ̸= ⊤ and is minimal, ℎ0() = . By IH, our claim also holds for ′+1 = ′+1( ′+1∧· · ·∧ ′ ′) and +1 = +1( +1 ∧ · · · ∧ ) and gives a containment witness ℎ1 for +1 and ′+1. We then obtain a containment witness for and ′ by concatenating ℎ0 and ℎ1.
Finally, suppose that there is no ′ ̸= ⊤ with ′+1 = ◇ and > 0. Then ′ takes the form ′0 ∧ ◇(︀ ′ ∧ ′+1 ′+1 · · · ∧ ′ ′)︀) , where > 0, ′ ̸= ⊤, and ′+1 = · · · = ′ = ○ . We claim that there exists ≥ such that +1 = · · · = +− = ○ and +ℓ ⊇ ′+ℓ, for all ℓ with 0 ≤ ℓ ≤ − , which clearly implies the existence of a containment witness for and ′. To prove this claim, suppose there is no such . Consider the data instance = 01 1 . . . , where = (the empty word) if = ○ , and = ∅ if = ◇. Then , 0 |= but , 0 ̸|= ′, contrary to |= ′. ⊣
Lemma 2. If = ∧ 1 ∧ · · · ∧ ∈ [◇] is in normal form and ′ ∈ [◇], then |= ′ if ∧ |= ′, for some , 1 ≤ ≤ .
To illustrate, consider the queries 1 and 2 from Example 1, in which we replace ○ by ◇, and ′. It is easy to see that 1 ̸|= ′, 2 ̸|= ′, and so 1 ∧ 2 ̸|= ′. To check the latter, consider = ∅{, }{}{}, which satisfies ∧ from 1 and 2 at the same time instant, and then from 1 and from 2 at diferent time instants.
Proof. (⇒) Suppose that ′ = 0 ∧ ◇︀( 1 ∧ ◇( 2 ∧ · · · ∧ ◇ ))︀ , = ◇︀( 1 ∧ ◇( 2 ∧ · · · ∧ ◇ ))︀ , for 1 ≤ ≤ , and |= ′. Note that ⊇ 0 as otherwise ̸|= ′. For each , 1 ≤ ≤ , we define inductively a function
: {1, . . . , } → {1, . . . , } ∪ {∞}.
To begin with, we set (
⋃︁ 1≤≤, (ℓ)<∞ where ℓ, = min{, (ℓ+1)−1} , for 1 ≤ ≤
(ℓ + 1) = ∞. It follows immediately from the definition that if there is ≤ such that () < ∞, then ∧ |= ′, as required. So suppose there is no such ≤ and derive a contradiction by proving that in this case ̸|= ′.
Let ′ ≤ be minimal such that (′) = ∞ for all ≤ . Consider the data instance 1 =
11 . . . 11 . . . 1 . . . , where = min{, (
(ℓ)+1 . . . = 1 12 2 . . . ′−1 ′ .
It follows from the construction that , 0 |= and , 0 ̸|= ′, contrary to |= ′.
Theorem 2. The query containment problem for [○ ◇] is coNP-complete.
Proof. To show the upper bound, suppose we are given two queries , ′ ∈ [○ ◇] in normal form, where ⊣ ⊣ = ∧ 1 ∧ · · · ∧ with = ◇︀( ,1 ∧ ◇(,2 ∧ · · · ∧ ◇ , )︀) ,
, , ∈ [○ ], for = 1, . . . , , = 1, . . . , , ′ = ′ ∧ ′1 ∧ · · · ∧ ′′ with ′ = ◇︀( ′
,1 ∧ ◇(′,2 ∧ · · · ∧ ◇ ′,′ )︀) , ′, ′, ∈ [○ ], for = 1, . . . , ′, = 1, . . . , ′.
By definition, ̸|= ′ if there exist a data instance and some , 1 ≤ ≤ ′, such that |= and ̸|= ′ ∧ ′. Our aim is to show that it sufices to consider with max ≤ (||| ′|). If this is the case, then an obvious NP-algorithm deciding ̸|= ′ would be to guess such and with sig() = sig() ∪ sig(′), and then check in polytime whether |= and ̸|= ′ ∧ ′.
So, suppose we have |= and ̸|= ′ ∧ ′, for some and . As |= , for each , there is a satisfying function in , which is a monotone function : [1, ] → [max ] such that, for all ∈ [1, ], we have ()()+1 . . . ()+tdp(,) |= , . Let , = [(), () + tdp(, )], for ∈ [1, ] and ∈ [1, ]. We may clearly assume that = ∅, for all ∈ [max ] with ∈/ ⋃︀=1 ⋃︀=1 , ∪ [tdp()]. Now, we cut certain segments from maintaining the property that the resulting data instance ′ makes true and ′ ∧ ′ false at time 0.
Suppose there exist , and ′,′ such that ′ (′) − ︀( () + tdp(, )︀) > tdp(′) and (︀ () + tdp(, ), ′ (′))︀ ∩ , = ∅, for all ∈ [1, ] and ∈ [1, ]. Then we remove from the segment ()+tdp(,)+1 . . . ′ (′)−1 of all with > () + tdp(, ) + tdp(′) + 1. By definition, the removed are all empty. The resulting shorter instance ′ is such that ′ |= and ′ ̸|= ′ ∧ ′. Indeed, we have kept all the witnesses that make ′ |= intact. Now, suppose ′ |= ′ ∧ ′. We take the satisfying function ′ for ′ in ′ and modify it to construct ′′ such that ′′() = ′(), for all ∈ [1, ′] with ′() ≤ ()+tdp(, ), and ′′() = ′()+ℓ, for all with ′() ≤ ()+tdp(, ), where ℓ is the number of the that were removed from the segment ()+tdp(,)+1 . . . ′ (′)−1 . It is readily seen that ′′ is a satisfying function for ′ in , which is a contradiction. Thus, ′ ̸|= ′ ∧ ′.
By performing this operation for all suitable , and ′,′ , we obtain a data instance with at most ∑︁ 1≤≤, 1≤≤
tdp() + 1 + (tdp(, ) + 1) +
∑︁ (tdp(′, ) + 1) 1≤≤ ′ time instants, where is the number of , in plus 1.
The matching lower bound is shown by reduction of the 3SAT problem to the complement of the [○ ]-queries , for all = 0, . . . , , and a [○ ◇]-query ′ such that containment problem for [○ ◇]. Suppose we are given a 3CNF = 1 ∧ · · · ∧ with clauses and variables 1, . . . , such that no contains both and ¬ , for any . Our aim is to construct is satisfiable if
⋀︁ ◇ ̸|= ◇′.
0≤≤
(
ℓ = ∖ { ℓ}, for a literal ℓ over 1, . . . , , over the alphabet 2 that represent 0 ∧ ○ ︀( 1 ∧ ○ ( 2 ∧ · · · ∧ ○ )︀) . Namely, we set Let = { 1, ¯ 1, . . . , ¯ , , }. We define the [○ ]-queries as words of the form 0 1 2 . . . 0 = {}∅ 2−1 1 . . . ∅ 2{},
and = ,1,2,3{}, for = 1, . . . , , where the substrings ,, for = 1, 2, 3, of are defined as follows: if = ℓ1 ∨ ℓ2 ∨ ℓ3 , then , = 1 . . . −1 ℓ +1 . . . .
Thus, the length of each word , for = 1, . . . , , is 3 + 2, and so the temporal depth of the corresponding queries is 3 + 1. The length of 0 is 5 + 2. Finally, we set
′ = ∧ ○ 2◇( ∧ ○ 2◇). use the queries ◇).
Example 2. Consider the 3CNF = 1 ∧ 2 with 1 = 1 ∨ ¬2 ∨ 4, 2 = 1 ∨ ¬3 ∨ ¬4, = 2
and = 4. The words 0, 1, 2 for are illustrated in the picture below, where the numbers indicate
the positions of the respective characters, starting from 1, and ∅ is omitted (remember that, in (
. For each clause = ℓ1 ∨ ℓ2 ∨ ℓ3 in , fix some ∈ {1, 2, 3} such that the literal ℓ is true under a. Denote by () the th character in the word (see Example 2). Define a data instance by taking, for all ∈ and ≤ 5 + 2, () ∈ if ∈ 0() or ∈ ( − (3 − )), for some ∈ [1, ].
∅-characters to make 1 in 0 aligned with the first character of the substring , in and then taking the union of the characters in the aligned positions of the resulting words and 0. Example 3. Consider again the 3CNF from Example 2 and the satisfying assignment a that make 3 false and all the other variables true. Let 1 = 3 and 2 = 2. In this case, the data instance looks as follows: 0 1 2 3 4 1 1 2 3 4 1 ¬2 3 4 1 2 3 4 2 1 2 3 4 1 ¬3 3 4 1 2 3 ¬4 0 1 2 3 4 5 6 7 8
Returning to the proof of (⇒), we see that , 1 |= 0 and , 1 + (3 − ) |= follow immediately from the definitions, which gives |= ⋀︀0≤≤ ◇. It also follows from the definitions that |= ◇′ if , |= , for some ∈ [2 + 2, 3 + 1]. Thus, |= ◇′ would imply that , 2 + 1 + |= , for some ∈ [1, ], and so there must exist distinct , ∈ [1, ] such that , and , have and ¬ at position , respectively. But this is impossible as, by the choice of and , the assignment a should make both and ¬ true.
(⇐) Assuming ⋀︀0≤≤ ◇ ̸|= ◇′, we take a data instance with |= ⋀︀0≤≤ ◇ and ̸|= ◇′. Let be the minimal number such that , |= . Observe that ≥ 0 for all ∈ [1, ], as otherwise we would have |= ◇′. For the same reason and because ∈ , we must have ≤ 0 + 2 (see the picture in Example 2 for an illustration). Moreover, there are only three possibilities for , namely, ∈ {0, 0 + , 0 + 2}. Indeed, suppose otherwise. Then > 1 and ∈ [0, 0 + 2] ∖ {0, 0 + , 0 + 2}, and so , 0 + 2 + 1 |= , which implies |= ◇′. It follows that, for each ∈ [1, ], we have either , 0 + 2 + 1 |= ,1 or , 0 + 2 + 1 |= ,2 or , 0 + 2 + 1 |= ,3. Let = be such that , 0 + 2 + 1 |= , (if there are several such , we can take the minimal one).
Consider the assignment a that makes false if has a clause = ℓ1 ∨ ℓ2 ∨ ℓ3 with ℓ = ¬, and true otherwise. We show that, for each = ℓ1 ∨ ℓ2 ∨ ℓ3 in , the literal ℓ is true under a. This is clearly the case if ℓ = ¬. So, suppose ℓ = . By definition, a makes true if there is no ′ = ℓ1′ ∨ ℓ2′ ∨ ℓ3′ with ℓ′′ = ¬. Suppose, on the contrary, that such a ′ exists. By the choice of and ′ , it follows that , 0 + 2 + 1 |= , and , 0 + 2 + 1 |= ′,′ . But then , 0 + 2 + |= , and so |= ◇ ′, which is a contradiction. ⊣
We have shown that the containment problem for the classes [○ ◇] and [◇] of LTL-queries lies in the complexity class L. It would be of interest to understand if this complexity bound is tight or the problem is easier, e.g., in NC1. As observed earlier, unlike first-order conjunctive queries but similarly to XPath-queries and queries with transitive roles, [○ ◇]-query containment is not polytime reducible to query evaluation (unless P = NP). However, it follows from the proofs above that, for [○ ◇] and [◇], containment is polytime reducible to evaluation, although the reduction is less trivial than in the ifrst-order case. It is also worth noting that a polysize witness for non-containment exists for all of our queries, similarly to some classes of XPath/transitive queries [25].
In this paper, we have not considered conjunctive queries with the until-operator U, for which containment is only known to be in PSpace. Natural restricted fragments of conjunctive path-queries with U that only allow conjunctions of atoms on the left-hand side of U have been identified in [ 20, 19]; however, the complexity of containment for those fragments have not been studied yet. For path-Uqueries satisfying the restriction above, the existence of a polysize witness for non-containment was shown in [19, Theorem 9]. This fact implies a coNP upper bound for containment, but it is not known whether this bound is tight.
[13] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Ontologymediated query answering over temporal data: A survey (invited talk), in: S. Schewe, T. Schneider,
2017, October 16-18, 2017, Mons, Belgium, volume 90 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, pp. 1:1–1:37. URL: https://doi.org/10.4230/LIPIcs.TIME.2017.1. doi:10.4230/ LIPIcs.TIME.2017.1. [14] S. Brandt, E. G. Kalayci, V. Ryzhikov, G. Xiao, M. Zakharyaschev, Querying log data with metric temporal logic, J. Artif. Intell. Res. 62 (2018) 829–877. URL: https://doi.org/10.1613/jair.1.11229. doi:10.1613/jair.1.11229. [15] D. Wang, P. Hu, P. A. Walega, B. C. Grau, Meteor: Practical reasoning in datalog with metric temporal operators, in: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty
Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, AAAI Press, 2022, pp. 5906–5913. URL: https://doi.org/10.1609/aaai.v36i5.20535. doi:10.1609/AAAI.V36I5.20535. [16] A. Kurucz, V. Ryzhikov, Y. Savateev, M. Zakharyaschev, Deciding fo-rewritability of regular languages and ontology-mediated queries in linear temporal logic, J. Artif. Intell. Res. 76 (2023) 645–703. URL: https://doi.org/10.1613/jair.1.14061. doi:10.1613/JAIR.1.14061. [17] D. Neider, R. Roy, What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications, Springer Nature Switzerland, Cham, 2025, pp. 109–125. URL: https://doi.org/10. 1007/978-3-031-75778-5_6. doi:10.1007/978-3-031-75778-5_6. [18] R. Raha, R. Roy, N. Fijalkow, D. Neider, Scalable anytime algorithms for learning fragments of linear temporal logic, in: D. Fisman, G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer International Publishing, Cham, 2022, pp. 263–280. [19] M. Fortin, B. Konev, V. Ryzhikov, Y. Savateev, F. Wolter, M. Zakharyaschev, Unique characterisability and learnability of temporal instance queries, in: G. Kern-Isberner, G. Lakemeyer,
https://proceedings.kr.org/2022/17/. [20] M. Fortin, B. Konev, V. Ryzhikov, Y. Savateev, F. Wolter, M. Zakharyaschev, Reverse engineering of temporal queries mediated by LTL ontologies, in: Proceedings of the Thirty-Second International
ijcai.org, 2023, pp. 3230–3238. URL: https://doi.org/10.24963/ijcai.2023/360. doi:10.24963/IJCAI. 2023/360. [21] J. C. Jung, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Extremal separation problems for temporal instance queries, in: Proceedings of the Thirty-Third International Joint Conference on Artificial
https://www.ijcai.org/proceedings/2024/382. [22] C. Fraser, Consistent subsequences and supersequences, Theor. Comput. Sci. 165 (1996) 233–246.
URL: https://doi.org/10.1016/0304-3975(95)00138-7. doi:10.1016/0304-3975(95)00138-7. [23] M. Crochemore, C. Hancart, T. Lecroq, Algorithms on strings, Cambridge University Press, 2007. [24] A. Chandra, P. Merlin, Optimal implementation of conjunctive queries in relational data bases, in: Conference Record of the Ninth Annual ACM Symposium on Theory of Computing, 2-4 May 1977, Boulder, Colorado, USA, ACM, 1977, pp. 77–90. [25] G. Miklau, D. Suciu, Containment and equivalence for an xpath fragment, in: L. Popa, S. Abiteboul,
on Principles of Database Systems, June 3-5, Madison, Wisconsin, USA, ACM, 2002, pp. 65–76.
URL: https://doi.org/10.1145/543613.543623. doi:10.1145/543613.543623. [26] H. Björklund, W. Martens, T. Schwentick, Conjunctive query containment over trees, J. Comput.
Syst. Sci. 77 (2011) 450–472. URL: https://doi.org/10.1016/j.jcss.2010.04.005. doi:10.1016/J.JCSS. 2010.04.005. [27] C. Haase, C. Lutz, Complexity of subsumption in the el family of description logics: Acyclic and cyclic TBoxes, in: M. Ghallab, C. D. Spyropoulos, N. Fakotakis, N. M. Avouris (Eds.), ECAI 2008 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings, volume 178 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2008, pp. 25–29. URL: https://doi.org/10.3233/978-1-58603-891-5-25. doi:10.3233/978-1-58603-891-5-25. [28] D. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-Dimensional Modal Logics: Theory and
[29] S. Demri, V. Goranko, M. Lange, Temporal Logics in Computer Science, Cambridge Tracts in