On the First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic (Extended Abstract)

1 Introduction

Ontology-mediated query (OMQ) answering has recently become one of the most successful applications of description logics (DLs) and semantic technologies. Its main aim is to facilitate user-friendly access to possibly heterogeneous, distributed and incomplete data. To this end, an ontology is employed to provide (a) a convenient and uniform vocabulary for formulating queries and (b) a conceptual model of the domain for capturing background knowledge and obtaining more complete answers. Thus, instead of querying data directly by means of convoluted database queries, one can use OMQs of the form (O, q), where O is an ontology and q a query formulated in the vocabulary of O. Under the standard certain answer semantics for OMQs, the answers to (O, q) over a data instance D are exactly those tuples of individual names from D that satisfy q in every model of O and D. Because of this open-world semantics, answering OMQs can be computationally much harder than evaluating standard database queries. For example, answering an atomic query A(x) using an ontology in the standard description logic ALC can be CONP-hard for data complexity-the complexity measure (adopted in this paper) that regards the OMQ as fixed and the data instance as the only input to the OMQ answering problem. For this reason, weaker description logics (DLs) have been developed to enable not only tractable OMQ answering but even a reduction-known as first-order (FO-) rewritability [Calvanese et al., 2007b]-of OMQ answering to evaluation of standard relational database queries directly over the data, which is in AC0 for data complexity. After 15 years of intensive research and coding, ontology-based data access (OBDA, aka virtual knowledge graphs) originally conceived by [Calvanese et al., 2007b; Poggi et al., 2008] has become a well-developed area lying at the crossroads of knowledge representation, databases and computational complexity [Xiao et al., 2018], with multiple real-word applications using mature systems such as Mastro and Ontop; see [Xiao et al., 2019] for a survey.

∗Extended version published in the AI journal, 2021.

†Contact Author

An important application area where OBDA has so far failed to make a substantial impact is the management of temporal data. A typical example is querying data from sensors in complex industrial systems such as gas turbines, where sensors read the temperature, rotor speed, power, etc., in order to analyse and predict their behaviour. One of the problems engineers are facing in this scenario is identifying various events of interest (active power trip, abnormal restart, etc.) based on timestamped sensor readings stored in a database. The OBDA approach could immensely simplify this task for engineers by (i) encoding the definitions of those temporal events in an ontology, thereby making query formulation easier, and by (ii) using background knowledge to compensate for incomplete data due, for example, to sensor failures.

Unfortunately, OBDA languages such as OWL 2QL, standardised by the W3C, provide no means to express temporal events in ontologies because the addition of temporal operators even to inexpressive description logics tends to dramatically increase the complexity of reasoning and, in particular, ruin FO-rewritability of OMQs; see [Lutz et al., 2008; Artale et al., 2017] for surveys. One way to avoid this 'curse of many-dimensional logics' would be to keep OWL 2QL as the ontology language but extend the query language (say, SPARQL) with the relevant temporal operators [Borgwardt et al., 2015]. However, this approach clearly undermines principle (i) of OBDA as the burden of encoding complex temporal events in queries lies solely on the users' shoulders.

Here, we propose an alternative approach to designing logics for temporal OBDA, viz., to start with classical linear temporal logic LTL as an ontology language and monadic firstorder logic with < over timestamps as a query language. Our first observation is that already this basic temporal OBDA formalism is sufficiently expressive in scenarios where the interaction among the individuals in the object domain-say, between different turbines and their parts-usually captured by binary relations in DLs, is not important and can be neglected.

Example 1 Gas turbines, t, are equipped with multiple sensors, s, measuring the rotor speed, the temperature of the blades, vibration, electric current, etc. Imagine that a relational database in a remote diagnostic centre stores a binary predicate location(s, t) saying that sensor s is located in turbine t and a ternary predicate measurement(s, v, n) giving the numerical value v of the reading of s at time instant n. The timestamps of sensor readings are synchronised with a central computer clock, and so can be regarded as integers.

