First-Order Rewritability of Temporal Ontology-Mediated Queries

1 Introduction

Ontology-based data access (OBDA), one of the most promising applications of description logics, has recently been touted as a key ingredient in data streammanagement systems [Calbimonte et al., 2012; Baader et al., 2013; ¨Ozc¸ep and M¨oller, 2014; Kharlamov et al., 2014]. Its role is to facilitate querying data streams from heterogeneous sensor networks (measuring temperature, vibration, wind speed and direction, blood pressure, etc.) in order to detect, analyse and predict certain events or situations. For example, we may want to detect areas of the country that have been hit by blizzards-severe snowstorms with low temperatures and strong winds for at least three hours-using the weather stations' sensors streaming raw data such as (sensorId, temperature, timestamp) [Zhang et al., 2012]. The OBDA component would give us an ontology, O, that defines a high-level vocabulary-possibly including the relation 'area x was hit by a blizzard at time t'-which is linked to the raw data by means of (say, R2RML) mappings. Given a query in the vocabulary of O such as ∃t Blizzard(x, t), the system would first rewrite the pair (O, ∃t Blizzard(x, t)), called a temporal ontology-mediated query (TOMQ), into a query over the original timestamped data and then evaluate it using standard relational or stream data management systems.

The OBDA scenario outlined above is similar to the classical one [Calvanese et al., 2007a]. An essential difference, however, is that nowwe query temporal data and therefore, require temporal constructs in the ontology and/or query languages, which, on the other hand, should not undermine the rewritability property of TOMQs. As temporal extensions of knowledge representation formalisms are notorious for their bad computational behaviour [Lutz et al., 2008], a first natural step could be to keep standard atemporal OBDA languages (e.g., OWL 2 QL or DL-Lite logics), assuming that ontology axioms hold at all moments of time, but add temporal constructs to queries. This approach was taken by [Guti´errez-Basulto and Klarman, 2012;

2Department of Computer Science 3Department of Computer Science

and Information Systems

Birkbeck, University of London, UK

Baader et al., 2013; Borgwardt et al., 2013; ¨Ozcep et al., 2013; Klarman and Meyer, 2014] and shown to preserve query rewritability. Note, however, that the inability to define temporal predicates such as Blizzard(x, t) in ontologies leaves the burden of encoding them within queries to the user, which goes against the OBDA paradigm. Moreover, natural queries such as 'check if a weather station has been serviced every 24 hours' are not expressible in these languages.

The first attempt to introduce linear-time temporal logic (LTL) operators to the TOMQs' ontologies was made by Artale et al. [2013b], who showed that the operators ✸F and ✸P (sometime in the future and past) on the left-hand side of DL-Lite axioms allow rewritings of conjunctive queries into the two-sorted first-order language FO(<) with variables of sorts 'object' and 'time' and an explicit temporal precedence relation <. On the other hand, it was observed that the nextand previous-time operators ©F and ©P-perhaps the most powerful and versatile temporal modelling constructs-do not support FO(<)-rewritability.

The aim of this paper is to launch a systematic investigation of rewritability of TOMQs with arbitrary temporal operators. Apart from FO(<), we consider two more target languages for rewritings: FO(<, +), which complements FO(<) with a ternary predicate PLUS for 'addition' and still ensures query evaluation in LOGTIME-uniform AC0 for data complexity; and monadic second-order logic MSO(<), which guarantees query evaluation over finite linear orders (flows of time) in NC1 ⊆ LOGSPACE for data complexity. Axioms of our ontologies are given in clausal normal form

where the λi are all either DL-Lite concepts or roles, possibly prefixed with the operators ©F , ©P , ✷F and ✷P (always in the future and the past). Let o ∈ {✷,©,✷©} and c ∈ {bool, horn, krom, core}. We denote by DL-Liteoc the temporal description logic with axioms of the form (1), where the λi can only use the (future and past) operators indicated in o, and m ≤ 1 if c = horn; n+m ≤ 2 if c = krom; n+m ≤ 2 and m ≤ 1 if c = core; and arbitrary n, m if c = bool. For example, the DL-Lite©horn axioms

SevereSnow ⊓ LowTemp ⊓ StrongWind ⊑ BlizzardCondition,

University of Liverpool, UK

where ©iF is a sequence of i-many ©F , define the temporal concept Blizzard (the concepts on the left-hand side of the second axiom are defined via mappings from the sensor data), while the DL-Lite©core axiom Scheduled ⊑ ©24 F Scheduled can be used to detect 'service every 24 hours' (see below).

