Temporal OBDA with LTL and DL-Lite Alessandro Artale1, Roman Kontchakov2, Alisa Kovtunova1, Vladislav Ryzhikov1, Frank Wolter3 and Michael Zakharyaschev2 1 Faculty of Computer Science, Free University of Bozen-Bolzano, Italy 2 Department of Computer Science and Information Systems Birkbeck, University of London, U.K. 3 Department of Computer Science, University of Liverpool, U.K. Abstract. We investigate various types of query rewriting over ontologies given in the standard temporal logic LTL as well as combinations of LTL with DL-Lite logics. In particular, we consider FO(<)-rewritings that can use the temporal precedence relation, FO(<, +)-rewritings that can also employ the arithmetic predicate PLUS, and rewritings to finite automata with data given on the automaton tape. 1 Introduction Ontology-based data access (OBDA), one of the most promising applications of description logics, has recently been extended to temporal ontologies and data. Motivated by applications in temporal data management, data stream management and monitoring in context-aware systems [11, 4, 7, 3, 15], a few approaches to temporal OBDA have been suggested. In all of them, data is stored in an ABox as timestamped assertions. It is assumed to be incomplete and supplemented by an ontology representing information about the domain or system under consideration. A user can access the data by means of queries in the vocabulary of the ontology that refer to time via either the temporal precedence relation directly or standard temporal operators from logics such as LTL. Within this framework, a fundamental challenge is to minimally restrict the use of temporal constructs in ontologies and queries so that query answering is tractable (in data complexity) and can ideally be delegated to existing temporal or stream data management tools after query rewriting into an appropriate query language. For example, [4, 7] have explored the data complexity of query answering and the possibility of first-order rewritability for standard ontologies, which do not employ any temporal constructs, and conjunctive queries extended with the temporal operators of LTL. The only temporal aspect the ontology can represent in this approach is that some roles and concepts can be declared rigid (time-invariant), which has a strong impact on the complexity of query answering. An extension of SPARQL with temporal operators was designed in [15]. In contrast, the aim of [3] was to identify most expressive combinations of the ontology language OWL 2 QL (and other logics of the DL-Lite family) with LTL that would ensure rewritability of temporal ontologies and conjunctive queries with timestamped atoms into first-order queries with the temporal precedence relation <. One such combination, TQL, allows the temporal operators 3P (sometime in the past) and 3F (sometime in the future) in axioms of the form 3P signsForMU u 3F endOfContract v onMUcontract, (1) saying that since the signing of a contract with Manchester United and until its end, one is contracted to Manchester United. We can then use the query  q(x) = ∃y, t (n1 ≤ t ≤ n2 ) ∧ Striker(x, t) ∧ onMUcontract(x, y, t) to find MU strikers in the time interval [n1 , n2 ]. It was also observed that axioms with the next- and previous-time operators F and P such as ≤21 HamstringPulled v F Injured, saying that if a player pulls his hamstring then he is injured for at least three weeks, can ruin FO(<)-rewritability. It was conjectured, however, that the addition of the operations + and × could be enough to guarantee rewritability in this case. In this paper, we launch a more systematic investigation of various types of query rewritability over temporal extensions of DL-Lite logics. To begin with, we consider ‘ontologies’ formulated in pure LTL, which is interpreted over the timeline (Z, <), and ‘data instances’ with atoms of the form p(n), where p is a propositional variable and n a moment of time in Z. Ontology axioms in this case are of the form 2 ∗ ϕ, where 2 ∗ is the temporal operator ‘always’ and ϕ is any LTL-formula. Our initial observation is that any FO-query q with atoms p(τ ), τ < τ 0 and τ = τ 0 (where τ , τ 0 are variables or constants from Z) and any LTL ontology T can be ‘rewritten’ to a nondeterministic finite automaton (NFA) that computes answers to (T , q) over any data instance given on the automaton tape. In complexity-theoretic terms, this means that the entailment problem for such ontology-mediated queries is in the class NC1 for data complexity. We then investigate rewritability of two types of FO-queries over ontologies given in the fragments of LTL that have been identified in [2]. More specifically, we consider atomic queries (AQs) as well as positive existential queries that can also use a built-in successor relation over Z (UCQ+ , for short). The fragments from [2] operate with LTL-formulas in clausal normal form 2 ∗ (¬λ1 ∨ · · · ∨ ¬λn ∨ λn+1 ∨ · · · ∨ λn+m ), (2) where the temporal literals λi are defined by the grammar λ ::= ⊥ | p | F λ | P λ | 2F λ | 2P λ. (3) (Here 2F and 2P are the operators ‘always in the future’ and ‘always in the past’.) Similarly to [10], one can show that any LTL-ontology can be transformed to clausal normal form. For example, axiom (1) can be replaced by three axioms signsForMU v 2F B, endOfContract v 2P E, B u E v onMUContract with fresh concepts B and E. Borrowing the terminology from [1], we distinguish four types of clauses ¬λ1 ∨ · · · ∨ ¬λn ∨ λn+1 ∨ · · · ∨ λn+m in (2): bool clauses with arbitrary n and m; horn clauses with m ≤ 1; krom clauses with n + m ≤ 2; and core clauses with n + m ≤ 2 and m ≤ 1. We consider 12 fragments of LTL denoted by LTL2 2 α , LTLα and LTLα , where α ∈ {bool, horn, krom, core} indicates the type of clauses and the superscript indicates the temporal operators that can be used in the literals λ in the clauses of the fragments. (For instance, LTLcore contains formulas in clausal normal form with core clauses whose literals can only contain F and P .) The obtained results are summarised in the table below: LTL2 α LTLα LTL2 α AQ UCQ+ AQ UCQ+ AQ UCQ+ bool FO(<) NFA NFA NFA NFA NFA horn FO(<) FO(<) NFA NFA NFA NFA krom FO(<) NFA FO(<, +) NFA ≤ NFA NFA core FO(<) FO(<) FO(<, +) FO(<, +) ≤ NFA ≤ NFA Thus, if only the operators 2F and 2P can be used in ontology axioms, then ontology-mediated UCQ+ s are rewritable to FO(<)-queries for all Horn ontologies. If the operators F and P are allowed then in the best case we can only have FO(<, +)-rewritings, which use < and +. (By ‘≤ NFA’ we indicate that the exact complexity is still unknown.) We then ‘lift’ these rewritability results to the temporal description logics 2 T2 DL-Liteflat flat horn and T DL-Litecore whose concept and role inclusions are LTLhorn and LTLcore clauses with concepts or roles in place of propositional variables and without ∃R on the right-hand side (we impose this restriction to focus on the temporal aspects of query rewriting). We prove that temporal UCQ+ s over T2 DL-Liteflat flat horn -ontologies are FO(<)-rewritable, while over T DL-Litecore - + ontologies they are FO(<, +)-rewritable. We also show that the UCQ -entailment problem over T2 DL-Liteflat horn -ontologies, which do not contain role inclusions, is NC1 -complete for data complexity. 2 OBDA with LTL We begin by considering the propositional temporal logic LTL over the flow of time (Z, <). LTL-formulas are built from propositional variables P = {p0 , p1 , . . . }, propositional constants > and ⊥, the Booleans ∧, ∨, → and ¬, and the temporal operators: 2∗ (always), 3∗ (sometime), S (since) and U (until), 3P (sometime in the past) and 3F (sometime in the future), 2P (always in the past) and 2F (always in the future), P (in the previous moment) and F (in the next moment). A temporal interpretation, I, defines a truth-relation, |=, between moments of time n ∈ Z and propositional variables pi . We write I, n |= pi to indicate that pi is true at n in I. This truth-relation is extended to all LTL-formulas in the following way (the Booleans are interpreted as expected): – I, n |= 2 ∗ ϕ iff I, k |= ϕ, for all k ∈ Z, – I, n |= 3 ∗ ϕ iff I, k |= ϕ, for some k ∈ Z, – I, n |= ϕ U ψ iff there is k > n with I, k |= ψ and I, m |= ϕ, for n < m < k, – I, n |= 2F ϕ iff I, k |= ϕ, for all k > n, – I, n |= 3F ϕ iff I, k |= ϕ, for some k > n, – I, n |= F ϕ iff I, n + 1 |= ϕ, and symmetrically for the past-time operators. (Note that the interpretation of U and S only involves moments of time that are ‘strictly’ in the future and, respectively, past; all other temporal operators are expressible via such S and U.) An LTL-ontology, O, is a finite set of LTL-formulas of the form 2 ∗ ϕ. With each p ∈ P we associate a unary predicate over Z, also denoted p. A data instance is a finite set, D, of atoms of the form p(`) with p ∈ P and ` ∈ Z. We denote by min D (max D) the minimal (maximal) number occurring in D and set ∆D = {` | min D ≤ ` ≤ max D}. To simplify presentation, we assume in this paper that min D = 0 and max D ≥ 1. A temporal knowledge base (KB) is a pair K = (O, D). We call an interpretation I a model of K and write I |= K if I, n |= ϕ, for all 2∗ ϕ in O and n ∈ Z, and I, ` |= p, for all p(`) ∈ D. A temporal first-order query (FOQ) is any FO(<)-formula, q(t), built from atoms pi (τ ), τ = τ 0 or τ < τ 0 , where τ and τ 0 are temporal terms (individual variables or constants from Z). Although the successor relation S(τ, τ 0 ) (saying that τ 0 = τ + 1) is expressible in this language, we assume that it can be used as a basic atom. The free variables t of q(t) are the answer variables of q; if there are no answer variables, q is called Boolean. A union of conjunctive queries (or UCQ+ , with + indicating that we can use the successor relation) is a disjunction of FOQs of the form ∃s ϕ(s, t), where ϕ is a conjunction of atoms. Finally, an atomic query (or AQ) takes the form pi (τ ), for a temporal term τ . A certain answer to a FOQ q(t) with t = t1 , . . . , tm over a KB (O, D) is any tuple ` = `1 , . . . , `m of elements in ∆D such that, for every model I of (O, D), we have I |= q(`) regarding I as a first-order structure; in this case we write O, D |= q(`). We refer to the problem ‘O, D |= q?’, where q is a Boolean FOQ, as FOQ-entailment over temporal ontologies. q,O Let q(t) be a FOQ and O an LTL-ontology. Denote by ID the finite first- q,O q,O order structure defined as follows. The domain ∆D of ID is the minimal closed interval in Z that contains ∆D as well as some fixed integers that only depend on q and O (for example, all ` ∈ / ∆D occurring in q should be included into ∆q,O D ). For any ` ∈ ∆ q,O D , we set q,O ID |= p(`) iff p(`) ∈ D. We also assume that the binary relations <, = and S and ternary relation PLUS are interpreted over ∆q,O D in a natural way (e.g., PLUS(n, m, k) is true iff n = m + k). If we extend q,O the domain of ID to Z, then the resulting structure is denoted by ID Z . 0 A FOQ q (t) is an FO(<)-rewriting of q(t) and O if, for any data instance D q,O and any tuple ` from ∆D , we have O, D |= q(`) iff ID |= q 0 (`). If we allow the 0 use of PLUS in q (t), then it is called an FO(<, +)-rewriting of q(t) and O. Example 1. Consider the ontology O = {2 ∗ ( P p → q), 2 ∗ ( P q → p)}. Then ∃s, n [(p(s) ∧ (t − s = 2n ≥ 0)) ∨ (q(s) ∧ (t − s = 2n + 1 ≥ 0))] is an FO(<, +)- rewriting of the AQ p(t) and O, where t − s = 2n ≥ 0 is a shortcut for ∃n2 (PLUS(n2 , n, n) ∧ PLUS(t, s, n2 ) ∧ (n2 ≥ 0)) and t − s = 2n + 1 ≥ 0 is defined similarly. However, p(t) and O do not have an FO(<)-rewriting because properties of numbers such as ‘t is even’ are not expressible by FO(<)-formulas [14]. On the other hand, for any ` ∈ Z, the Boolean AQ p(`) and O are FO(<)-rewritable: for instance, p(3) ∨ q(2) ∨ p(1) ∨ q(0) is an FO(<)-rewriting of p(3) and O. Consider next the ontology O0 with the axioms: 2 ∗ (? → p0 ), 2 ∗ ( F pk ∧ a → pk ) and 2 ∗ ( F pk ∧ a → p1−k ), k = 0, 1. For w = (w1 , . . . , wn ) ∈ {0, 1}n , let Dw contain a(i) if wi = 1, a(i) if wi = 0, as well as ?(n + 1). Then O0 , Dw |= p0 (0) iff the number of 1s in w is even. It follows that the AQ p0 (0) and the ontology O0 are not FO-rewritable even if we are allowed to use arbitrary arithmetic predicates (not only <, S and PLUS) [12]. This observation motivates the following definitions. An NFA A is an NFA-rewriting of a Boolean FOQ q and an LTL-ontology O if, for any data instance D, we have O, D |= q iff A accepts D written on the tape as the word D0 , . . . , Dk , Dk+1 , where Di = {p | p(i) ∈ D}, k = max D and Dk+1 = ? is a special ‘end of data’ marker. Thus, the alphabet of A is Σq,O = 2sig(q,O) ∪ {?}, where sig(q, O) is the set of variables from P used in q and O. Now suppose we are given a FOQ q(t) with non-empty t = t1 , . . . , tm . We say that an NFA A with the tape alphabet Σq,O × 2{t1 ,...,tm } is an NFA-rewriting of q(t) and O when, for any D and ` = `1 , . . . , `m in ∆D , we have O, D |= q(`) iff A accepts the input word (D0 , V0 ), . . . , (Dk , Vk ), (Dk+1 , ∅) with the Di as above and Vi = {tj | `j = i}, for 0 ≤ i ≤ k. Note that instead of NFA-rewritability we could define an equivalent notion of MSO(<)-rewritability (cf. [17, Theorem 1.1]). It is known [6] that if a Boolean FOQ q and an LTL-ontology O are FO(<, +)- rewritable then the problem ‘O, D |= q?’ is in LogTime-uniform AC0 for data complexity. It is also known [13] that if q and O are NFA-rewritable then this problem is in the class NC1 for data complexity. Theorem 2. Any FOQ q(t) and any LTL-ontology O are NFA-rewritable. Proof. Suppose t = t1 , . . . , tm . For a data instance D, let ID N be the restriction of ID to N. It is easy to construct an MSO-formula µ(t) such that ID Z N |= µ(`) iff O, D |= q(`), for all tuples ` in N. By Büchi’s theorem [8], one can now construct a Büchi automaton B which accepts an ω-word (G0 , V0 ), (G1 , V1 ), . . . over the alphabet Σq,O × 2{t1 ,...,tm } iff (i ) there is exactly one k with Gk = ?; (ii ) Vk+1 = ∅ and (Gk0 , Vk0 ) = (∅, ∅), for all k 0 > k; (iii ) for any D with Di = Gi for i < k, we have IDN |= µ(`) for `j = i if tj ∈ Vi . Finally, one can transform B to an NFA A that accepts a finite word (G0 , V0 ), . . . , (Gk , Vk ) iff B accepts its ω-extension with (∅, ∅), (∅, ∅), . . . . q Let us now assume that the axioms of LTL-ontologies are represented in clausal normal form (2) and consider the fragments LTL2 2 α , LTLα and LTLα , for α ∈ {bool, horn, krom, core}, defined in Section 1. The next theorem establishes NC1 -hardness of query entailment for various types of queries and ontologies. Theorem 3. (i ) AQ-entailment over LTLhorn -ontologies is NC1 -hard. (ii ) FOQ-entailment over the empty ontology is NC1 -hard. (iii ) UCQ+ -entailment over LTL2 1 krom - and LTLkrom -ontologies is NC -hard. Proof. We use the fact [5] that there exist NC1 -complete regular languages. Suppose A is an NFA, q0 its initial state and q1 the only accepting state. Given an input word w = w0 . . . wn , we set Dw = { wi (i) | i ≤ n } ∪ { q1 (n + 1) }. (i ) Let O = {2∗ ( F q 0 ∧a → q) | q →a q 0 }. Then A accepts w iff O, Dw |= q0 (0). (ii ) Let q = q0 (0) ∨ q→a q0 ∃t, t0 S(t, t0 ) ∧ q 0 (t0 ) ∧ a(t) ∧ ¬q(t) . Then A accepts W  w iff ∅, Dw |= q. (iii ) Let q 0 be the result of replacing each occurrence of ¬q(t) in q with q̄(t), for a fresh q̄, and let O0 be an ontology containing 2 ∗ (q̄ ↔ ¬q) for every such q̄. Then A accepts w iff O0 , Dw |= q 0 . q We now establish the FO(<, +)- and FO(<)-rewritability results advertised in the introduction. Theorem 4. Any AQ and LTLkrom -ontology are FO(<, +)-rewritable, but not necessarily FO(<)-rewritable. Proof. Suppose we are given an AQ q(τ ) and an LTLkrom -ontology O. (That they are not necessarily FO(<)-rewritable was shown in Example 1.) Without loss of generality we assume that O does not contain nested F and P and write n ϕ in place of Fn ϕ if n > 0, ϕ if n = 0, and P−n ϕ if n < 0. By a literal, L, we mean a propositional variable from sig(q, O) or its negation. Given literals L and L0 , we write O |= 2 ∗ (L → L ) to say that 2 k 0 ∗ (L → k 0 L ) is true in all O models of O. Let AL,L0 be an NFA whose tape alphabet is {0}, the states are all the literals, with L being the initial and L0 the accepting states, and whose transitions are of the form L1 →0 L2 , for O |= 2 ∗ (L1 → L2 ). L,L0 accepts 0 iff O |= 2 (L → Lemma 5. For any k > 0, the NFA AO L0 ). k ∗ k Every unary automaton AO L,L0 with N states gives rise (via Chrobak normal 2 form [9, 18]) to M = O(N ) arithmetic progressions ai +bi N = {ai +bi ·m | m ≥ 0}, for i ≤ M , such that 1 ≤ ai , bi ≤ N and, for any k > 0, AO k L,L0 accepts 0 iff divbi (k − ai ), for some i ≤ M , where divb (v) = ∃n ((0 ≤ n ≤ v) ∧ (v = bn)). Let M ( O _ O 0 (t = t0 ), if O |= 2∗ (L → L0 ), PL,L 0 (t) = divbi (t − ai ) and EL,L 0 (t, t ) = i=1 ⊥, otherwise. Lemma 6. (i ) If (O, D) is consistent then, for any ` ∈ Z, we have O, D |= q(`) iff either O |= 2 ∗ q or there exists p(m) ∈ D such that O |= 2∗ (p → `−m q). (ii ) If (O, D) is inconsistent then either O |= 2 ⊥ or there are p(m) ∈ D and ∗ r(n) ∈ D such that O |= 2 ∗ (p → n−m ¬r). The conditions of this lemma can be encoded as an FO(<, +)-formula ϕq (t), which is > if O |= 2∗ ⊥ or O |= 2 ∗ q, and otherwise a disjunction of the following formulas, for p, r ∈ sig(q, O), ∃s, s0 p(s) ∧ r(s0 ) ∧ (Pp,¬r O (s0 − s) ∨ Ep,¬r O (s0 , s))) ,  (4) O O O  ∃s p(s) ∧ Pp,q (t − s) ∨ Ep,q (t, s) ∨ P¬q,¬p (s − t) . (5) Thus, O, D |= q(`) iff ID Z |= ϕq (`), for any D and ` ∈ Z. In fact, for a slight 0 q,O modification ϕq (t) of ϕq (t), we can show that O, D |= q(`) iff ID |= ϕ0q (`) where ∆q,O D = [min{0, `}, max{max D, |`| + O(|O|)}]. It follows that ϕ0q (τ ) is a q,O FO(<, +)-rewriting of q(τ ) and O over ID . q By Theorem 3, UCQ+ s and LTLkrom -ontologies are not always FO(<, +)- rewritable. In the next theorem, we restrict attention to LTLcore -ontologies. Theorem 7. Any UCQ+ q(t) and LTLcore -ontology O are FO(<, +)-rewritable. Proof. Let q 0 (t) result from replacing any q(τ ) in q(t) with the above mentioned ϕ0q (τ ). Assuming that O and D are consistent, denote by CO,D the canonical q,O model of O and D. We then have CO,D |= q(`) iff ID Z |= q 0 (`). Let ID be the interpretation defined in the proof of Theorem 4, where ` is the constant in q with maximal |`|, if any. Let max and min be the maximum and minimum of ∆q,O D . By analysing the structure of (4) and (5), we obtain: Lemma 8. Suppose q 0 (t) = ∃s ψ(t, s) with quantifier-free ψ and s = s1 , . . . , sm . If ID Z |= q 0 (`), for some ` in ∆D , then there is a tuple n = n1 , . . . , nm in the interval [min − |q| · O(|O||q| ), max + |q| · O(|O||q| )] such that ID Z |= ψ(`, n). We can now transform q 0 to an FO(<, +)-rewriting q 00 (t) of q and O over q,O ID using FO(<, +)-sentences ϕkq such that, for k < 0 and ` = min + k or for q,O k > 0 and ` = max + k, we have ID Z |= q(`) iff ID |= ϕkq (`). To construct such sentences ϕkq , we require the (max + 1)-ary representation of numbers and a technique from [12, Sec. 1.4]. q Consider next the LTL-ontologies whose axioms (in clausal normal form) can only contain the operators 2P and 2F . All AQs over arbitrary LTL2 bool -ontologies turn out to be FO(<)-rewritable. Theorem 9. Any AQ and LTL2 bool -ontology are FO(<)-rewritable. Proof. Let O be an LTL2 bool -ontology. First we construct an NFA A that describes the structure of models of O and a given data instance D written on the tape as defined above (cf. [19]). Denote by Φ the set of all subformulas of O and their negations. Each state of A is a maximal consistent subset S ⊆ Φ; let S be the set of all such states. For any S, S 0 ∈ S and any tape symbol X = 6 ?, we set S →X S 0 just in case (i ) X ⊆ S 0 , (ii ) 2F ψ ∈ S iff ψ, 2F ψ ∈ S 0 , and (iii ) 2P ψ ∈ S 0 iff ψ, 2P ψ ∈ S. We also set S →? S 0 iff S →∅ S 0 . A state S ∈ S is accepting if A contains an infinite ‘ascending’ chain of transitions of the form S →∅ S1 →∅ S2 →∅ . . . ; S is initial if A contains an infinite ‘descending’ chain · · · →∅ S2 →∅ S1 →∅ S. It is not hard to check that A accepts D iff O and D are consistent. An NFA is called partially ordered [16] if it contains no cycles other than trivial loops. We now convert A to an equivalent partially-ordered NFA A0 . Define an equivalence relation, ∼, on S by taking S ∼ S 0 iff either S = S 0 or A contains a cycle with both S and S 0 . Denote by [S] the ∼-equivalence class of S. It is readily seen that if S →X S 0 then S1 →X S 0 , for any S1 ∈ [S]. The states of A0 are of the form [S], for S ∈ S, and it contains a transition [S] →X [S 0 ] iff S1 →X S10 , for some S1 ∈ [S] and S10 ∈ [S 0 ]. The initial (accepting) states of A0 are all [S] with initial (accepting) S. Clearly, A0 is partially ordered, and it follows from the construction that A0 and A accept the same language. ∗ (p → 2P q), 2 Example 10. Let O = {2 ∗ (2P q → r)}. The NFA A0 for O is shown below: all but q all all [S1 ] [S2 ] [S3 ] all where all states are initial and accepting, [S1 ] = {{2P q, q, p, r}, {2P q, q, r}}, [S2 ] = {{2P q, p, r}, {2P q, r}}, [S3 ] = 2{r,q} (negative literals are omitted). Consider a maximal path pi in A0 of the form [S0 ] →X1 · · · →Xn [Sn ], where all the [Si ] are pairwise distinct, [S0 ] is initial and [Sn ] accepting. We call π a prime path in A0 . Suppose [Si ] →X [Si ] in A0 . The operation of duplicating [Si ] (required for technical reasons that will be clear from Lemma 11) in a prime path π replaces [Si ] in π with [Si ] →X [Si ]. Denote by ΨO the set of all paths obtained by at most two applications of duplication to some prime path. The 2 length of each path in ΨO is polynomial in |O| and |ΨO | = 2O(|O| ) . Given an interpretation I and ` ∈ Z, let tI (`) = {p ∈ Φ ∩ P | I, ` |= p} (the I-type of `). Lemma 11. For any AQ q(t), interpretation I and ` ∈ Z, we have I |= O ∪ D and I 6|= q(`) iff there exist a path π = [S0 ] →X1 · · · →Xn [Sn ] in ΨO , an injective function f : {0, . . . , n} → Z and numbers k, b, e in {0, . . . , n} such that – f (k) = `, f (b) = 0, f (e) = max D and b < e; – for any m ≤ f (0), there is S00 ∈ [S0 ] such that tI (m) = S00 ; – for any m with f (i) ≤ m < f (i + 1), there is Si0 ∈ [Si ] with tI (m) = Si0 ; – for any m ≥ f (n), there is Sn0 ∈ [Sn ] such that tI (m) = Sn0 . Example 12. Consider again the ontology O from Example 10, D = {p(0), p(2)} and the model I of O and D shown below: r, q, 2P q r, q, 2P q p, r, q, 2P q r, q, 2P q p, r, 2P q −2 −1 0 1 2 3 We have I, 3 6|= r and, for the path [S1 ] = [S0 ] →{p} [S1 ] →{p} [S2 ] →∅ [S3 ] in ΨO , we can take f (0) = −1, f (1) = 0, f (2) = 2, f (3) = 3, k = 3, b = 1 and e = 2. The conditions of Lemma 11 for π can be expressed by an FO(<)-formula such as ϕπ,r (t) = ∃tb , te [(tb = 0) ∧ ?(te + 1) ∧ (t > te ) ∧ φπ,[S1 ] (tb ) ∧ φπ,[S2 ] (te ) ∧ ∀t00 ((tb < t00 < te ) → φ[S1 ] (t00 ))], where φπ,[S1 ] (t) = φπ,[S2 ] (t) = p(t) ∧ ¬q(t) ∧ ¬r(t) characterises the transitions [S0 ] →{p} [S1 ] →{p} [S2 ], and φ[S1 ] (t) = >(t) the loops [S1 ] →all [S1 ]. Lemma 13. For any AQ q(t) and LTL2 bool -ontology O, there is an FO(<)- formula χq (t) such that O, D |= q(`) iff ID Z |= χq (`), for all D and ` ∈ Z. The formula χq (t) is defined as a negation of a disjunction of formulas such as ϕπ,r (t) in Example 12, for all possible choices of π, k, b and e. To complete the proof of Theorem 14, we proceed in the same way as in Theorem 4. q By using the canonical models and the technique of the proof of Theorem 7, we also obtain: Theorem 14. Any UCQ+ and LTL2 horn -ontology are FO(<)-rewritable. Our next aim is to ‘lift’ these results to temporal extensions of DL-Lite logics. 3 OBDA with Temporal DL-Lite Let α be one of bool, horn, krom or core, and let β be one of 2, or 2 . We denote by Tβ DL-Liteα the temporal description logic with inclusions of the form λ1 u · · · u λn v λn+1 t · · · t λn+m (6) such that ¬λ1 ∨ · · · ∨ ¬λn ∨ λn+1 ∨ · · · ∨ λn+m is an α-clause (according to the definition in Section 1) and the λi are all either DL-Lite basic concepts or DL-Lite roles, possibly prefixed with temporal operators indicated in β. Recall [1] that DL-Lite basic concepts, B, are of the form B ::= ⊥ | A | ∃R, where A is a concept name and R a role. DL-Lite roles are defined by R ::= ⊥ | P | P − , where P is a role name. A Tβ DL-Liteα TBox T (RBox R) is a finite set of Tβ DL-Liteα concept (respectively, role) inclusions. A TBox is said to be flat if its concept inclusions do not contain ∃R on the right-hand side. We denote by Tβ DL-Liteflat β α the fragment of T DL-Liteα in which only flat TBoxes are allowed. flat (Note that DL-Litecore is basically RDFS.) An ABox A is a set of atoms of the form A(a, n) and P (a, b, n), where a, b are object names and n ∈ Z. A temporal interpretation is a pair I = (∆I , ·I(n) ), in which ∆I 6= ∅ and I(n) I(n) I(n) = (∆I , aI0 , . . . , A0 , . . . , P0 , . . . ) is a standard DL interpretation for each time instant n ∈ Z. Thus, we assume that the domain ∆I and the inter- pretations aIi ∈ ∆I of the object names are the same for all n ∈ Z. The DL and temporal constructs are interpreted in I(n) as expected, for example, \ ( F B)I(n) = B I(n+1) and (2F B)I(n) = B I(k) . k>n d F Concept and role inclusions are interpreted in I globally, that is, I |= λi v λj T I(n) S I(n) just in case λi ⊆ λj , for all n ∈ Z. Given an ABox A, we denote by IAZ the interpretation with domain ind(A), which consists of the object names in A, such that IA Z |= A(a, n) iff A(a, n) ∈ A and IA Z |= P (a, b, n) iff P (a, b, n) ∈ A, for a, b ∈ ind(A) and n ∈ Z. Temporal FOQs are built in the same way as in the LTL case, but from atoms of the form A(ξ, τ ), P (ξ, ζ, τ ) using =, <, S and PLUS. As before, we are interested in various types of FO-rewriting of a FOQ q and a Tβ DL-Liteα q,T ,R ontology T , R over finite first-order structures IA which are restrictions of IA to the minimal closed intervals in Z containing all time instants from A as Z well as some fixed integers that only depend on q and T , R. Theorem 15. Any UCQ+ and T DL-Liteflat core ontology are FO(<, +)-rewritable. Proof. Without loss of generality, we assume that the TBox, T , and RBox, R, do not contain nested temporal operators; together with any role inclusion, R contains the respective inclusion for the inverses; and for every role inclusion in R, say P P − v R, there is an inclusion for their domains, P ∃P − v ∃R, in T . It can be seen that, for any ABox A consistent with T , R and any a, b ∈ ind(A) and ` ∈ Z, we have: R, A |= R(a, b, `) iff T , R, A |= R(a, b, `), and T , A |= B(a, `) iff T , R, A |= B(a, `). Denote by T p (Rp ) the LTLcore -ontology that contains all inclusions from T (R) in which every basic concept (role) is regarded as a propositional variable. For a concept name A (role name P ), let ϕA (t) (respectively, ϕP (t)) be the FO(<, +)-rewriting of A(t) and T p (of P (t) and Rp ) constructed in the proof of Theorem 4. For any ABox A and a, b ∈ ind(A), denote by Aa,b the LTL data instance containing P (n) if P (a, b, n) ∈ A and P − (n) if P (b, a, n) ∈ A. Similarly, for any a ∈ ind(A), let Aa contain A(n) if A(a, n) ∈ A and ∃R(n) if R(n) ∈ Aa,b , for some b. Then Rp , Aa,b |= R(n) iff R, A |= R(a, b, n), and T p , Aa |= B(n) iff T , A |= B(a, n). Now, given an atom P (ξ, ζ, τ ), we construct an FO(<, +)-formula P ∗ (ξ, ζ, τ ) by replacing every R(τ 0 ) in ϕP (τ ) with R(ξ, ζ, τ 0 ) if R is a role name, and with Q(ζ, ξ, τ 0 ) if R = Q− . Similarly, given an atom A(ξ, τ ), we construct an FO(<, +)- formula A∗ (ξ, τ ) by replacing every B(τ 0 ) in ϕA (τ ) with B(ξ, τ 0 ) if B is a concept name, with ∃y P ∗ (ξ, y, τ 0 ) if B = ∃P , and with ∃y P ∗ (y, ξ, τ 0 ) if B = ∃P − . As a consequence of Theorem 4 and the observations above, we obtain: Lemma 16. For any ABox A, any a, b ∈ ind(A) and any ` ∈ Z, we have: T , R, A |= P (a, b, `) iff IA Z |= P ∗ (a, b, `), and T , R, A |= A(a, `) iff IA Z |= A∗ (a, `). The remainder of the proof is a straightforward modification of the corre- sponding part in the proof of Theorem 7. q Example 17. Suppose q = ∃x, y, t (P (x, y, t)∧A(x, t)) and let T contain ∃P − v A and R contain P P − v P . We will also assume that P P v P − is in R and so, both P ∃P − v ∃P and P ∃P v ∃P − are in T . We obtain the following FO(<, +)- rewriting of q and T , R, where all the variables are existentially quantified: [(P (x, y, s) ∧ (t − s = 2n ≥ 0)) ∨ (P (y, x, s) ∧ (t − s = 2n + 1 ≥ 0))] ∧ | {z } P ∗ (x,y,t) [A(x, t) ∨ ∃z ((P (z, x, s) ∧ (t − s = 2n ≥ 0)) ∨ (P (x, z, s) ∧ (t − s = 2n + 1 ≥ 0)))] . | {z } A∗ (x,t) Theorem 18. Any UCQ+ and any T2 DL-Liteflat horn ontology are FO(<)-rewritable. Proof. We proceed similarly to the proof of Theorem 15. One important difference is that, given an RBox R, we extend it with 2F R ≡ FR , for every 2F R in R, and 2P R ≡ PR , for every 2P R in R. (These new roles are auxiliary and do not occur in any ABox.) Treating (the extended) R as an LTL2 horn -ontology, we take the rewriting χR (t) of R(t) and R constructed in the proof of Theorem 14. Let R∗ (ξ, ζ, τ ) be the result of replacing every P (τ 0 ) in χR (t) with P (ξ, ζ, τ 0 ) and every P − (τ 0 ) with P (ζ, ξ, τ 0 ). To construct a rewriting for atoms A(ξ, τ ), we extend T with ∃FR v 2F ∃R, for every FR in R, and ∃PR v 2P ∃R, for every PR in R. (The need for such axioms, connecting T and R, is explained by Example 19.) Treating (the extended) T as an LTL2 horn -ontology, we take the rewriting χA (t) of A(t) and T from Theorem 14. Denote by A∗ (ξ, τ ) the result of replacing every A0 (τ 0 ) in χA (t) with A0 (ξ, τ 0 ), every ∃P (τ 0 ) with ∃y P ∗ (ξ, y, τ 0 ), and every ∃P − (τ 0 ) with ∃y P ∗ (y, ξ, τ 0 ). The remainder of the proof is now routine. Example 19. Consider R = {R v 2P T }, T = {2P ∃T v A} and the AQ A(x, t). Then χT (t) = T (t)∨∃s [(s > t)∧R(s)]. If we did not extend T with ∃PT v 2P ∃T , we would have χA (t) = A(t). But due to this inclusion, we obtain χA (t) = A(t) ∨ ∃t0 [(t0 ≥ t) ∧ ∃PT (t0 )] ∨ ∃t0 [(t0 < t) ∧ ∃PT (t0 ) ∧ ∀s ((t0 ≤ s < t) → ∃T (s))], χPT (t) = ∃t [(t ≥ t) ∧ R(t0 )] ∨ ∃t0 [(t0 < t) ∧ R(t0 ) ∧ ∀s ((t0 ≤ s < t) → T (s))]. 0 0 Theorem 20. The UCQ+ -entailment problem over T2 DL-Liteflat horn -ontologies without role inclusions is NC1 -complete for data complexity. Proof. To sketch the idea, let us assume that the given TBox T does not contain roles (roles are mostly harmless without role inclusions). Let q = ∃x∃t ϕ(x, t) be the given UCQ+ . We treat the atoms A(xi , t) in ϕ as unary predicates Axi (t) and, using the construction from [19], define an NFA A such that, for any ABox A and any tuple a from A, we have T , A 6|= ∃t ϕ(a, t) iff A accepts a word Da , constructed by a constant-size circuit and encoding the data in A relevant to a. We convert A to an NC1 circuit and then use multiple copies of the constructed circuits to assemble an NC1 circuit answering q over any given ABox. q 4 Conclusions This paper launches a systematic investigation of the rewritability problem for temporal queries and ontologies. We first consider this problem for AQs and UCQ+ s over LTL-ontologies in clausal normal form and classify them in terms of FO(<)-, FO(<, +)- or NFA-rewritability. However, it remains unclear whether NFA-rewritability of AQs over LTL2 + krom -ontologies, and of AQs and UCQ s over 2 LTLcore -ontologies can be improved to FO(<, +)-rewritability. Another interesting problem is to analyse rewritability of general FO-queries in more detail. We also show that some of our rewritability results over LTL-ontologies can be lifted to the corresponding flat DL-Lite-ontologies. Extending these results to the non-flat case looks more of less straightforward but is technically challenging. We are working on the extension of Theorem 20 to the case with role inclusions and on a complete classification of temporalised DL-Lite logics according to query rewritability. References 1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. Journal of Artificial Intelligence Research (JAIR) 36, 1–69 (2009) 2. Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: The complexity of clausal fragments of LTL. In: Proc. of the 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNCS, vol. 8312, pp. 35–52. Springer (2013) 3. Artale, A., Kontchakov, R., Wolter, F., Zakharyaschev, M.: Temporal description logic for ontology-based data access. In: Proc. of the 23rd Int. Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI (2013) 4. Baader, F., Borgwardt, S., Lippmann, M.: Temporalizing ontology-based data access. In: Proc. of the 24th Int. Conf. on Automated Deduction, CADE-24. LNCS, vol. 7898, pp. 330–344. Springer (2013) 5. Barrington, D.A.M., Compton, K.J., Straubing, H., Thérien, D.: Regular languages in NC1 . J. Comput. Syst. Sci. 44(3), 478–499 (1992) 6. Barrington, D.A.M., Straubing, H.: Superlinear lower bounds for bounded-width branching programs. J. Comput. Syst. Sci. 50(3), 374–381 (1995) 7. Borgwardt, S., Lippmann, M., Thost, V.: Temporal query answering in the descrip- tion logic DL-Lite. In: Proc. of the 9th Int. Symposium on Frontiers of Combining Systems (FroCoS’13). LNCS, vol. 8152, pp. 165–180. Springer (2013) 8. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the 1960 Int. Congress on Logic, Methodology and Philosophy of Science (LMPS’60). pp. 1–11. Stanford University Press (1962) 9. Chrobak, M.: Finite automata and unary languages. Theor. Comput. Sci. 47(2), 149–158 (1986) 10. Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. on Computational Logic 2(1), 12–56 (2001) 11. Gutiérrez-Basulto, V., Klarman, S.: Towards a unifying approach to representing and querying temporal data in description logics. In: Proc. of the 6th Int. Conf. on Web Reasoning and Rule Systems (RR 2012). LNCS, vol. 7497, pp. 90–105. Springer (2012) 12. Immerman, N.: Descriptive Complexity. Springer (1999) 13. Ladner, R.E., Fischer, M.J.: Parallel prefix computation. J. ACM 27(4), 831–838 (1980) 14. Libkin, L.: Elements Of Finite Model Theory. Springer (2004) 15. Özcep, O., Möller, R., Neuenstadt, C., Zheleznyakov, D., Kharlamov, E.: A semantics for temporal and stream-based query answering in an OBDA context. Tech. rep., Deliverable D5.1, FP7-318338, EU (2013) 16. Schwentick, T., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Revised Papers of the 5th Int. Conf. in Developments in Language Theory (DLT 2001). LNCS, vol. 2295, pp. 239–250. Springer (2002) 17. Straubing, H., Weil, P.: An introduction to finite automata and their connection to logic. CoRR abs/1011.6491 (2010) 18. To, A.W.: Unary finite automata vs. arithmetic progressions. Inf. Process. Lett. 109(17), 1010–1014 (2009) 19. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proc. of the Symposium on Logic in Computer Science (LICS’86). pp. 332–344 (1986)