Extremal Separation Problems for Temporal Instance Queries

1 Introduction

The separation (aka fitting or consistency) problem for a class Q of queries is to find some q ∈ Q that separates a given set E = (E+,E-) of positive and negative data examples in the sense that D |= q for all D ∈ E+, and D ̸|= q for all D ∈ E-. Separation underpins the query-by-example approach, which aims to support database users in constructing queries and schema mappings with the help of data examples [Alexe et al., 2011; Martins, 2019], inductive logic programming [Cropper et al., 2022], and, more recently, automated feature extraction, where separating queries are proposed as features in classifier engineering [Kimelfeld and R´e, 2018; Barcel´o et al., 2021]. Separating queries (and, more generally, formulas) also underpin recent logic-based approaches aiming to explain positive and negative data examples given by applications [Sarker et al., 2017; Camacho and McIlraith, 2019; Raha et al., 2022].

The space of all separating queries, denoted s(E, Q), forms a convex subset of Q under the containment (or logical entailment) relation q |= q′ between queries q, q′ , and is an instance of the more general version spaces [Mitchell, 1982]. If finite, s(E,Q) can be represented by its extremal elements: the most specific (logically strongest) and most general (logically weakest) separators in Q. In fact, many known algorithms check the existence of separators by looking for a most specific one [ten Cate and Dalmau, 2015; Barcel´o and Romero, 2017; Guti´errez-Basulto et al., 2018; Funk et al., 2019]. This is not surprising as query classes are often closed under ∧, and so the conjunction of all separators gives the unique most specific one. Dually, the unique most general separator is given by the disjunction of all separators if the query class is closed under ∨, which is a less common assumption. For the case of first-order queries constructed using ∧ and existential quantifiers (conjunctive queries or CQs), a systematic study of extremal separation has recently been conducted in the award winning [ten Cate et al., 2023].

Here, we study extremal separation for temporal instance queries. Data instances take the form (δ0, . . . , δn) describing temporal evolutions, where the δi are the sets of atomic propositions that are true at time i. Queries are formulated in the fragment of linear temporal logic LTL with the operators ∧, ⃝ (next), and ✸ (eventually). These ⃝✸- queries and its subclass of ✸-queries without ⃝, are obtained by restricting CQs to propositional temporal data and form the core of most temporal query languages proposed in the database and knowledge representation literature [Chomicki and Toman, 2018; Baader et al., 2015; Borgwardt et al., 2015; Artale et al., 2021]. We are particularly interested in subclasses of the classes of ⃝✸-and ✸-queries that are not closed under ∧ and take the form of path queries:

with oi ∈ {⃝,✸} and conjunctions ρi of atoms. The temporal patterns expressed by path queries correspond to common subsequences, subwords, and combinations thereof, which have been investigated in the string pattern matching literature for more than 50 years. Their applications range from computational linguistics to bioinformatics and revision control systems [Bergroth et al., 2000; Chowdhury et al., 2010; Abboud et al., 2015; Blum et al., 2021]. In fact, our results can also be interpreted and applied in that research tradition and our techniques combine both logic and automata-based methods with pattern matching. We note that not admitting ∨ in our query languages is crucial for finding this type of patterns and adding it would often trivialise separation.

Example 1. Suppose the first two sequences of events shown below are 'positive', the third one is 'negative', and our task is to explain this phenomenon using path queries. The space of

possible explanations includes q1 = ✸(A ∧ ⃝(B ∧ ⃝C)), q2 = ✸(A ∧ ⃝⃝C) and q3 = ✸(B ∧ ⃝C), all of which are true at 0 in the positive examples and false in the negative one. In fact, q1 is the unique most specific explanation, while q2 and q3 are the non-equivalent most general ones. On the other hand, there exists no explanation in terms of ✸ only.

The (bounded-size) separator existence problem for various classes Q of LTL-queries has recently been studied in [Fijalkow and Lagarde, 2021; Raha et al., 2022; Fortin et al., 2023]. Our aim here is to investigate systematically the separator spaces s(E,Q) by determining the complexity of verifying and counting most specific and general separators and giving algorithms computing them. On our way, we determine the complexity of entailment (aka containment in database theory) between queries and computing weakening and strengthening frontiers, which are the key to understanding s(E,Q). Intuitively, a weakening/strengthening frontier of q ∈ Q is a set of queries properly weaker/stronger than q that form a boundary between q and all of its weakenings/strengthenings in Q.

In detail, we first prove that query containment is in P for the class of ✸-queries and all of our classes of path queries. Based on this result, we show that strengthening and weakening frontiers can be computed in polytime for path queries. This is also the case for ✸-queries and weakening frontiers but not for strengthening ones. It follows that checking whether a path query is a most specific/general separator and whether a ✸-query is a most general one are both in P. In contrast, we establish CONP-completeness of checking whether a ✸-query is a most specific separator and whether a path query is the unique most specific/general one. Using frontiers, we show for path queries that the existence of unique most specific/general separators is in the complexity class US (for which unique SAT is complete) and that counting the number of most general/specific separators is in ♯P. We show that these upper bounds are tight, sometimes using the rich literature on algorithms for sequences (e.g., longest common subsequences). Our lower bounds mostly require only a bounded number of atomic propositions and an unbounded number of either negative or positive examples.