The queries in our TOMQs range from atoms of the form A(x, t) or P(x, y, t), for A a concept and P a role name, in atomic TOMQs (or TOMAQs), to arbitrary positive temporal concepts and roles such as (Blizzard U(Rain⊔Flooding))(x, t) in instance TOMQs (TOMIQs), where U is the 'until' operator, and further to two-sorted FO-formulas built from positive temporal concepts and roles. It is well known that, due to the open-world semantics of OBDA, negation in queries results in non-tractable (often undecidable) query evaluation even in the atemporal case. In classical OBDA, a way to retain all FO-constructs in queries was proposed by Calvanese et al. [2007b] who interpreted them under an epistemic semantics. We follow in their footsteps: for example, the query Scheduled(x, t) ∧ ¬Serviced(x, t) returns weather stations x that are not known (or not certain) to have been serviced at scheduled times t. With this semantics, TOMQs cover all firstorder features of SPARQL 1.1 under the OWL 2 QL entailment regime [Kontchakov et al., 2014]. Although the variables in TOMQs range over the active domain, their positive temporal concepts can express (via qualified existential restrictions and role intersections) tree-shaped CQs with one answer variable.

To only focus on rewritability, we assume that data instances are given as finite ABoxes with timestamped atoms of the form A(a, n) and P (a, b, n), n ∈ Z (e.g., generated from streamed data via mappings and the window operator [Calbimonte et al., 2012]). We proceed in two steps. First, we investigate rewritability of TOMQs without roles, which can be regarded as LTL TOMQs. Using automata-theoretic techniques, we obtain the following rewritability classification:

∗ It is still open whether these can be improved to FO(<, +); all other results in the table are optimal.

In the second step, we reduce FO-rewritability of DL-Lite ✷© horn TOMQs to FO-rewritability of certain LTL ✷© horn TOMQs. In particular, we prove that all DL-Lite ✷ core TOMQs are FO(<)-rewritable, while DL-Lite©core TOMQs are FO(<, +)-rewritable. On the other hand, we show that some DL-Lite ✷ horn TOMQs are NC1 -hard for data complexity, and so they cannot be FOrewritable even using arbitrary numeric predicates. All omitted proofs can be found at tinyurl.com/q6ahvnt.

2 Temporal Ontology-Mediated Queries

First we remind the reader of basic DL-Lite logics [Calvanese et al., 2007a; Artale et al., 2009]. Their language contains object names a0, a1, . . . , concept names A0, A1, . . . , and role names P0, P1, . . . . Roles R and basic concepts B are defined as R ::= Pk | P - k and B ::= Ak | ∃R. For c ∈ {bool, horn, krom, core}, we denote by DL-Litec the description logic with concept and role inclusions of the form (1) such that the λi are all either basic concepts or roles. As usual, we assume that the empty ⊓ is ⊤ and the empty ⊔ is ⊥. Note that DL-Litehorn and DL-Litebool contain role inclusions with monotone Boolean operators.

In temporal DL-Lite, we also allow applications of the operators ©F , ©P , ✷F , ✷P to basic concepts and roles. For any o ∈ {✷,©,✷©}, DL-Liteoc is the temporal description logic with concept and role inclusions of the form (1), where each λi is a basic concepts or roles are (possibly) prefixed by a string of (future or past) operators indicated in o.

A DL-Liteoc TBox T (RBox R) is a finite set of DL-Liteoc concept (role) inclusions; O = T ∪R is a DL-Liteoc ontology. An ABox (or data instance), A, is a finite set of atoms of the form A(a, ℓ) and P (a, b, ℓ), where a, b are object names and ℓ ∈ Z. We denote by ind(A) the set of object names in A, by minA and maxA the minimal and maximal numbers in A, and set tem(A) = {n ∈ Z | min A ≤ n ≤ max A}. Without loss of generality, we assume that min A = 0 and max A ≥ 1.

A temporal interpretation is a pair I = (∆I , ·I(n) ), where ∆I ̸= ∅ and I(n) = (∆I , aI0 , . . . , AI(n) 0 , . . . , P I(n) 0 , . . . ) is a standard DL interpretation for each time instant n ∈ Z, that is, aIi ∈ ∆I , AI(n) i ⊆∆I and P I(n) i ⊆∆I ×∆I . Thus, we assume that the domain ∆I and the interpretations aIi ∈ ∆I of the object names are the same for all n ∈ Z. The DL and temporal constructs are interpreted in I(n) as follows:

and symmetrically for ✷P and ©P ; as usual, ⊥ is interpreted by ∅ and ⊤ by ∆I for concepts and by ∆I ×∆I for roles. Concept and role inclusions are interpreted in I globally in the sense that (1) holds in I if ⋂ λI(n) i ⊆ ⋃ λI(n) j for all n ∈ Z. We call I a model of (O,A) and write I |= (O,A) if all concept and role inclusions from O hold in I, and aI ∈ AI(n) for A(a, n) ∈ A, and (aI , bI ) ∈ P I(n) for P(a, b, n) ∈ A.

Remark 1. Note that the LTL operators ✸F , ✸P , U and S ('since') can be expressed in DL-Lite ✷© bool [Fisher et al., 2001; Artale et al., 2013a]. DL-Lite ✷ horn extends the ontology language TQL of Artale et al. [2013b] as ✸PA ⊑ B is equivalent to A ⊑ ✷FB. Note also that each of our ontology languages can say that a role or basic concept λ is expanding (using λ ⊑ ©F λ in DL-Lite©core and λ ⊑ ✷F λ in DL-Lite ✷ core ) or rigid (using, in addition, λ ⊑ ©P λ and λ ⊑ ✷P λ).

To query temporal ontologies with data, we suggest the following language inspired by the recently standardised SPARQL 1.1 entailment regimes (www.w3.org/TR/sparql11entailment); cf. also [Motik, 2012; Gutierrez et al., 2007].

Positive temporal concepts κ and positive temporal roles ϱ are defined by the grammars

where op ranges over ©F , ✸F , ✷F , ©P , ✸P , ✷P and op′ over U, S. The extensions of κ and ϱ in a temporal interpretation I are computed using the definition above and the following clauses (given only for κ and the future-time operators):

A DL-Liteoc ontology-mediated instance query (TOMIQ) is a pair of the form (O, κ) or (O, ϱ), for a DL-Liteoc ontology O. A certain answer to (O, κ) over an ABox A is a pair (a, ℓ) such that a ∈ ind(A), ℓ ∈ tem(A) and aI ∈ κI(ℓ) for every I |= (O,A). A certain answer to (O, ϱ) over A is a triple (a, b, ℓ) with a, b ∈ ind(A), ℓ ∈ tem(A) and (aI , bI ) ∈ ϱI(ℓ) for every I |= (O,A). Let ans(O, κ,A) denote the set of certain answers to (O, κ) over A, and similarly for (O, ϱ).

As a technical tool in our proofs, we also require 'certain answers' in which ℓ can range over the whole Z rather than only the active domain tem(A); we denote the set of such certain answers over A and Z by ansZ (O, κ, A) or ansZ (O, ϱ, A).

Example 2. Let O={©PA ⊑ B, ©PB ⊑ A}, A={A(a, 0)} and κ = ©2 F B. Then aI ∈ BI(2n+1) , for any n ≥ 0 and I |= (O,A). So, ansZ (O, κ,A) = {(a, 2n + 1) | n ≥ 0} but ans(O, κ, A) = {(a, 1)} since tem(A) = {0, 1}.

Given an ABox A and convex D ⊇ tem(A), denote by SDA the two-sorted structure with object domain ind(A) and temporal domain D such that SDA |= A(a, ℓ) iff A(a, ℓ) ∈ A and SDA |= P(a, b, ℓ) iff P(a, b, ℓ) ∈ A, for concept and role names A and P . Let q = (O, κ) be a TOMIQ and Φ(x, t) a constant-free FO-formula whose signature is the concept and role names in q, < and =. We call Φ(x, t) an FO(<)-rewriting of q if, for any ABox A, a ∈ ind(A) and ℓ ∈ tem(A), we have (a, ℓ) ∈ ans(q,A) iff S tem(A) A |= Φ(a, ℓ). If Φ(x, t) also uses the predicate PLUS(k, n1, n2) (for k = n1 +n2) then it is called an FO(<,+)-rewriting of q. FO-rewritings of TOMIQs (O, ϱ) are defined analogously. Note that FOformulas using < and PLUS as built-in predicates can be evaluated by standard relational or stream database management systems, and so are an appropriate target for query rewriting.

