In reverse engineering of database queries, one aims to construct a query from a set of positively and negatively labelled answers and non-answers. The query can then be used to explore the data further or as an explanation of the answers and non-answers. We consider this reverse engineering problem for queries formulated in various fragments of positive linear temporal logic LTL over data instances given by timestamped atomic concepts. We focus on the design of suitable query languages and the complexity of the separability problem: 'does there exist a query in the given query language that separates the given answers from the non-answers?'. We deal with both plain LTL queries and those that are mediated by ontologies providing background knowledge and formulated in fragments of clausal LTL.
Supporting users of databases by constructing a query from examples of answers and nonanswers to the query has been a major research area for many years [1]. In the database community, research has focussed on standard query languages such as (fragments of) SQL, graph query languages, and SPARQL [2, 3, 4, 5, 6, 7, 8, 9]. The KR community has been concerned with constructing queries from examples under the open world semantics and with background knowledge given by an ontology [10, 11, 12, 13, 14]. In both cases, the focus has been on general multi-purpose query languages. A fundamental problem that has been investigated by both communities is known as separability or query-by-example: given sets + and − of pairs (, ) with a database and a tuple in , and a query language , does there exist a query ∈ that separates (+, − ) in the sense that |= () for all (, ) ∈ + and ̸|= () for all (, ) ∈ − (or , |= () for all (, ) ∈ + and , ̸|= () for all (, ) ∈ − if an ontology is present)?1 There are various strategies to ensure that the query is a generalisation of the positive examples and does not overfit. For instance, one can ask for the existence of a small separating query in or one can choose a query language that enforces generalisation by not admitting disjunction. In the latter case, query-by-example is often very hard computationally: it is coNExpTime-complete for conjunctive queries (CQs) over standard relational databases [15, 16] and even undecidable for CQs under ℰ ℒℐ or ℒ ontologies [17].
In many applications, the input data is timestamped and queries are naturally formulated in languages with temporal operators. Taking into account the prohibitive complexity of many query-by-example problems already in the static case, it does not seem wise to start an investigation of the temporal case by considering temporal extensions of standard query languages (which can only lead to computationally even harder problems). Instead, we investigate the simpler but still very useful case in which data, , is a set of timestamped atomic concepts. 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 [18]. To avoid overfitting, we only consider such fragments without ∨. The most expressive query language we deal with, [U], is thus defined as the set of formulas constructed from atoms using ∧ and U (via which ○ and ◇ can be defined). The fragments [◇], [○ ], and [○ , ◇] are defined analogously.
Within this temporal setting, we take a broad view of the potential applications of the reverse
engineering of queries and the query-by-example problem. On the one hand, there are
nonexpert end-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. Query-by-example 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 linear temporal logic formulas and, more
generally, explainable AI [19, 20, 21, 22, 23]. The following example illustrates this point.
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’, which can be represented by the atomic concept , ‘strong vibration’, , etc. Suppose the
engine stopped after the runs 1+ and 2+ shown below but did not stop after the runs 1− , 2− ,
3− , where we assume the runs to start at 0 and measurements to be recorded at 0, 1, 2, . . . :
1+ = { (
+
3+ = { (
The queries used in Example 1 are of a particular ‘linear’ form and suggest a restriction to
path queries in which the order of the atoms is fixed and not left open as in ◇ ∧ ◇. More
precisely, path ○ ◇-queries in the class [○ , ◇] take the form
(
= 0 ∧ ( 1 U ( 1 ∧ ( 2 U (. . . ( U ) . . . )))), where is a conjunction of atoms or ⊥. Path queries are motivated by two observations. First, if a query language allows conjunctions of queries, then, dually to the overfitting problem for disjunction, the admission of multiple negative examples becomes trivialised: if queries separate (+, {}) for ∈ − , then the conjunction ⋀︀∈− separates (+, − ). In particular, the query-by-example problem becomes polynomially reducible to its version with a single negative example. This is clearly not the case for path queries.
Example 2. Let 1 = {(
Second, numerous natural types of query classes from applications are represented by path queries. For example, the existence of a common subsequence of the positive examples that is not a subsequence of any negative example corresponds to the existence of a separating query in [◇] with 0 = ⊤ and ̸= ⊤ for > 0, and the existence of a common subword of the positive examples that is not a subword of any negative example corresponds to the existence of a separating query of the form ◇( 1 ∧ ○ ( 2 ∧ · · · ∧ ○ )). The unique characterisability and learnability of path queries is investigated in [24].
Except for [○ ] = [○ ] (modulo logical equivalence), no nontrivial inclusion relations hold between the separation capabilities of the query languages introduced above, as illustrated by the following example.
Example 3. (
(
(
(
We now briefly present our initial results on the complexity of the separability problem for LTL queries, both plain and mediated by an LTL-ontology.
Ontology-free LTL queries. Separability in [○ ] is almost trivial as it corresponds to the existence of a time point where some atom holds in all positive examples but in no negative example, which is decidable in polynomial time. For the query languages ranging from [◇] and [◇] to [○ , ◇] and [○ , ◇] and also [U], separability turns out to be NP-complete. The upper bound is proved by observing that, in any of these languages, every separable example set can be separated by a query of polynomial size. The matching lower bound is established by reduction of the NP-hard problem of deciding whether the words in a given set contain a common subsequence of a given length [25]. Separability by [U]-queries turns out to be trickier because of the interplay of ∧, the left- and the right-hand sides of the U-operator. Example 4. The example set below, where the instance on the right is negative, is separated by 2, 1 2 1, 2 1 0 1 2 3 4 5 0 1 2 3 0 1 3 the [U]-query ◇(︀ (1 U 1) ∧ (2 U 2))︀ but is not separable in any other class of queries.
We give a separability criterion in terms of U-simulations between subsets of the disjoint union of the positive examples and points of a negative example (cf. [26]). Then, using a gametheoretic variant of U-simulations, we show that a separating [U]-query can be constructed in PSpace. However, at the moment, we only have an NP-lower bound for separability. Separability under LTL Ontologies. Apart from full LTL, we consider its fragment LTL□◇ that only uses the operators □ and ◇, also known as the Prior logic [27, 28, 29, 30], and the Horn fragment LTLh□o○ rn containing axioms of the form 1 ∧ · · · ∧ → +1, where the are atoms possibly prefixed by □ and ○ for ≤ + 1, and also by ◇ for ≤ . The ontology axioms are supposed to hold at all times.
Separability by (path) ◇-queries is Σ 2-complete under LTL□◇ ontologies and PSpacecomplete under LTLh□o○ rn ontologies. For LTL ontologies, we have a NExpTime upper bound. We conjecture that exactly the same bounds can be proved for (path) ○ ◇-queries. As concerns [U]-queries, separability under LTLh□o○ rn ontologies is shown to be between ExpSpace and NExpTime; for ‘branching’ [U− ]-queries without nesting U-operators on the left of U, it can be decided in ExpTime using U-simulations. We establish the upper bounds by constructing two exponential-size transition systems + and − from (, +) and (, − ) such that () there is a trace-based simulation of + by − if (+, − ) is separated in [U] and () there is a tree-based simulation of + by − if (+, − ) is separated in [U− ]. The existence of trace-based and tree-based simulations can be decided in PSpace- and P, respectively [31].
The obtained complexity results are summarised in the table below: 1 2 2 4 QBE(ℒ, ) [U] [U− ] [U] [○ , ◇] [○ , ◇] [◇] [◇]
? ≤
NExpTime ≥
LTLh□o○ rn
? ≤ ExpTime NExpTime, ≤ ExpSpace ≤ ExpTime ≤ ExpSpace = PSpace
This research was supported by the EPSRC UK grants EP/S032207 and EP/S032282 for the joint project ‘quantMD: Ontology-Based Management for Many-Dimensional Quantitative Data’ and by the RSF grant 22-11-00323 when M. Zakharyaschev was visiting the HSE University. [13] G. Cima, F. Croce, M. Lenzerini, Query definability and its approximations in ontologybased data management, in: G. Demartini, G. Zuccon, J. S. Culpepper, Z. Huang, H. Tong (Eds.), CIKM ’21: The 30th ACM International Conference on Information and Knowledge Management, Virtual Event, Queensland, Australia, November 1 - 5, 2021, ACM, 2021, pp. 271–280. URL: https://doi.org/10.1145/3459637.3482466. doi:10.1145/3459637. 3482466. [14] J. C. Jung, C. Lutz, H. Pulcini, F. Wolter, Separating data examples by description logic concepts with restricted signatures, in: Proc. of KR, 2021. [15] R. Willard, Testing expressibility is hard, in: D. Cohen (Ed.), Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer Science, Springer, 2010, pp. 9–23. URL: https://doi.org/10.1007/978-3-642-15396-9_4. doi:10. 1007/978-3-642-15396-9\_4. [16] B. ten Cate, V. Dalmau, The product homomorphism problem and applications, in: Proc.
of ICDT, 2015, pp. 161–176. [17] M. Funk, J. C. Jung, C. Lutz, H. Pulcini, F. Wolter, Learning description logic concepts: When can positive and negative examples be separated?, in: Proc. of IJCAI, 2019, pp. 1682–1688. [18] S. Demri, V. Goranko, M. Lange, Temporal Logics in Computer Science, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2016. [19] C. Lemieux, D. Park, I. Beschastnikh, General LTL specification mining (T), in: Proc. of
ASE, IEEE, 2015, pp. 81–92. [20] D. Neider, I. Gavran, Learning linear temporal properties, in: Proc. of FMCAD 2018, IEEE, 2018, pp. 1–10. URL: https://doi.org/10.23919/FMCAD.2018.8603016. doi:10.23919/ FMCAD.2018.8603016. [21] A. Camacho, S. A. McIlraith, Learning interpretable models expressed in linear temporal logic, in: Proc. of ICAPS 2018, AAAI Press, 2019, pp. 621–630. URL: https://aaai.org/ojs/ index.php/ICAPS/article/view/3529. [22] N. Fijalkow, G. Lagarde, The complexity of learning linear temporal formulas from examples, in: J. Chandlee, R. Eyraud, J. Heinz, A. Jardine, M. Zaanen (Eds.), Proceedings of the 15th International Conference on Grammatical Inference, 23-27 August 2021, Virtual Event, volume 153 of Proceedings of Machine Learning Research, PMLR, 2021, pp. 237–250.
URL: https://proceedings.mlr.press/v153/fijalkow21a.html. [23] 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 - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, Springer, 2022, pp. 263–280. URL: https://doi.org/10. 1007/978-3-030-99524-9_14. doi:10.1007/978-3-030-99524-9\_14. [24] M. Fortin, B. Konev, V. Ryzhikov, Y. Savateev, F. Wolter, M. Zakharyaschev, Unique characterisability and learnability of temporal instance queries, in: Proc. of KR, 2022. [25] D. Maier, The complexity of some problems on subsequences and supersequences, J. ACM 25 (1978) 322–336. URL: https://doi.org/10.1145/322063.322075. doi:10.1145/322063. 322075. [26] N. Kurtonina, M. de Rijke, Bisimulations for temporal logic, J. Log. Lang. Inf. 6 (1997) 403– 425. URL: https://doi.org/10.1023/A:1008223921944. doi:10.1023/A:1008223921944. [27] A. Prior, Time and Modality, Oxford University Press, 1956. [28] H. Ono, A. Nakamura, On the size of refutation Kripke models for some linear modal and tense logics, Studia Logica (1980) 325–333. [29] J. P. Burgess, Basic tense logic, in: Handbook of Philosophical Logic: Volume II: Extensions of Classical Logic, Reidel, Dordrecht, 1984, pp. 89–133. [30] M. Y. Vardi, From Church and Prior to PSL, in: 25 Years of Model Checking - History,
Achievements, Perspectives, volume 5000 of LNCS, Springer, 2008, pp. 150–171. [31] O. Kupferman, M. Y. Vardi, Verification of fair transisiton systems, in: R. Alur, T. A.
Henzinger (Eds.), Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, volume 1102 of Lecture Notes in Computer Science, Springer, 1996, pp. 372–382. URL: https://doi.org/10.1007/3-540-61474-5_ 84. doi:10.1007/3-540-61474-5\_84.