These complexity results are complemented with algorithms for computing extremal separators in the majority of our query classes. The algorithms use a graph encoding of the input example set, associating (extremal) separators with certain paths in the graph. Complexity-wise, they are optimal, running in polytime if the number of examples is bounded and exponential time otherwise.

Omitted proofs can be found in [Jung et al., 2024].

1.1 RelatedWork

Being inspired by the investigation of extremal separation for first-order conjunctive queries (CQs) [ten Cate et al., 2023], our results turn out to be very different. For instance, while separability by CQs is NEXPTIME-complete and separating queries are exponential in the size of the examples (the extremal ones even larger), the extremal separation problems for LTL-queries are often complete for SAT-related complexity classes, with separating queries being of polynomial size. For work on separation in the query-by-example paradigm we refer the reader to [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] in the database context and to [Guti´errez-Basulto et al., 2018; Ortiz, 2019; Cima et al., 2021; Jung et al., 2022] in the context of KR.

Our contribution is also closely related to work on synthesising LTL-formulas that explain the positive and negative data examples coming from an application [Lemieux et al., 2015; Neider and Gavran, 2018; Camacho and McIlraith, 2019; Raha et al., 2022; Fortin et al., 2022; Fortin et al., 2023]. While concerned with separability of temporal data instances and, in particular, separability by LTL-formulas of small size, the separator spaces s(E,Q) themselves have not yet been investigated in this context.

2 Data and Queries in LTL

Fix some countably-infinite set of unary predicate symbols, called atoms. A signature, σ, is any finite set of atoms. A (temporal) data instance is any finite set D ̸= ∅ of facts A(ℓ) with an atom A and a timestamp ℓ ∈ N, saying that A happened at ℓ. The size |D| of D is the number of symbols in it, with the timestamps given in unary. Let maxD be the maximal timestamp in D. Where convenient, we also write D as the word δ0 . . . δmaxD with δi = {A | A(i) ∈ D}. Without loss of generality, we can assume that δi ̸= ∅, using placeholders ⊤(i) if needed. The signature sig(D) of D is the set of atoms occurring in it.

We query data instances by means of LTL-formulas, called queries, that are built from atoms (treated as propositional variables) and the logical constant ⊤ (truth) using ∧ and the temporal operators ⃝ (next time) and ✸ (sometime in the future). We consider the following classes of queries:

Q[⃝✸]: all ⃝✸-queries; Q[✸]: all ✸-queries (not containing ⃝); Qp[⃝✸]: path ⃝✸-queries of the form (1), where the conjunctions of atoms ρi are often treated as sets and the empty conjunction as ⊤; Qp[✸]: all path ✸-queries (not containing ⃝); Qin: interval-queries of the form (1) with ρ0 = ⊤, ρ1 ̸= ⊤, o1 = ✸, and oi = ⃝, for i > 1.

Queries in Qin single out an interval of a fixed length starting at some time-point ≥ 1; q1-q3 from Example 1 are in Qin. Qσ is the restriction of a class Q to a signature σ. The temporal depth tdp(q) of q is the maximum number of nested temporal operators in q. The signature sig(q) of q is the set of atoms in q; the size |q| of q is the number of symbols in it.

The truth-relation D, n |= q-saying that q is true in D at moment n ∈ N-is defined as usual in temporal logic under the strict semantics: D, n |= ⊤ for all n ∈ N; D, n |= A iff A(n) ∈ D; D, n |= ⃝q′ iff D, n + 1 |= q′ ; and D, n |= ✸q′ iff D,m |= q′ , for some m > n. A data instance D is called a positive example for a query q if D, 0 |= q; otherwise, D is a negative example for q. Checking whether D is a positive

(negative) example for our queries q can obviously be done in polytime in |D| and |q|.

We write q |= q′ if D, 0 |= q implies D, 0 |= q′ for all instances D, and q ≡ q′ if q |= q′ and q′ |= q, in which case q and q′ are equivalent. For example, for any query q, we have ✸⃝q ≡ ⃝✸q ≡ ✸✸q. It follows that every path query in Qp[⃝✸] is equivalent to a query of the form (1), in which ρn ̸= ⊤ and whenever ρi = ⊤, 0 < i < n, then oi = oi+1; in this case we say that q is in normal form. Unless indicated otherwise, we assume all path queries to be in normal form.

Sequences. There is a close link between evaluating path queries and algorithms for finding patterns in strings [Crochemore et al., 2007]. A sequence is a data instance D = δ0 . . . δn with δ0 = ∅ and |δi| = 1, for i > 0; a sequence query is a path query of the form (1) with |ρ0| = 0 and |ρi| = 1, for i > 0. Querying sequences using sequence queries corresponds to the following matching problems:

• for any sequence query q ∈ Qp[✸] of the form (1), we have D, 0 |= q iff ρ1 . . . ρm is a subsequence of D;
• for any sequence query q ∈ Qin of the form (1), we have D, 0 |= q iff ρ1 . . . ρm is a subword of D.

3 Query Containment

The query containment problem for a class Q of queries is to decide whether q |= q′ , for any given q, q′ ∈ Q. In contrast to conjunctive queries, where query containment is NPcomplete [Chandra and Merlin, 1977], query containment is tractable for the majority of query classes defined above:

Theorem 2. The query containment problems for Qp[⃝✸], Q[✸] (and their subclasses) are all in P.

To prove Theorem 2, suppose first that we are given two queries q, q′ ∈ Qp[⃝✸], where q takes of the form (1) and q′ = ρ′0 ∧ o′1 (ρ′1 ∧ · · · ∧ o′mρ′m). Denote by [m] the closed interval [0,m] ⊆ N. A function h: [m] → [n] is monotone if h(i) < h(j) whenever i < j. Then tractability of containment for path queries follows from the criterion below, which is proved in the appendix by induction on tdp(q′ ):

Lemma 3. Let q, q′ ∈ Qp[⃝✸]. Then q |= q′ iff there is a monotone function h: [m] → [n] such that h(0) = 0 and, for all i ∈ [m], we have ρ′i ⊆ ρh(i) and if o′i+1 = ⃝, then oh(i+1) = ⃝ and h(i + 1) = h(i) + 1.

We refer to any function h defined in Lemma 3 as a containment witness for the pair q, q′ ∈ Qp[⃝✸].

Suppose now q ∈ Q[✸]. As shown in [Fortin et al., 2022], we can convert q in polytime to an equivalent query in the normal form ρ ∧ q1 ∧ · · · ∧ qn, where ρ is a conjunction of atoms and each qi is in Qp[✸] and starts with ✸. Tractability of containment for Q[✸]-queries follows from:

Lemma 4. If q = ρ ∧ q1 ∧ · · · ∧ qn ∈ Q[✸] is in normal form, q′ ∈ Qp[✸] and q |= q′ , then there is qi, 1 ≤ i ≤ n, with ρ ∧ qi |= q′ .

Proof. In the detailed proof given in the appendix, we show that, assuming ρ ∧ qi ̸|= q′ for all i, we can convert the qi into a data instance D with D, 0 |= q and D, 0 ̸|= q′ . ⊣

For queries q ∈ Q[⃝✸], Lemma 4 does not hold:

Example 5. Let q = q1 ∧ q2 ∧ q3 ∧ q4, where

q1 = ✸(a ∧ ⃝((a ∧ b) ∧ ⃝a)),

q2 = ✸(b ∧ ⃝((a ∧ b) ∧ ⃝b)),

q3 = ✸(a ∧ ⃝((a ∧ b) ∧ ⃝b)),

q4 = ✸(a ∧ ✸(b ∧ ✸(a ∧ ✸(b ∧ ✸(a ∧ ✸b))))),

and q′ = ✸(b∧✸((a∧b)∧✸a)). Then q |= q′ but qi ̸|= q′ , for any i, 1 ≤ i ≤ 4.

At the moment, the question whether containment of Q[⃝✸]-queries is tractable remains open.

4 Example Sets and Separating Queries

An example set E is a pair (E+,E-) of finite sets E+ ̸= ∅ and E- of data instances. We say that a query q separates E if all D ∈ E+ are positive examples and all D ∈ Eare negative examples for q. Denote by s(E,Q) the set of queries in a class Q separating E and call E Q-separable if s(E,Q) ̸= ∅. Our general aim is to understand the structure of s(E,Q) for various important query classes Q.

We consider queries in Q modulo equivalence, not distinguishing between q ≡ q′ . In this case, the relation |= is a partial order on Q. For any q ∈ s(E, Q), we clearly have

• tdp(q) ≤min{maxD | D ∈ E+},
• sig(q) ⊆ ⋂{sig(D) | D ∈ E+},

so s(E,Q) is finite. We refer to the |=-minimal elements of s(E,Q) ̸= ∅ as most specific Q-separators of E and to the |=-maximal elements as most general Q-separators of E (modulo ≡); they comprise the sets mss(E,Q) and mgs(E,Q), respectively. If these sets are singletons, we call their only element the unique most specific and, respectively, unique most general Q-separator of E. Note that the former always exists if s(E, Q) ̸= ∅ and Q is closed under ∧.

Example 6. (i) Suppose D+ = {A(0),B(0),A(1),B(1)}, D- = {A(0)} and E = ({D+}, {D-}). The separator space s(E, Qp[✸]) is shown below as a Hasse diagram with arrows indicating the partial order |= (and ⊤, A /∈ s(E, Qp[✸])), so

⊤

the most general Qp[✸]-separators of E comprise the set mgs(E,Qp[✸]) = {B,✸A,✸B} and the unique most specific one is A ∧ B ∧ ✸(A ∧ B).