Example 3. Consider q = (O, A), where O is the same as in Example 2. It is not hard to see that

is an FO(<,+)-rewriting of q, where t - s = 2n ≥ 0 stands for ∃k (PLUS(k, n, n) ∧ PLUS(t, s, k) ∧ (k ≥ 0)) and t-s = 2n+1 ≥ 0 is defined similarly. (The constant 0 is obviously definable.) Note that q is not FO(<)-rewritable since properties such as 't is even' are not definable by FO(<)-formulas [Libkin, 2004].

Example 4. For a word e = (e0, . . . , en-1) ∈ {0, 1}n , take Ae = {B0(a, n)} ∪ {Aei (a, i) | i < n } and let O′ contain

One can check that (a, 0) is a certain answer to (O′ , B0) over Ae iff the number of 1s in e is even (parity). It follows that (O′ ,B0) is not FO-rewritable even using arbitrary numeric predicates [Arora and Barak, 2009].

If we replace S tem(A) A in the definition above withSZA, then we call Φ(x, t) an FOZ (<)- or FOZ (<,+)-rewriting of q. Finding FOZ -rewritings is often a first step in the construction of FO-rewritings, which are usually more involved.

Example 5. Suppose O = {A ⊑ ©2 F A, B ⊑ ©3 F B} and κ = ✸F (A ⊓ B). Then

is an FOZ (<,+)-rewriting of (O, κ) but not an FO(<,+)- rewriting because s can be outside the active domain tem(A).

A temporal ontology-mediated query (TOMQ) is a pair (O, ψ), where ψ is an FO-formula built from atoms κ(x, t), ϱ(x, y, t) and t < t′ , with κ and ϱ being any positive temporal concept and role, x and y object variables, and t and t′ temporal variables. Given an ABox A, (O, ψ) is evaluated over the two-sorted structure with the object domain ind(A) and the temporal domain tem(A), where κ(a, ℓ) holds true iff (a, ℓ) ∈ ans(O, κ, A), and likewise for ϱ(a, b, ℓ). Thus, similarly to the SPARQL 1.1 entailment regime, we interpret the DL and temporal constructs of TOMIQs in arbitrary temporal models (over Z), while the object and temporal variables of TOMQs range over the active domains only.

Example 6. Suppose O = {Scheduled ⊑ ©24 F Scheduled}, ψ(x, t) = Scheduled(x, t) ∧ ¬Serviced(x, t) and A contains Scheduled(a, 0) as well as entries Serviced(a, ℓ) made by a serviceman. Then (O, ψ) returns all pairs (a, 24n) such that 24n ≤ maxA and there is no entry Serviced(a, 24n) in A.

FO-rewritings of TOMQs are defined similarly to TOMIQs. We generalise [Calvanese et al., 2007b]:

Theorem 7. If all constituent TOMIQs of a TOMQ q are FO(<)- or FO(<,+)-rewritable, then q is also FO(<)- or, respectively, FO(<, +)-rewritable.

From now on we only focus on rewritability of TOMIQs.

3 Rewriting LTL TOMQs

We begin our study of FO-rewritability by considering ontologies without role names and assuming that all ABoxes contain a single object name, say a. To simplify notation, we will omit a from the ABox assertions, interpretations, certain answers, etc., and write A(ℓ) instead of A(a, ℓ) and assume that answers to TOMIQs are subsets of tem(A) rather than {a} × tem(A), and that FO-rewritings Φ(x, t) are one-sorted FO-formulas ϕ(t). Ontologies in this restricted language can be regarded as formulas of the propositional temporal logic LTL given in clausal normal form (1), and so we denote the corresponding restrictions of DL-Liteoc by LTLoc . In this context, positive temporal concepts are simply negation-free LTL-formulas.

As shown by Example 4, some LTL©horn TOMAQs cannot be FO(<,+)-rewritable. On the other hand, relying on the well-known fact that the semantics of temporal formulas can be encoded by monadic second-order (MSO) formulas (built from atoms of the form A(t), t = t′ and t < t′ using the Booleans, first-order quantifiers ∀t, ∃t and second-order quantifiers ∀A and ∃A), one can prove the following:

Theorem 8. All LTL ✷© bool TOMQs are MSO(<)-rewritable.

