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 nite automata with data given on the automaton tape.
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 [
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, [
In contrast, the aim of [
n2) ^ Striker(x; t) ^ onMUcontract(x; y; t) to nd 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
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 nite 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 identi ed in [
F j
P
j 2F
j 2P :
(Here 2F and 2P are the operators `always in the future' and `always in the past'.)
Similarly to [
B u E v onMUContract
with fresh concepts B and E. Borrowing the terminology from [
LTL2
AQ FO(<) FO(<) FO(<) FO(<)
UCQ+ NFA FO(<) NFA FO(<)
LTL AQ NFA
NFA FO(<; +) FO(<; +)
UCQ+ NFA NFA
NFA FO(<; +)
LTL2 AQ NFA NFA NFA NFA
UCQ+ NFA NFA 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 T2DL-Litehoartn and T DL-Litecoarte whose concept and role inclusions are LTLh2orn and LTLcore clauses with concepts or roles in place of propositional variables and without 9R 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 T2DL-Litehoartn-ontologies are FO(<)-rewritable, while over T DL-Litecoarteontologies they are FO(<; +)-rewritable. We also show that the UCQ+-entailment problem over T2 DL-Litehoartn-ontologies, which do not contain role inclusions, is NC1-complete for data complexity. 2
We begin by considering the propositional temporal logic LTL over the ow of time (Z; <). LTL-formulas are built from propositional variables P = fp0; p1; : : : g, 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, de nes a truth-relation, j=, between moments of time n 2 Z and propositional variables pi. We write I; n j= 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 j= 2 ' i I; k j= '; for all k 2 Z, { I; n j= 3 ' i I; k j= '; for some k 2 Z, { I; n j= ' U i there is k > n with I; k j= { I; n j= 2F ' i I; k j= '; for all k > n, { I; n j= 3F ' i I; k j= '; for some k > n, { I; n j= F ' i I; n + 1 j= ', and I; m j= '; for n < m < k, 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 nite set of LTL-formulas of the form 2 '. With each p 2 P we associate a unary predicate over Z, also denoted p. A data instance is a nite set, D, of atoms of the form p(`) with p 2 P and ` 2 Z. We denote by min D (max D) the minimal (maximal) number occurring in D and set D = f` j min D ` max Dg. 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 j= K if I; n j= ', for all 2 ' in O and n 2 Z, and I; ` j= p, for all p(`) 2 D.
A temporal rst-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 9s '(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 j= q(`) regarding I as a rst-order structure; in this case we write O; D j= q(`). We refer to the problem `O; D j= q?', where q is a Boolean FOQ, as FOQ-entailment over temporal ontologies. q;O the nite rst
Let q(t) be a FOQ and O an LTL-ontology. Denote by ID ionrtdeerrvsatlruinctZurtehdaet cnoendtaaisnfsolloDwsa. sTwheeldloamsasoinme qD;Oxedof iInDqte;Ogeirsstthheamtionnimlyadlecploesnedd on q and O (for example, all ` 2= D occurring in q should be included into qD;O). For any ` 2 qD;O, we set IDq;O j= p(`) i p(`) 2 D. We also assume that the binary relations <, = and S and ternary relation PLUS are interpreted over q;O in a natural way (e.g., PLUS(n; m; k) is true i n = m + k). If we extend D
q;O to Z, then the resulting structure is denoted by IDZ. the domain of ID
A FOQ q0(t) is an FO(<)-rewriting of q(t) and O if, for any data instance D
and any tuple ` from D, we have O; D j= q(`) i IDq;O j= q0(`). If we allow the
use of PLUS in q0(t), then it is called an FO(<; +)-rewriting of q(t) and O.
Example 1. Consider the ontology O = f2( P p ! q); 2( P q ! p)g. Then
9s; 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
9n2 (PLUS(n2; n; n) ^ PLUS(t; s; n2) ^ (n2 0)) and t s = 2n + 1 0 is de ned
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 [
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 j= q i A accepts D written on the tape as the word D0; : : : ; Dk; Dk+1, where Di = fp j p(i) 2 Dg, k = max D and Dk+1 = ? is a special `end of data' marker. Thus, the alphabet of A is q;O = 2sig(q;O) [ f?g, 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 2ft1;:::;tmg is an NFA-rewriting of q(t) and O when, for any D and ` = `1; : : : ; `m in D, we have O; D j= q(`) i A accepts the input word (D0; V0); : : : ; (Dk; Vk); (Dk+1; ;) with the Di as above and Vi = ftj j `j = ig, for 0 i k. Note that instead of NFA-rewritability we could de ne an equivalent notion of MSO(<)-rewritability (cf. [17, Theorem 1.1]).
It is known [
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 IDN be the restriction
of IDZ to N. It is easy to construct an MSO-formula (t) such that IDN j= (`)
i O; D j= q(`), for all tuples ` in N. By Buchi's theorem [
Let us now assume that the axioms of LTL-ontologies are represented in clausal normal form (2) and consider the fragments LTL2, LTL and LTL2 , for 2 fbool; horn; krom; coreg, de ned 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 LTLk2rom- and LTLkrom-ontologies is NC1-hard.
Proof. We use the fact [
(i ) Let O = f2( F q0 ^a ! q) j q !a q0g. Then A accepts w i O; Dw j= q0(0). (ii ) Let q = q0(0) _ Wq!aq0 9t; t0 S(t; t0) ^ q0(t0) ^ a(t) ^ :q(t) . Then A accepts w i ;; Dw j= q. (iii ) Let q0 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 i O0; Dw j= q0. 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 j= 2(L ! kL0) to say that 2(L ! kL0) is true in all models of O. Let ALO;L0 be an NFA whose tape alphabet is f0g, 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 j= 2(L1 ! L2).
Lemma 5. For any k > 0, the NFA ALO;L0 accepts 0k i O j= 2(L ! kL0).
Every unary automaton ALO;L0 with N states gives rise (via Chrobak normal
form [
ELO;L0 (t; t0) = ((t = t0); if O j= 2(L ! L0); ?; otherwise: Lemma 6. (i ) If (O; D) is consistent then, for any ` 2 Z, we have O; D j= q(`) i either O j= 2 q or there exists p(m) 2 D such that O j= 2(p ! ` mq).
(ii ) If (O; D) is inconsistent then either O j= 2 ? or there are p(m) 2 D and r(n) 2 D such that O j= 2(p ! n m:r).
The conditions of this lemma can be encoded as an FO(<; +)-formula 'q(t), which is > if O j= 2 ? or O j= 2 q, and otherwise a disjunction of the following formulas, for p; r 2 sig(q; O), 9s; s0 p(s) ^ r(s0) ^ (PpO;:r(s0
s) _ EpO;:r(s0; s))) ; 9s p(s) ^ PpO;q(t s) _ EpO;q(t; s) _ P:Oq;:p(s t) : (4) Thus, O; D j= q(`) i IDZ j= 'q(`), for any D and ` 2 Z. In fact, for a slight modi cation '0q(t) of 'q(t), we can show that O; D j= q(`) i IDq;O j= '0q(`) wFOhe(r<e; +qD)-;Orew=ri[tminignfo0f; q`(g; )maanxdfmOaxovDe;rj`IjDq+;OO.(jOj)g]. It follows that '0q( ) is qa
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 q0(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 model of O and D. We then have CO;D j= q(`) i ID j q;O be the Z = q0(`). Let ID interpretation de ned in the proof of Theorem 4, where ` is the constant in q with maximal j`j, if any. Let max and min be the maximum and minimum of q;O. By analysing the structure of (4) and (5), we obtain:
D Lemma 8. Suppose q0(t) = 9s (t; s) with quanti er-free and s = s1; : : : ; sm. If IDZ j= q0(`), for some ` in D, then there is a tuple n = n1; : : : ; nm in the interval [min jqj O(jOjjqj); max + jqj O(jOjjqj)] such that IDZ j= (`; n).
We can now transform q0 to an FO(<; +)-rewriting q00(t) of q and O over q;O using FO(<; +)-sentences 'qk such that, for k < 0 and ` = min + k or for ID k > 0 and ` = max + k, we have IDZ j= q(`) i IDq;O j= 'qk(`). To construct such sentences 'k, we require the (max + 1)-ary representation of numbers and a q 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 LTLb2ool-ontologies turn out to be FO(<)-rewritable.
Theorem 9. Any AQ and LTLb2ool-ontology are FO(<)-rewritable.
2
Proof. Let O be an LTLbool-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 de ned above (cf. [
An NFA is called partially ordered [
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 length of each path in O is polynomial in jOj and j Oj = 2O(jOj2). Given an interpretation I and ` 2 Z, let tI (`) = fp 2 \ P j I; ` j= pg (the I-type of `). Lemma 11. For any AQ q(t), interpretation I and ` 2 Z, we have I j= O [ D and I 6j= q(`) i there exist a path = [S0] !X1 !Xn [Sn] in O, an injective function f : f0; : : : ; ng ! Z and numbers k, b, e in f0; : : : ; ng such that { f (k) = `, f (b) = 0, f (e) = max D and b < e; { for any m f (0), there is S00 2 [S0] such that tI (m) = S00; { for any m with f (i) m < f (i + 1), there is Si0 2 [Si] with tI (m) = Si0; { for any m f (n), there is Sn0 2 [Sn] such that tI (m) = Sn0.
Example 12. Consider again the ontology O from Example 10, D = fp(0); p(2)g 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 6j= r and, for the path [S1] = [S0] !fpg [S1] !fpg [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) = 9tb; te[(tb = 0) ^ ?(te + 1) ^ (t > te) ^ ;[S1](tb) ^
;[S2](te) ^ 8t00((tb < t00 < te) ! [S1](t00))]; where ;[S1](t) = ;[S2](t) = p(t) ^ :q(t) ^ :r(t) characterises the transitions [S0] !fpg [S1] !fpg [S2], and [S1](t) = >(t) the loops [S1] !all [S1]. Lemma 13. For any AQ q(t) and LTLb2ool-ontology O, there is an FO(<)formula q(t) such that O; D j= q(`) i IDZ j= q(`), for all D and ` 2 Z.
The formula q(t) is de ned 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 LTLh2orn-ontology are FO(<)-rewritable.
Our next aim is to `lift' these results to temporal extensions of DL-Lite logics. 3
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
de nition in Section 1) and the i are all either DL-Lite basic concepts or DL-Lite
roles, possibly pre xed with temporal operators indicated in . Recall [
A temporal interpretation is a pair I = ( I ; I(n)), in which I 6= ; and I(n) = ( I ; a0I ; : : : ; A0I(n); : : : ; P0I(n); : : : ) is a standard DL interpretation for each time instant n 2 Z. Thus, we assume that the domain I and the interpretations aiI 2 I of the object names are the same for all n 2 Z. The DL and temporal constructs are interpreted in I(n) as expected, for example, ( F B)I(n) = BI(n+1) and (2F B)I(n) = \ k>n
BI(k): Concept and role inclusions are interpreted in I globally, that is, I j= d i v F j just in case T iI(n) S jI(n), for all n 2 Z. Given an ABox A, we denote by
Z the interpretation with domain ind(A), which consists of the object names in IA A, such that IAZ j= A(a; n) i A(a; n) 2 A and IAZ j= P (a; b; n) i P (a; b; n) 2 A, for a; b 2 ind(A) and n 2 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 ontology T , R over nite rst-order structures IAq;T ;R which are restrictions of
Z to the minimal closed intervals in Z containing all time instants from A as IA well as some xed integers that only depend on q and T , R.
Theorem 15. Any UCQ+ and T DL-Litecoarte 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 9P v 9R, in T . It can be seen that, for any ABox A consistent with T , R and any a; b 2 ind(A) and ` 2 Z, we have: R; A j= R(a; b; `) i T ; R; A j= R(a; b; `), and T ; A j= B(a; `) i T ; R; A j= 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 2 ind(A), denote by Aa;b the LTL data instance containing P (n) if P (a; b; n) 2 A and P (n) if P (b; a; n) 2 A. Similarly, for any a 2 ind(A), let Aa contain A(n) if A(a; n) 2 A and 9R(n) if R(n) 2 Aa;b, for some b. Then Rp; Aa;b j= R(n) i R; A j= R(a; b; n), and T p; Aa j= B(n) i T ; A j= 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 9y P ( ; y; 0) if B = 9P , and with 9y P (y; ; 0) if B = 9P . As a consequence of Theorem 4 and the observations above, we obtain: Lemma 16. For any ABox A, any a; b 2 ind(A) and any ` 2 Z, we have: T ; R; A j= P (a; b; `) i IAZ j= P (a; b; `), and T ; R; A j= A(a; `) i IAZ j= A (a; `).
The remainder of the proof is a straightforward modi cation of the corresponding part in the proof of Theorem 7. q Example 17. Suppose q = 9x; y; t (P (x; y; t)^A(x; t)) and let T contain 9P 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 9P v 9P and P 9P v 9P are in T . We obtain the following FO(<; +)rewriting of q and T ; R, where all the variables are existentially quanti ed: [(P (x; y; s) ^ (t s = 2n |
P ({xz;y;t) 0)) _ (P (y; x; s) ^ (t s = 2n + 1 Proof. We proceed similarly to the proof of Theorem 15. One important di erence 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 2 not occur in any ABox.) Treating (the extended) R as an LTLhorn-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 9FR v 2F 9R, for every FR in R, and 9PR v 2P 9R, for every PR in R. (The need for such axioms, connecting T and R, is explained by 2 Example 19.) Treating (the extended) T as an LTLhorn-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 9P ( 0) with 9y P ( ; y; 0), and every 9P ( 0) with 9y P (y; ; 0). The remainder of the proof is now routine. Example 19. Consider R = fR v 2P T g, T = f2P 9T v Ag and the AQ A(x; t). Then T (t) = T (t) _ 9s [(s > t) ^ R(s)]. If we did not extend T with 9PT v 2P 9T , we would have A(t) = A(t). But due to this inclusion, we obtain A(t) = A(t) _ 9t0 [(t0 t) ^ 9PT (t0)] _ 9t0[(t0 < t) ^ 9PT (t0) ^ 8s ((t0 s < t) ! 9T (s))]; PT (t) = 9t0 [(t0 t) ^ R(t0)] _ 9t0 [(t0 < t) ^ R(t0) ^ 8s ((t0 s < t) ! T (s))]: Theorem 20. The UCQ+-entailment problem over T2 DL-Litehoartn-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 = 9x9t '(x; t)
be the given UCQ+. We treat the atoms A(xi; t) in ' as unary predicates Axi(t)
and, using the construction from [
This paper launches a systematic investigation of the rewritability problem for temporal queries and ontologies. We rst 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 2 NFA-rewritability of AQs over LTLkrom-ontologies, and of AQs and UCQ+s over LTLc2ore-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 at DL-Lite-ontologies. Extending these results to the non- at 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 classi cation of temporalised DL-Lite logics according to query rewritability.