s(E, Qp[✸]) = {✸A, ✸B} = mss/mgs(E, Qp[✸]) but there is no unique most specific/general separator. In contrast, s(E,Q[✸]) = {✸A,✸B,✸A ∧ ✸B} has the unique most specific separator ✸A∧✸B but no unique most general one.

(iii) One can show that mss/mgs(E, Q) always contains a longest/shortest separator of E in Q (of largest/smallest temporal depth). To illustrate, let E = ({D+ 1 }, {D1 ,D2 ,D3 }),

Then mgs(E, Qp[✸]) = {B ∧ C, B ∧ ✸A, C ∧ ✸A}, where B ∧ C of depth 0 is the shortest separator of E in Qp[✸].

Our main concern is the following three algorithmic problems for query classes Q ⊆ Q[⃝✸] with input E and q ∈ Q:

most specific/general separator verification: decide

whether q is an element of mss(E, Q) / mgs(E, Q);

counting most specific/general separators: count the elements of mss(E, Q) / mgs(E, Q);

computing a most specific/general separator: construct some query in mss(E, Q) / mgs(E, Q).

We are particularly interested in deciding whether there is a unique most specific/general separator and computing it. To achieve our aims, we obviously should be able to decide whether q ∈ s(E,Q) (separator verification) and whether s(E,Q) ̸= ∅ (separator existence). As mentioned in Section 2, separator verification is in P. We are also interested in the case when the number of positive or negative examples in E is bounded. The table below summarises the complexities of separator existence for our query classes, where b+ / b-

means that |E+| / |E-| is bounded, and one can assume a bounded signature. Except for Qin, these results are shown in [Fortin et al., 2023]. The proofs use techniques developed for the longest common subsequence problem (given k > 0 and a set E+ of sequences, is there a sequence query in Qp[✸] of depth ≥ k that is a subsequence of all D ∈ E+; see Section 2) and separator existence for sequence queries in Qp[✸] [Maier, 1978; Fraser, 1996]. The NP-upper bound for Qin is trivial; the lower one follows from the proof of Theorem 21, and tractability for b+ is ensured by the observation that there are polynomially-many relevant intervals in the E+-examples.

This NP-lower bound shows that great care is needed when transferring techniques from the literature on algorithms for sequences to our framework as separability of example sets of sequences using sequence queries in Qin is easily seen to be in P even for unbounded example sets and signatures.

A key to the extremal separator problems above is the following notions of strengthening and weakening frontiers.

5 Strengthening andWeakening Frontiers

Let Q be a class of queries and q ∈ Q. A set F ⊆ Q is called a strengthening frontier for q in Q if

• for any q′ ∈ F, we have q′ |= q and q′ ̸≡ q;
• for any q′′ ∈ Q, if q′′ |= q and q′′ ̸≡ q, then there is q′ ∈ F such that q′′ |= q′ .

A set F ⊆ Q is called a weakening frontier for q in Q if

• for any q′ ∈ F, we have q |= q′ and q′ ̸≡ q;
• for any q′′ ∈ Q, if q |= q′′ and q′′ ̸≡ q, then there is q′ ∈ F with q′ |= q′′ .

Trivial strengthening/weakening frontiers for q comprise all queries that are properly stronger/weaker than q in Q; our concern, however, is finding small frontiers. We show now that, for Qσp [✸] and Qσp [⃝✸], one can compute a strengthening/weakening frontier for any given q in polytime.

Theorem 7. Let q ∈ Qσp [⃝✸] be in normal form (1). A strengthening frontier for q in Qσp [⃝✸] can be computed in polytime by applying once to q one of the following operations, for i ∈ [n] and qi = ρi ∧ oi+1(ρi+1 ∧ · · · ∧ onρn):

1. extend some ρi in q by some A ∈ σ \ ρi;
2. replace some ✸qi in q by ✸(⊤∧✸qi);
3. replace some oi = ✸ in q by ⃝ provided that the resulting query is in normal form;
4. add on+1ρn+1 at the end of q, where on+1 = ✸ and ρn+1 = A, for some A ∈ σ.

If q ∈ Qσp [✸], a strengthening frontier for q in Qσp [✸] can be computed in polytime using operations 1, 2, and 4.

Proof. Let F be the set of queries obtained by a single application of one of these operations to q. By Lemma 3, q′ |= q and q ̸≡ q′ for all q′ ∈ F. Let q′ |= q and q ̸≡ q′ , for some q′ ∈ Qσp [⃝✸] of the form q′ = ρ′0 ∧ o′1 (ρ′1 ∧ · · · ∧ o′m(ρ′m)). Take a containment witness h: [n] → [m] for q′ , q. If h is surjective, then n = m and h(i) = i for all i ∈ [n], and so ρi ⊆ ρ′i . As q ̸≡ q′ , either o′i = ⃝ and oi = ✸, for some i ∈ [n], or ρi ⊊ ρ′i , for some i ∈ [n]. In the former case, operation 3 gives q′′ ∈ F with q′ |= q′′ ; in the latter one, operation 1 gives such a q′′ .