It follows that, for any LTL ✷© bool TOMQ q, one can build an NFA accepting an ABox A and ℓ ∈ tem(A) written on its tape iff ℓ ∈ ans(q,A) [Straubing and Weil, 2010], and that the evaluation problem for q is in NC1 for data complexity [Ladner and Fischer, 1980]. On the other hand, we also have:

Theorem 9. There exist an LTL©horn TOMAQ and LTL ✷ krom and LTL©krom TOMIQs that are NC1 -hard for data complexity; in particular, they are not FO-rewritable even with arbitrary numeric predicates.

Proof sketch. It is known that there exist NC1 -complete regular languages [Barrington et al., 1992]. Given an NFA A and input a = a0 . . . an-1, we take concept names Aa and Bq for tape symbols a and states q of A, and then set Aa = {Bq1 (n)}∪{Aai (i) | i < n }, where q1 is the accepting state, and O = {©FBq′ ⊓ Aa ⊑ Bq | q →a q′ }. Then A accepts a iff 0 ∈ ans(O,Bq0 ,Aa), for the initial state q0. Next, let O′ containNq ⊓Bq ⊑ ⊥ and⊤ ⊑ Bq ⊔Nq, for each state q, and let κ = Bq0 ⊔ ⊔q→aq′ ✸P✸F (©FBq′ ⊓Aa ⊓Nq). Then A accepts a iff 0 ∈ ans(O′ , κ, Aa). q

Next, we show the FO(<)- and FO(<, +)-rewritability results from the table in the introduction. To begin with, we focus on temporal ontology-mediated atomic queries (TOMAQs) of the form (O, A), where A is a concept name.

Theorem 10. Any LTL©krom TOMAQ is FO(<,+)-rewritable. Proof sketch. Suppose q = (O,A) is an LTL©krom TOMAQ. By a literal, L, we mean a concept name in q or its negation. We use ©nL in place of ©n F L if n > 0, L if n = 0, and ©-n P L if n < 0. We write O |= L ⊑ ©kL′ if I |= L ⊑ ©kL′ in every model I of O. For any ABox A consistent with O, we have:

Given literals L and L′ , let AL,L′ be an NFA whose tape alphabet is {0}, the states are the literals, with L initial and L′ accepting, and whose transitions are of the form L1 →0 L2, for O |= L1 ⊑ ©L2 (without loss of generality we assume that O does not contain nested ©). It is easy to see that AL,L′ accepts 0k (k > 0) iff O |= L ⊑ ©kL′ . By [Chrobak, 1986; To, 2009], there are N = O(|AL,L′ |2 ) arithmetic progressions ai + biN = {ai + bi · m | m ≥ 0}, 1 ≤ i ≤ N, such that 0 ≤ ai, bi ≤ |AL,L′ | and AL,L′ accepts 0k iff k ∈ ai + biN for some i, 1 ≤ i ≤ N. These progressions give rise to the FO-rewriting we need. To illustrate, suppose q = (O, A) and

The NFA AB,A (more precisely, the states reachable from B) is shown below, and for L ∈ {A, C, D, E}, AL,A is the same NFA but with the initial state L. It is readily seen that AB,A accepts 0k iff k ∈ 3 + 2N, which can be described by the formula

where with a = 3, b = 2, t - s = a + bn ≥ 0 is defined as in Example 3. Similarly, for AE,A, we have a = b = 2. (Note that in general more than one progression is needed to characterise automata AL,A.) To obtain an FO(<,+)- and FOZ (<, +)-rewriting of q, we take a disjunction of ϕL,A(t), for all literals L. q