When defining important events like active power trip, engineers usually operate with statements such as 'the active power of turbine t measured by s is above 1.5MW at moment n', which can be obtained as database views of the form PowerSensort,s ≥1.5 (n). We regard these unary predicates as atomic propositions that can be true or false at different moments of time. Omitting t and s to simplify notation, we can then assume that our database D contains facts of the form

based on which we analyse the behaviour of the turbines. As some sensors occasionally fail to send their measurements, we cannot assume the data to be complete. Thus, in our sample data above, the sensor detecting if the turbine is running (by measuring the electric current) failed to send a signal at time instant 7. However, the power sensor attached to the turbine recorded ≥ 1.5MW at 7, which should imply that the turbine must have been running at 7. This piece of domain knowledge can be encoded as an ontology axiom

with the LTL-operator ✷ (at all times). Other LTL axioms in our example ontology O could look like

✷(Malfunction → ©F Pause ∧ ✸F Diagnostics).

The first of them says that a turbine cannot be paused and running at the same time; the second says that a disabled turbine cannot undergo diagnostics in the future (✸F ); and the third axiom asserts that immediately after (©F ) a malfunction the turbine is paused and will eventually be diagnosed.

Now, if we are interested in maximal intervals of uninterrupted run of a turbine, we can execute the following query formulated in MFO(<) (monadic first-order logic with <):

which is mediated by the ontology O and returns the certain answer [6, 8] over D. The MFO(<)-query

q2(x, y) = q1(x, y)∧∃z ((y < z < y+3)∧Diagnostics(z)) finds intervals of maximal continuous run followed by a diagnostics event within 3 time units. The certain answer to the OMQ (O, q2(x, y)) over D is [6, 8] as well because O and D imply that the diagnostics took place at some (unknown) moment within the interval [9, 11].

2 OMQs in LTL andMFO(<)

Formally, the temporal ontology language we present here operates with LTL axioms given in the clausal normal form

where the Ci are atomic concepts (unary predicates), possibly prefixed with the temporal operators ©F (next time), ✷F (always in the future) and their past-time counterparts ©P and ✷P . An ontology, O, is a finite set of such axioms. Note that every finite set of ✷-prefixed LTL-formulas can be efficiently converted into clausal form without affecting OMQ answering to be defined below. For example, the last axiom of O from Example 1 can be replaced by ✷(Disabled → ✷FA) and ✷(A ∧ Diagnostics → ⊥) with fresh A.

A data instance, D, is a finite set of atoms of the form A(n) with a timestamp n ∈ Z. We query data using MFO(<) formulas q(x) built from unary atoms A(x) and binary atoms x < y as usual in first-order logic. Here, x is the set of free variables in q, denoted as answer variables. An ontologymediated query is a pair (O, q(x)). A certain answer to (O, q(x)) over D is any assignment of some timestamps from D to the answer variables x under which q is true in all LTL-models of O and D. Note that we use the standard strict semantics of the LTL operators (which does not include the current point); see, e.g., [Gabbay et al., 1994; Demri et al., 2016].

We now define the key notion of FO-rewritability. Let L be a first-order language that is capable of speaking about finite linear orders. An OMQ (O, q(x)) is called L-rewritable if there is an L-formula Q(x) with free variables x-an Lrewriting of (O, q(x))-such that, for any data instance D, a tuple ℓ of timestamps from D is a certain answer to (O, q(x)) over D if and only if Q(ℓ) is true in D regarded as an FOstructure. Thus, answering L-rewritable LTL OMQs under the open-world semantics as defined above reduces to evaluating their L-rewritings over the original data under the closed-world semantics. In other words, the data complexity of answering those OMQs is the same as the data complexity of evaluating L-formulas. Good target languages L whose evaluation lies in one of the smallest complexity classes AC0 are FO(<) with one built-in predicate < over timestamps and FO(<,≡) that also allows the unary predicates x ≡ 0 (mod n), for any fixed n > 1. Executing such L-queries can be done by standard database management systems.

Example 2 (a) The OMQ (O, q1(x, y)) from Example 1 is FO(<)-rewritable to the following formula:

where π(x) stands for Pause(x) ∨ Malfunction(x - 1), ρ(x) for Run(x) ∨ PowerSensor≥1.5(x) and ι is a disjunction of sentences such as ∃z (Malfunction(z) ∧ Run(z + 1)) and ∃z (Pause(z) ∧ Run(z)) expressing inconsistency of O, D.

(b) Now, suppose an ontology O contains the axioms

saying that the turbine undergoes diagnostics in 24 hours after its activation, and that diagnostics repeats every 24 hours. The OMQ (O, q(x)) with q(x) = Diagnostics(x) is FO(<,≡)-rewritable to the following formula:

where x-y ∈ a+bN with constants a, b-i.e., x-y = a+bk, for some k ∈ N-is expressible via predicates of the form z ≡ 0 (mod b). However, (O, q) is not FO(<)-rewritable.

Not all OMQs are FO(<,≡)-rewritable: e.g., there is an OMQ that checks if the number of some events happened in a given data instance is even or odd, and as well known, the parity function is not in AC0 . This parity OMQ can be rewritten to an FO(<,MOD)-formula with quantifiers ∃nxϕ(x) checking if the number of timestamps ℓ satisfying ϕ(ℓ) is divisible by n. Evaluating FO(<,MOD) formulas corresponds to the circuit complexity class ACC0 . Our first result is:

Theorem 3 Any OMQ with an LTL-ontology and an MFO(<)-query is FO(RPR)- and MSO(<)-rewritable, and so can be answered in NC1 for data complexity.

Here, FO(RPR) comprises first-order formulas with relational primitive recursion [Compton and Laflamme, 1990] and MSO(<) monadic second-order formulas with <, both of which can be evaluated in NC1 for data complexity. Note that the SQL:1999 ISO standard contains a WITH RECURSIVE construct, which can represent some FO(RPR)-queries, and that AC0 ⫋ ACC0 ⊆ NC1 ⊆ LOGSPACE ⊆ P. This implies that answering LTL/MFO(<) OMQs can be performed by an efficient parallel algorithm; it also means that answering such OMQs can be done using finite automata.

One of the main results of this paper is a uniform syntactical classification of OMQs according to their rewritability type (= data complexity). We classify OMQs (O, q) along three axes: the form of MFO(<)-queries q, the Boolean shape of the clauses in ontologies O, and the temporal operators that can occur in O.

Before giving a survey of our results in terms of these axes, we discuss our choice of LTL and MFO(<) as ontology and query languages. LTL can be regarded as a fragment of MFO(<) by spelling out the quantifier patterns defining the temporal operators. This standard FO-translation can be done in linear time, and so from a purely technical viewpoint, we can equivalently express any LTL ontology in MFO(<). We note, however, that typical ontological axioms are much more intuitive and succinct in LTL than in MFO(<). The question then is whether MFO(<) could provide additional expressive power to formulate domain knowledge in the ontology. By a celebrated result in philosophical logic, called Kamp's Theorem [Kamp, 1968], the answer is negative: for every MFO(<)-formula ϕ with one free variable, one can construct an equivalent LTL formula ϕ∗ (i.e., ϕ(ℓ) is true in a model I over Z iff ϕ∗ is true at ℓ in I). It follows, in particular, that axioms ∀xϕ(x) can be translated into LTL as ✷ϕ∗ . In the worst case, this translation is non-elementary, and so there are sentences in MFO(<) that cannot be practically expressed in LTL. It seems, however, that such sentences are hardly relevant for the formulation of domain knowledge, and so we focus on LTL as our ontology language.

The question whether queries should be formulated in MFO(<) or LTL requires a more nuanced answer. First, Kamp's Theorem only holds for formulas with one free variable, and so there are practically relevant MFO(<) queries with more than one answer variable that cannot be expressed in LTL (see q1 and q2 in Example 1). Second, when formulating queries, one is often interested in non-tree-shaped patterns such as, for instance, the very simple MFO(<)-query

whose LTL-translation needs all possible linearisations of the variables, and so could be difficult to read. Below, we formulate our results for queries in MFO(<), but also characterise our most important fragment of MFO(<) in terms of LTL.