Suppose h is not surjective. If there is i < n such that h(i + 1) - h(i) ≥ 2, then q′ |= q′′ for a q′′ ∈ F given by operation 2. Otherwise m is not in the range of h, and we get such a q′′ ∈ F by operation 4. ⊣

Example 8. For σ = {A,B} and q = ✸(A ∧⃝B), operations 1-4 give the following strengthening frontier for q:

A weakening frontier can be constructed by reversing operations 1-3 from Theorem 7 and using a similar argument:

Theorem 9. Let q ∈ Qσp [⃝✸] be in normal form (1). A weakening frontier for q in Qσp [⃝✸] can be computed in polytime by applying once to q one of the following operations, for i ∈ [n] and qi = ρi ∧ oi+1(ρi+1 ∧ · · · ∧ onρn):

1. drop some atom from ρi;
2. replace some ✸(⊤∧✸qi) in q by ✸qi;
3. replace some oi = ⃝ by ✸.

If q ∈ Qσp [✸], a weakening frontier for q in Qσp [✸] can be computed in polytime using operations 1 and 2.

Example 10. For σ = {A, B} and q = ✸(A ∧ ⃝B), operations 1-3 give the following weakening frontier for q:

Note that the computed weakening frontier can be made smaller by omitting ✸A, which is weaker than ✸(A ∧ ✸B).

We next consider frontiers for queries in Qσ [✸]. We say that q = ρ ∧ q1 ∧ · · · ∧ qn ∈ Qσ [✸] in normal form is redundancy-free if it does not contain qi, qj with i ̸= j and qi |= qj. Clearly, for any q ∈ Qσ [✸], we can compute an equivalent redundancy-free q′ ∈ Qσ [✸] in polytime.

Theorem 11. Let q = ρ ∧ q1 ∧ · · · ∧ qn ∈ Qσ [✸] be redundancy-free. A weakening frontier for q in Qσ [✸] can be computed in polytime by a single application of one of the following operations to q:

1. drop some atom from ρ;
2. replace some qi by ∧ Fi, where Fi is the weakening frontier for qi in Qσp [✸] provided by Theorem 9.

Proof. Let F be the set of queries defined above. Clearly, q |= q′ ; as q is redundancy-free and in view of Lemma 4, q ̸≡ q′ for all q′ ∈ F. Suppose q |= q′ and q ̸≡ q′ , for some q′ = ρ′ ∧ q′1 ∧ · · · ∧ q′m in Qσ [✸]. By Lemma 4, ρ′ ⊆ ρ and, for each j, 1 ≤ j ≤ m, there exists f(j), 1 ≤ f(j) ≤ n, with qf(j) |= q′j . If ρ′ ⊊ ρ, then operation 1 gives a q′′ ∈ F with q′′ |= q′ . Otherwise, as q ̸≡ q′ , there is qi such that q′j ̸|= qi for all q′j , 1 ≤ j ≤ m. Let q′′ be the query obtained from q by replacing qi with ∧ Fi by operation 2. To establish q′′ |= q′ , it suffices to show that f(j) = i implies ∧ Fi |= qj. So suppose f(j) = i. Then q′j ̸|= qi, and so, by the definition of Fi, there is q′′ i ∈ Fi with q′′ i |= qj. ⊣

However, strengthening frontiers for queries in Qσ [✸] are not necessarily of polynomial size as shown by the following: Example 12. We represent queries in Qσ [✸] of the form (1) as ρ0 . . . ρn. For σ = {A1,A2,B1,B2}, let q1 = ∅(qσ)nq, q2 = ∅σ2n+1 , and q = {A1, A2}{B1, B2}. Using [Fortin et al., 2022, Example 18], one can show that any strengthening frontier for the query q1 ∧ q2 in Qσ [✸] is of size O(2n ).