Theorem 11. Any LTL ✷ bool TOMAQ is FO(<)-rewritable. Proof sketch. Given an LTL ✷ bool -ontology O, we construct an NFA A that takes as input an ABox A written as the word A0, . . . ,Ak, where k = maxA and Ai = {A | A(i) ∈ A}. Let Σ be the set of temporal concepts in O and their negations. Each state of A is a maximal set S ⊆ Σ that is consistent with O; let S be the set of all such states. For S, S′ ∈ S and a tape symbol (set of concept names) X, we set S →X S′ just in case X ⊆ S′ , ✷Fβ ∈ S iff β,✷Fβ ∈ S′ , and ✷Pβ ∈ S′ iff β, ✷Pβ ∈ S. A state S ∈ S is accepting if A has an infinite 'ascending' chain S →∅ S1 →∅ . . . ; S is initial if A has an infinite 'descending' chain · · · →∅ S1 →∅ S. The NFA A simulates O in the following sense: for any ABox A, concept name A and ℓ ∈ Z, we have ℓ ∈ ansZ (O,A,A) iff A does not contain an accepting path S0 →X1 · · · →Xm Sm (S0 initial and Sm accepting) such that A /∈ Sℓ, Xi+j = Aj if 0 ≤ j ≤ k, and Xj = ∅ otherwise, for some 0 < i ≤ m- k. Define an equivalence relation, ∼, on S by taking S ∼ S′ iff S = S′ or A has a cycle with both S and S′ . Let [S] be the ∼-equivalence class of S. One can check that S →X S′ implies S1 →X S′ , for any S1 ∈ [S]. Let A′ be the NFA with states [S], for S ∈ S, and transitions [S] →X [S′ ] iff S1 →X S′1 , for some S1 ∈ [S] and S′1 ∈ [S′ ]. The initial (accepting) states of A′ are all [S] with initial (accepting) S. The NFA A′ also simulates O and contains no cycles other than trivial loops, which makes it possible to express the simulation condition by an FO(<)-formula. For example, A′ for O = {A ⊑ ✷PB, ✷PB ⊑ C} is shown below, where all states are initial and accepting, and negated concepts omitted:

2{A,B,C}

Let q = (O,C). Take all accepting paths π in A′ with pairwise distinct states at least one of which has a set without C. Thus, for π = [S1] →{A} [S2] →∅ [S3], a set in [S3] has no C, and the simulation condition for π, which makes sure that ¬C holds at t, can be written as

where sym{A}(t) = A(t) ∧ ¬B(t) ∧ ¬C(t) and sym∅(t) = ¬A(t) ∧ ¬B(t) ∧ ¬C(t) define transitions →{A} and →∅ in π, and loop[S1] = ⊤, loop[S3] = ¬A(t) and loop[S2] = ⊥ say that [S1] and [S3] have loop transitions with any input and any input but A, respectively, but [S2] has no loop. To obtain an FO(<)- and FOZ (<)-rewriting of q, we take a disjunction of such formulas for all accepting paths π in A′ and negate it. q

FO-rewritings of LTL©core and LTL ✷ horn TOMIQs can now be constructed by induction on the structure of concepts using the fact that any consistent (O,A) in these languages has a single canonical model providing answers to all TOMIQs with the given ontology (it will be formally defined in Section 4). For example, an FOZ (<)-rewriting of (O, A1 U A2) is defined as

where ϕAi (t) is an FOZ (<)-rewriting of (O, Ai). Note, however, that such FOZ (<)-rewritings are not in general FO(<)- rewritings as they may refer to time instants outside the active domain tem(A); cf. Example 5. To cope with this problem, we require (constant-free) sentences ϕkA, for any concept A and k ̸= 0, such that, for every ABox A consistent with O,

The existence of such sentences, called witnesses for (O, A) and k, follows from the proofs of Theorems 10 and 11. Instead of (2), we can now take the infinite 'formula'

It turns out that we can make it finite by observing that the canonical models are ultimately periodical with at most exponential period (see the full paper). Thus, we obtain

4 OBDAwith Temporal DL-Lite

Now we transfer the rewritability results obtained above to certain DL-Lite ✷© horn TOMIQs. To simplify presentation, we assume that our ontologies do not contain nested temporal operators and ⊥ (and so they are always consistent with any data); a proof without this assumption is given in the full paper.

Observe first that rewritability of TOMIQs of the form (O, ϱ) can be easily reduced to rewritability of LTL ✷© horn TOMIQs because only the RBox R in O has to be taken into account. We assume that with every role inclusion (e.g., ✷FR⊓©FQ- ⊑ T ) the RBox also contains the corresponding inclusion for the inverse roles (that is, ✷FR- ⊓©FQ ⊑ T -). We treat the roles in R and ϱ as concept names and denote the resulting LTL ✷© horn TOMIQ by (R∗ , ϱ∗ ). If it has an FOrewriting ϕR∗, ϱ∗(t), then we replace every P(s) in it with P(x, y, s), every P -(s) with P(y, x, s), and denote the resulting FO-formula by ΦO,ϱ(x, y, t).

Theorem 13. For every DL-Lite ✷© horn TOMIQ (O, ϱ) with O = T ∪R, if ϕR∗, ϱ∗(t) is an F-rewriting of (R∗ , ϱ∗ ) then ΦO,ϱ(x, y, t) is an F-rewriting of (O, ϱ), where F is FO(<) or FO(<, +).