Now, for the first axis, apart from arbitrary MFO(<)- queries, we consider atomic queries of the form A(x) and quasi-positive queries that are built (inductively) from atoms A(x), (x < x′ ), (x = x′ ) and (x = x′ + 1) using ∧, ∨, ∀, ∃ as well as the guarded universal quantification such as

with quasi-positive ϕ. For example, the standard FOtranslation of the LTL formula AUB with the until operator U under the strict semantics is the quasi-positive MFO(<)- formula ∃y [(x < y) ∧ B(y) ∧ ∀z ((x < z < y) → A(z))]. Quasi-positive queries play a fundamental role for the formulation of our results, and so we start by characterising their expressive power. The first characterisation is semantical, in terms of monotone MFO(<)-formulas, i.e., those that are preserved under any addition of timestamps to the extension of atomic concepts in models. It is not hard to see that all quasipositive formulas are monotone. The other characterisation is syntactical, in terms of positive LTL concepts built from atomic concepts using ∧, ∨ and the temporal operators ✷F , ✸F , ©F , U and their past-time counterparts. It generalises Kamp's Theorem to the class of monotone formulas.

Theorem 4 An MFO(<)-formula is monotone iff it is equivalent over (Z, <) to a quasi-positive MFO(<)-formula.

(Monotone Kamp Theorem) Every monotone MFO(<)- formula with one free variable is equivalent over (Z,<) either to a positive LTL concept or to ⊥.

The second axis in our classification of OMQs is similar to that for DL ontologies [Calvanese et al., 2007b; Artale et al., 2009]: we distinguish between Boolean clauses (1), Horn clauses (without ∨ on the right-hand side), Krom clauses with k + m ≤ 2, and core clauses that are both Horn and Krom.

The third axis is in terms of temporal operators in ontologies. Namely, for any pair c ∈ {bool, horn, krom, core} and o ∈ {✷,©,✷©}, we denote by LTLoc the fragment of LTL with c-clauses (1), in which the temporal concepts Ci may only contain the (future and past) operators indicated in o. For example, ontologies given in Prior-LTL-one of the first temporal logics going back to Prior [Prior, 1956]- can be converted into LTL ✷ bool ontologies. We establish the following complete uniform syntactical classification of the LTL/MFO(<)-OMQs, complementing Theorem 3:

Theorem 5 (i) All OMQs with an LTL ✷ bool ontology and an atomic query are FO(<)-rewritable.

• (ii) All OMQs with an LTL ✷© krom ontology and an atomic query are FO(<,≡)-rewritable. Some of them are not FO(<)-rewritable.
• (iii) Answering OMQs with an LTL©horn ontology and an atomic query is NC1 -hard.
• (iv) All OMQs with an LTL ✷ horn ontology and a quasipositive MFO(<) query are FO(<)-rewritable.
• (v) All OMQs with an LTL ✷© core ontology and a quasipositive MFO(<) query are FO(<,≡)-rewritable. Some of them are not FO(<)-rewritable.
• (vi) Answering OMQs with an LTL ✷ krom ontology and a quasi-positive MFO(<) query is NC1 -hard.

3 Outlook

As an alternative to the open-world semantics for OMQ answering considered above, one can use the epistemic semantics (ES) proposed by [Calvanese et al., 2007a]. Under ES, ¬A(n) is regarded to be true if A(n) is not entailed. (The same semantics is used in the standard query language SPARQL for RDF datasets when interpreted with OWL ontologies under the entailment regimes [Glimm and Ogbuji, 2013].) For example, the answer to q1 from Example 1 under ES remains [6, 8]. However, q2 has no answers under ES because there is no ℓ in the interval [9, 11] such that Diagnostics(ℓ) is entailed. Indeed, the answer [6, 8] to q2 can be deemed meaningless as there is no definite time ℓ for diagnostics. This is one motivation for ES. Another motivation is that, for many OMQ languages, answering FO-queries with ∀ and ¬ under ES becomes decidable, while it is undecidable under the open-world semantics. As an alternative to our query language, we can use MFO(<) formulas, in which the atoms are replaced by LTL-formulas, under ES. All such OMQs will be FO(RPR)-rewritable. Even lower complexity bounds can be established when positive LTL-formulas are used as atoms; see [Artale et al., 2021b].