Note also that weakening frontiers for q ∈ Qσin can be computed in polytime using operation 1 in Theorem 9 (if i = 1 and |ρi| = 1, we drop ⊤ and take ✸(ρ2 ∧⃝(ρ3 ∧ · · · ∧⃝ρn)). On the other hand, strengthening frontiers can be infinite:

Example 13. All ✸(A∧⃝nA), n > 0, are in any strengthening frontier for q = ✸A in Qσin , where σ = {A}.

As shown by Theorem 17, the lack of polytime computable strengthening frontiers in Q[✸] affects the complexity of verifying most specific separators. In contrast, the lack of polytime computable strengthening frontiers in Qin turns out to be harmless. For n ≥ tdp(q), call F ⊆ Q an n-bounded weakening/strengthening frontier for q in Q if F is a weakening/strengthening frontier for q in the class {q′ ∈ Q | tdp(q′ ) ≤ n} (we assume n to be given in unary).

Theorem 14. Weakening frontiers and n-bounded strengthening frontiers in Qσin can be computed in polytime.

Finally, we observe that Theorems 7 and 9 give an alternative way of computing unique characterisations of queries in Qσp [⃝✸] by data examples in polynomial time compared to [Fortin et al., 2022], which opens another route to studying unique characterisations and exact learning of temporal queries.

6 Complexity

Now we show complexity bounds for the decision and counting problems from Section 4, starting with verification and observing that polytime computable n-bounded frontiers imply tractable verification of most specific/general separators:

Lemma 15. If an n-bounded strengthening/weakening frontier for q ∈ Q is polytime computable in |q| and n, then most specific/general separator verification for Q is in P.

Proof. Let n = min{maxD | D ∈ E+}. We compute an n-bounded strengthening frontier F for q in Q and use that q ∈ mss(E,Q) iff q ∈ s(E,Q) and q′ /∈ s(E,Q) for all q′ ∈ F. The case of mgs(E,Q) is similar. ⊣

Corollary 16. Most specific/general separator verification is in P for Qp[✸], Qp[⃝✸], and Qin. Most general separator verification is in P for Q[✸].

Proof. It follows fromLemma 15 and Theorems 7, 9, 14 that most specific/general separator verification is in P for Qp[✸], Qp[⃝✸], and Qin. By Theorem 11, most general separation verification is also in P for Q[✸]. ⊣

Most specific separator verification is harder for Q[✸]:

Theorem 17. For Q[✸], the most specific separator verification problem coincides with the unique most specific separator verification problem and is CONP-complete.

Proof. As we know, E has a unique most specific separator in Q[✸] iff s(E,Q[✸]) ̸= ∅. Hence most specific separator verification coincides with unique most specific separator verification. Given q and E, we can check in NP that either q /∈ s(E,Q[✸]) (which is in P) or that there is q′ ∈ s(E,Q[✸]) with q′ |= q and q′ ̸≡ q (which is in NP). This gives the CONP upper bound. The more involved proof of the lower one (in the appendix) is based on ideas similar to those in the proof of Theorem 21 below. ⊣

In the cases when most specific/general separators are not necessarily unique, we obtain the following:

Theorem 18. Unique most specific/general separator verification in Qp[⃝✸], Qp[✸], Qin as well as unique most general separator verification in Q[✸] are CONP-complete.

Proof. The upper bounds follow from Corollary 16. The lower ones are by reduction of the problem to decide whether, for a Boolean formula φ and a satisfying assignment a, there is a satisfying assignment for φ different from a. We use ideas similar to those in the proof of Theorem 21. ⊣

We now turn to the existence and counting problems. Recall that UNIQUE SAT is the problem to decide whether there is exactly one satisfying assignment for a propositional formula [Blass and Gurevich, 1982]. It is in ∆p2 , CONP-hard, and complete for the class US of problems solvable by a non-deterministic polynomial-time Turing machine M that accepts iff M has exactly one accepting path. A counting problem is in the class ♯P if there is such M whose number of accepting paths coincides with the number of solutions to the problem [Arora and Barak, 2009].

Theorem 19. For Qp[⃝✸], Qp[✸], Qin, counting most specific/general separators is ♯P-complete; the existence of a unique most specific/general separator is US-complete. The same holds for most general separators in Q[✸].

Theorem 19 follows from the very general and fine-grained complexity results provided by Theorems 20 and 21 below.

Theorem 20. Let Q ⊆ Qp[⃝✸] be a class with polytime decidable membership and polytime computable n-bounded strengthening/weakening frontiers for queries in Q. Then

• counting most specific/general Q-separators is in ♯P;
• the existence of a unique most specific/general Q-separator is in US.

This also holds for most general separators in classes of conjunctions of ⃝✸-path queries closed under dropping conjuncts and having polytime computable weakening frontiers.

Proof. Given E, construct a TM M that guesses a q ∈ Q with tdp(q) ≤ n = min{maxD | D ∈ E+} and accepts if q separates E and no q′ in the n-bounded frontier for q in Q separates E. As we know, the required checks are in P. In the second claim, M guesses a query q = ρ ∧ ✸q1 ∧ · · · ∧ ✸ql with qi ∈ Qp[⃝✸] and l ≤ |E-|. ⊣

For the lower bounds, we take into account the boundedness of sig(E) and the cardinalities |E+| and |E-| of positive and negative examples in E. The next result provides matching lower bounds for Theorem 19 even if the signature is bounded and only one of |E+| and |E-| is unbounded, except for Qin and Q[✸], where |E+| has to be unbounded.

Theorem 21. Let Q ⊆ Qp[⃝✸] be any class of queries containing all ✸ρ with a conjunction of atoms ρ. Then

• counting most specific/general Q-separators is ♯P-hard;
• the existence of unique most specific/general separator is US-hard

even for E = (E+, E-) and σ = sig(E) with (a) |E-| ≤ 1 or (b) |E-| ≤ 1, |σ| = 2 and Q = Qin or Q ⊇ Qp[✸], or (c) |E+| ≤ 4, |σ| = 3, Q ⊇ Qp[✸]. This result also holds for most general separators in Q[✸] and |E-| = 1, |σ| = 2.

Proof. We sketch the proof of the first claim by a parsimonious reduction from SAT for an unbounded number of negative examples (which can be easily merged into one). Take a CNF φ = ψ1 ∧ · · · ∧ ψk with clauses ψi over variables x1, . . . , xn. We construct E = (E+,E-) such that there is a bijection between the satisfying assignments for φ and the separators for E in Q[⃝✸] (even queries of the form ✸ρ). The claim follows from the fact that the separating queries are mutually |=-incomparable. Define the positive examples E+ = {D0,D′0 ,D1, . . . ,Dn} with 2n atoms A1, ¯ A1, . . . ,An, ¯ An by taking

for 1 ≤ i ≤ n. Let E- = {D1 1 , . . . ,D1 k , D2 1 , . . . , D2n }, where D1 i , 1 ≤ i ≤ k, comprises ¯ Aj(1) if xj does not occur negatively in ψi, and Aj(1) if xj does not occur positively in ψi, and D2 i = {Aj(1), ¯ Aj(1) | j ̸= i}. For an assignment a for x1, . . . , xn, let ρa contain Ai if a(xi) = 1 and ¯ Ai, otherwise. Now our claim follows from the following: (i) if a satisfies φ, then ✸ρa separates E; (ii) if q ∈ Qp[⃝✸] separates E, then q ≡ ✸ρa, for some a satisfying φ.

To bound σ and/or E+, we give parsimonious reductions from SAT and employ techniques for the longest common subsequence problem and separator existence for sequence queries in Qp[✸] [Blin et al., 2012; Fraser, 1996]. ⊣

Again, re-using techniques from the literature on algorithms for sequences needs some care. Similar to separability, for example sets of sequences, counting most general/specific sequence Qin-separators is easily seen to be in P even for unbounded signatures and example sets, but Theorem 21 shows that this is not so for Qin on non-sequence data instances.

Surprisingly, the complexities of counting most general separators and deciding the existence of a unique one diverge if we bound the number of examples, cf. Theorems 23 and 27.

Theorem 22. Let Q = Q[✸] or Q ⊆ Qp[⃝✸] be any class containing all ✸ρ with a conjunction of atoms ρ. Then counting most general Q-separators is ♯P-hard even for example sets E = (E+, E-) with |E+| = 2 and |E-| = 1.

Proof. The proof is by reduction from counting satisfying assignments for monotone formulas: E- is as in the proof of Theorem 21 and the positive examples are D0, D′0 . ⊣

Theorem 22 does not hold for counting most specific separators in Qin, which is easily seen to be in P if |E+| is bounded. It remains open whether some version of this theorem holds for most specific separators in Qp[⃝✸] or Qp[✸].

7 Algorithms

The frontiers defined in Section 5 give a polytime algorithm for computing a most specific/general separator starting from any given separator. Suppose Q ∈ {Qp[✸],Qp[⃝✸],Qin}, we are given q ∈ s(E,Q) and need a most specific separator. By Theorems 7, 9, the length of the longest |=-chain in s(E,Qp[⃝✸]) is polynomial in |E|. 1 We take, if possible, some q′ ∈ s(E,Q) in the strengthening frontier for q, then q′′ ∈ s(E,Q) in the strengthening frontier for q′ , etc. This process terminates after polynomially-many steps, returning a most specific Q-separator (and so the unique one, if any).

Thus, we can focus on algorithms deciding the existence of a (unique most specific/general) separator and constructing it. In the next theorem, we compute not just a random input separator, but a longest/shortest one. As strengthening/weakening frontiers contain queries that are not shorter/longer than the input, the procedure above will compute a longest most specific/shortest most general separator.

Theorem 23. Let E = (E+,E-), σ = sig(E), t+/t- be the maximum timestamp in E+/E-, c+ = |E+|, c- = |E-|, and Q ∈ {Qp[✸],Qp[⃝✸]}. The following can be done in time O(tc+ + tc-- ):

• (a) deciding whether s(E,Q) ̸= ∅;

1 In contrast, the proof of Theorem 21 shows the size of the maximal antichain in s(E,Qp[✸]) is in general exponential in |E|.

• (b) computing a longest/shortest separator in s(E,Q);
• (c) deciding the existence of a unique most specific Qseparator and a unique most general Qp[✸]-separator, and constructing such a separator.

For bounded c+ and c-, problem (a) is in NL.

Proof. We only sketch the construction for Q = Qp[✸].

(a) First, we define a directed labelled rooted graph P whose paths from the root represent Qp[✸]-queries with positive examples E+ = {D1, . . . ,Dc+ }. Its nodes are vectors (n1, . . . , nc+ ) with 0 ≤ ni ≤ maxDi, which are labelled by the sets {A ∈ σ | A(ni) ∈ Di for all i}, and the edges are (n1, . . . , nc+ ) → (n′1 , . . . , n′c+ ) with ni < n′i for all i. The root of P is ¯0 = (0, . . . , 0). To illustrate, let E = (E+, E-), where E+ = {D+ 1 ,D+ 2 }, E- = {D1 ,D2 ,D3 },

Graph P is shown on the left-hand side of the picture below:

Each path starting at ¯0 gives rise to a Qσp [✸]-query with positive examples in E+: e.g., (0, 0) → (1, 1) → (2, 2) gives rise to the query A ∧ ✸(C ∧ ✸B).

Next, define another graph N for E- = {D1, . . . ,Dc- }. Its nodes are (n1, . . . , nc- ), where ni ∈ [0, maxDi] ∪ {∞}, including ¯∞ = (∞, . . . ,∞), which is labelled by σ. The label of (n1, . . . , nc- ) is {A | A(ni) ∈ Di, for all ni ̸=∞}. The edges are defined in the same way as for P, with ni < ∞, for any ni. The root of N is (n1, . . . , nl), where ni = 0 if {A(0) | A(0) ∈ D, for all D ∈ E+} ⊆ Di and ni = ∞ otherwise (see the picture above). Let q be a Qσp [✸]-query of the form (1) with ρ0 contained in the root's label. Then all Di ∈ E- are negative examples for q iff every path starting at the root and having labels ρ′0 , . . . , ρ′n with ρ′i ⊇ ρi, for all i ≤ n, comes through node ¯∞. In our example, every such path for q = A∧✸B and q = A∧✸(C ∧✸B) involves ¯∞. However, this is not the case for q = A∧✸C.

Consider now a graph P ⊗ N with nodes (n,m), where n is a node in P and m a node in N with l(n) ⊆ l(m), for the labels l(n) and l(m) of n and m. We have an edge (n,m) → (n′ ,m′ ) in P⊗N iff n→n′ in P, m→m′ in N, and P ⊗ N has no (n′ , m′′ ) with m → m′′ , m′′ i < m′i and m′′ i ̸= ∞, for some i, mi being the ith coordinate of m. One can see that, for any (n,m) in P × N and n′ in P, there exists at most one edge (n,m) → (n′ ,m′ ). The root of P×N comprises the roots of P and N. In our example, the edges from the root (¯0, (0, 0,∞)) of P⊗N lead to ((1, 2), (∞, 1,∞)), ((2, 1), (1, 1,∞)), ((1, 1), (1,∞,∞)) and ((2, 2), ¯∞). Given a path

let qπ be the Qp[✸]-query of the form (1) with ρi = l(ni) (note that qπ is not necessarily in normal form). We call π a separating path for E if l(nn) ̸= ∅ and mn = ∞.

Lemma 24. s(E,Q) ̸= ∅ iff P ⊗ N contains a separating path π, with qπ separating E.

In our running example, P⊗N has two separating paths: π1 = (¯0, (0, 0,∞)), ((2, 2), ¯∞) and π2 = (¯0, (0, 0,∞)), ((1, 1), (1,∞,∞)), ((2, 2), ¯∞), which give rise to the separators qπ1 = A ∧ ✸B and qπ2 = A ∧ ✸(C ∧ ✸B).

The existence of a separating path in P⊗N can be checked in time O(tc+ + tc- ). If c+ and c- are bounded, given (n,m) and (n′ , m′ ), we can check in logspace whether (n, m) is the root of P⊗N and (n,m) → (n′ ,m′ ), and so the existence of a separating path can be decided in NL.

The proof of point (b) relies on the following observation:

Lemma 25. If q of the form (1) separates E, then there is a separating path of the form (2) with ρi ⊆ l(ni), for all i ≤ n.

It follows that the length of a longest/shortest separator for E coincides with the length of a longest/shortest separating path in P⊗N, which can be found in polytime.

The proof of point (c) is based on the following criterion:

Lemma 26. A Qp[✸]-query q is a unique most specific Qp[✸]-separator for E iff there is a separating path π such that q = qπ and qπ |= qν, for every separating path ν.

In our example, qπ2 is a unique most specific separator. We show that the criterion of Lemma 26 can be checked in polytime in P×N. For unique most general separators, the seemingly obvious inversion of qπ |= qν does not give a criterion, and a different type of graph is required. ⊣

Finally, we show how Theorem 23 can be used to check the existence of and construct unique most general separators in Q[✸] (the case of unique most specific ones is trivial).

Theorem 27. An example set E = (E+,E-) has a unique most general separator in Q[✸] iff q = ∧D∈S qD separates E, where S is the set of D ∈ E- such that (E+, {D}) has a unique most general separator, qD, in Qp[✸]. In this case, q is a unique most general separator of E in Q[✸].

8 Conclusions

We have conducted a comprehensive complexity analysis of extremal separators in the spaces s(E,Q) with Q ranging from various classes of temporal path ⃝✸-queries to arbitrary ✸-queries. For arbitrary ⃝✸-queries, we only know more or less straightforward upper bounds such as Πp2 for (unique) most general separator verification and Σp3 for unique most general separator existence. Establishing tight bounds remains a challenging open problem, which requires a deeper understanding of query containment for these queries.

We also plan to analyse the shortest and longest separators. For instance, Jung et al. (2024) show that verifying such separators in s(E,Qp[⃝✸]) is CONP-complete-harder than verifying most specific/general ones. An empirical evaluation of our algorithms and more expressive query languages (say, with non-strict ✸ and 'until') are left for future work.