However, this simple reduction to LTL does not work for TOMIQs of the form (O, κ). The main reason is that the RBox in O can have a strong impact on its TBox.

Example 14. Let O = T ∪ R, T = {B ⊑ ∃R, ∃Q ⊑ A} and R= {R ⊑ ©FQ}. It is not hard to see that the following is an FO(<)-rewriting of (O, A):

It can also be constructed by treating T as an LTL©core -ontology, but only if the connection axiom ∃R ⊑ ©F∃Q is added to T .

To understand what connection axioms are required for any given DL-Lite ✷© horn TOMIQ (O, κ), we first define a canonical model (or chase) for (O,A), which will also be used to prove our main Theorems 17 and 21. Let C be a set of atoms of the form A(a, n), ∃R(a, n) and R(a, b, n), possibly prefixed by temporal operators and such that P(a, b, n) ∈ C iff P -(b, a, n) ∈ C. Denote by cl(C) the result of applying non-recursively the following rules to (the same) C:

• if R(a, b, n) ∈ C then we add ∃R(a, n) to C;
• if (λ1 ⊓ · · · ⊓ λk ⊑ λ) ∈ O and λi(a, n) ∈ C, for all i = 1, . . . , k, then we add λ(a, n) to C;
• if ∃R(a, n) ∈ C then we add R(a, aRn , n) to C, where aRn is a new object name (called a witness for ∃R(a, n));
• if ✷Fλ(a, n) ∈ C then add λ(a,m) to C for all m > n;
• if λ(a,m) ∈ C for all m > n, then add ✷Fλ(a, n) to C;
• if ©Fλ(a, n) ∈ C then add λ(a, n+1) to C;
• if λ(a, n) ∈ C then add ©Fλ(a, n-1) to C;

and symmetrical rules for ✷P and ©P . Then we set cl0 (C) = C and, for any successor ordinal ξ + 1 and limit ordinal ζ,

Let N be the number of temporal operators in O. We regard CO,A = clω·N (A) as an interpretation whose domain ∆CO,A comprises ind(A) and the witnesses aRn and the interpretation function is defined by taking aCO,A = a, for a ∈ ind(A), and a ∈ SCO,A(ℓ) iff S(a, ℓ) ∈ CO,A, for concept or role names S. We call CO,A the canonical model of (O, A).

Example 15. Suppose that O = {A ⊑ ✷F∃P, ✷F∃R ⊑ B, P ⊑ ©FR, R ⊑ ©FR} and A = {A(a, 0)}. The canonical model of (O,A) is depicted below:

Theorem 16. For any DL-Lite ✷© horn TOMIQs (O, κ) and (O, ϱ), any ABox A, a, b ∈ ind(A) and ℓ ∈ Z, we have

Let (O, κ) be a DL-Lite ✷© horn TOMIQ with O = T ∪ R. For any role R in O, we consider the canonical model CR,{R(a,b,0)} and denote by rRn , n ∈ Z, the set of roles Q in O such that Q(a, b, n) ∈ CR,{R(a,b,0)}. It is known from temporal logic [Gabbay et al., 1994] that there are positive numbers nr, nl, kr, kl = O(2|R| ) such that

We take, for each R and 0 ≤ i ≤ nr +kr, fresh concept names Di and add to T the concept inclusions (cf. Example 14):

and symmetrical inclusions for -nl - kl ≤ i ≤ 0 . Denote by T ∗ the LTL ✷© horn TBox obtained from T by replacing the basic concepts in it with concept names.

Theorem 17. Suppose (O, κ) is a DL-Lite ✷© horn TOMIQ and O = T ∪ R with T supplemented by (con). If there exist F-rewritings of (T ∗, A) and (R∗ , P), for every concept name A and role name P in O, then (O, κ) is F-rewritable, where F is FO(<) or FO(<, +)

We illustrate the rather involved proof of this theorem (given in the full paper) by an example.

Example 18. Let O = T ∪R, where T = {B ⊑ ∃R} and R = {R ⊑ ✷F S-}, and q = (O, κ) with κ = ∃R.✸F ∃S.A. By Theorem 16, certain answers to q over an ABox A are all a ∈ ind(A) and n ∈ tem(A) with a ∈ κCO,A(n) . Witnesses for ∃R in κ are either located in ind(A) or of the form aRn if CO,A contains B(a, n), and so R(a, aRn , n), in which case there must also be some m > n such that A(a, m) ∈ CO,A:

This observation gives the following inductive rewriting:

Since the connection axioms (con) belong to DL-Lite©core , as a consequence of Theorems 12 (i), 13 and 17 we obtain:

On the other hand, the following unexpected result shows, in particular, that (con) cannot be expressed in DL-Lite ✷ horn :

Theorem 20. There is a DL-Lite ✷ horn TOMAQ which is NC1 - hard for data complexity; in particular, it is not FO-rewritable even using arbitrary numeric predicates.

Proof sketch. We first show non-rewritability by modifying the construction of Example 4. Consider the RBox R with

and the TBox T with

where k = 0, 1. For e = (e0, . . . , en-1) ∈ {0, 1}n , we take Ae = {B0(a, n)} ∪ {Aei (a, i) | i < n}. Then (a, 0) is a certain answer to (T ∪R,B0) over Ae iff the number of 1s in e is even-see the picture below and note that ∃Sk(a, n) always generates a fresh witness aSn k :

The same idea can be used to simulate arbitrary NFAs and show NC1 -hardness of DL-Lite ✷ horn TOMAQs; see Thm. 9. q

Thus, Theorem 12 (ii) cannot be lifted to DL-Lite ✷ horn . In the proof above, using Horn role inclusions with ✷F and ✷P , we have encoded ©F on concepts: T ∪R |= ©F∃Sk ⊑ ∃Rk.

We now give a sufficient condition under which (con) can be expressed in DL-Lite ✷ core . Call an RBox Rmonotone if, for any roles R, Q in it, Q ∈ rRn and n ̸= 0 imply Q ∈ rRm for all m ≥ n or all m ≤ n. Clearly, for a monotone R and any roles R and Q in it, one of the four options holds:

• (ii) there is mr ∈ Z such that Q ∈ rRn iff mr ≤ n or n = 0,
• (iii) there is ml ∈ Z such that Q ∈ rRn iff n ≤ml or n = 0,
• (iv) there are ml,mr ∈ Z, ml ≤ mr, such that Q ∈ rRn iff n ≤ ml or mr ≤ n or n = 0.

We encode (i) by ∃R ⊑ ∃Q; (ii) by the following:

with fresh D; (iii) is symmetrical; (iv) combines (ii) and (iii). The set of all such connection axioms is denoted by (con′ ).

Theorem 21. Theorem 17 holds true for O = T ∪ R with monotone R and (con′ ) in place of (con).

One can show that all DL-Lite ✷ core RBoxes as well as DL-Lite ✷ horn RBoxes without ✷-operators on the left-hand side of role inclusions are monotone. We denote by DL-Lite mon✷ horn the fragment of DL-Lite ✷ horn whose role inclusions do not contain negative occurrences of ✷F and ✷P ; this language can be regarded as an extension of TQL [Artale et al., 2013b].

Corollary 22. All DL-Lite ✷ core as well as DL-Lite mon✷ horn TOMIQs are FO(<)-rewritable.

5 Conclusions

We have developed a two-step approach to analysing FOrewritability of temporal ontology-mediated queries. First, we classified the FO-rewritability properties of TOMQs in fragments of LTL. Second, we proved two general transfer theorems identifying conditions under which FO-rewritability is preserved for combinations of LTL with DL-Lite. The transfer results show that, although temporal DLs are notorious for their high complexity, one can nevertheless find large 'islands' of tractable and expressive TOMQs. Many interesting and challenging research questions can be tackled based on the results of this paper:

• complexity and succinctness of rewritings (the size of our rewritings of TOMAQs varies from polynomial for LTL©krom to single, double and triple exponential in the size |T | of the TBox T for various temporalised versions of DL-Lite; rewritings of TOMQs are of size S|q| and S|q||T | for, respectively, LTL and DL-Lite ontologies, where |q| is the size of the query and S the size of the rewritings for the underlying TOMAQs);
• generalising our FO rewritings of TOMIQs to (twosorted) CQs using the methods of [Artale et al., 2013b];
• data complexity of evaluating DL-Lite ✷© horn TOMQs; based on our proofs, we conjecture that it is NC1 - complete;
• extension of the transfer results for Horn logics to ⊔ and ¬, possibly via a non-uniform analysis;
• our rewriting algorithms need to be optimised and evaluated in real-world applications.