The classification of LTL/MFO(<) OMQs obtained in this paper is uniform in the sense that all OMQs in a given syntactical class are L-rewritable, for a target language L, with some of them being non-rewritable to any weaker language. Yet, many useful OMQs in a syntactical class can be rewritten to more efficient languages. Ideally, we would like to have an OBDA system that could recognise the optimal rewritability type for any given OMQ-in other words, determine the exact data complexity of answering that OMQ. The same problem has been investigated for datalog queries since the 1980s [Kanellakis, 1990] and for description logic OMQs since the 2010s [Bienvenu et al., 2014; Hernich et al., 2020].

First steps in this direction for OMQs, in which both ontology and query are given in LTL, were made in [Ryzhikov et al., 2021]. It was shown that, for any target language L ∈ {FO(<), FO(<, ≡), FO(<, MOD)}, deciding Lrewritability of OMQs (O, q) with LTL queries q is equivalent to deciding L-definability of the regular language given by an exponential-size automaton. The problem of recognising whether a regular language is L-definable has been considered since the 1990s. In particular, it has been shown that deciding FO(<)-definability of regular languages is PSPACEcomplete [Cho and Huynh, 1991] and, recently, that deciding the other types of L-definability is PSPACE-complete, too [Kurucz et al., 2021]. Using these results, [Ryzhikov et al., 2021] prove that deciding L-rewritability of the LTL OMQs mentioned above is EXPSPACE-complete and also identify some smaller classes of OMQs in which Lrewritability is decidable in PSPACE (for positive OMQs with a core ontology) and CONP (for atomic OMQs with a Krom ontology). However, the full picture is still far from clear.

LTL OMQs over discrete (Z,<) are appropriate for modelling synchronous systems with a central clock against which all events can be sequenced. However, in scenarios where sensors report their readings asynchronously, dense (Q,<) for both timestamps and ontology axioms appears more adequate. A promising temporal KR formalism in this case is metric temporal logic MTL that was introduced for modelling and reasoning about real-time systems [Koymans, 1990]. In MTL, the temporal operators are indexed by a time interval over which the operator works: for example, ✸(0,1.5]A is true at n iff A holds at some n′ with 0 < n′ - n ≤ 1.5. The interpretation domain is Q under the continuous semantics and the active domain of the data instance under the pointwise semantics [Ouaknine and Worrell, 2008]. Some use cases, algorithms, and implementations for MTL OMQs under the continuous semantics are discussed by [Brandt et al., 2018; Wang et al., 2022]. Finding a syntactical classification of MTL OMQs according to their data complexity/rewritability type under the pointwise semantics is substantially more challenging than in the LTL case [Ryzhikov et al., 2019]. The relevant complexity classes for answering MTL OMQs include (N)LOGSPACE, P and NP, which, apart from the three axes above, also depend on the type of intervals indexing the temporal operators, say semi-infinite (a,∞), punctual [a, a], or bounded [0, a). The target languages for rewritings include FO(DTC), FO(TC) with (deterministic) transitive closure, and datalog(FO).

If n-ary relations over the object domain need to be taken into account in ontologies and queries, the 1D OMQ languages mentioned above should be extended with appropriate DL or datalog constructs. The FO-rewritability results presented above are lifted, in some cases, to combinations of LTL with DL-Lite and instance temporal queries in [Artale et al., 2021a]. Other DL examples include atomic queries in the temporal extensions of EL [Guti´errez-Basulto et al., 2016]; CQs with guarded negation and metric temporal operators under the minimal-world semantics in the extension of ELH [Borgwardt et al., 2019]. Extensions of datalog by constraints over a time domain provide an alternative and well investigated approach to querying temporal data [Revesz, 1993; Kanellakis et al., 1995; Toman and Chomicki, 1998].

Acknowledgements

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