Temporal Query Answering in DL-Lite∗

Abstract

Context-aware applications try to detect specific situations within a changing environment (e.g. a computer system or air traffic observed by radar) in order to react accordingly. To gain information, the environment is observed by sensors (for a computer system, data about its resources is gathered by the operating system), and the results of sensing are stored in a database. A context-aware application then detects specific predefined situations based on this data (e.g. a high system load) and executes some action (e.g. increases the CPU frequency). In a simple setting, such an application can be realized by using standard database techniques: the sensor information is stored in a database, and the situations to be recognized are specified as database queries [1]. However, we cannot assume that the sensors provide a complete description of the current state of the environment. Thus, the closed world assumption employed by database systems (i.e. facts not present in the database are assumed to be false) is not appropriate since there may be facts of which the truth is not known. For example, a sensor for certain information might not be available for a moment or not even exist. In addition, though a complete specification of the environment usually does not exist, often some knowledge about its behavior is available. This knowledge can be used to formulate constraints on the interpretation of the predicates used in the queries, to detect more complex situations. In ontology-based data access (OBDA) [8], domain knowledge is encoded in ontologies using a description logic (DL). In this paper, we consider logics of the DL-Lite family, which are lightweight DLs with a low complexity for many reasoning problems [8]. In order to recognize situations that evolve over time, we propose to add a temporal logical component to the queries. We use the operators of the temporal logic LTL, which allows to reason about a linear and discrete flow of time [17]. Usual temporal operators include next (#φ), eventually (3φ), and always (2φ), asserting that a property φ is true at the next point in time, at some point in the future, and at all time points in the future, respectively. We also use the corresponding past operators #−, 3−, and 2−. Consider, for example, a collection of servers providing several services. An important task is to migrate services between servers to balance the load. To decide when to migrate, we want to detect certain critical situations. We consider a process to be critical if it has an increasing workload, and at the same time the

-

Introduction ∗ Partially supported by DFG SFB 912 (HAEC) and GRK 1763 (QuantLA). server that hosts it is almost overloaded. We want to detect those processes and servers that were in a critical situation at least twice within the past ten time units, expressed by the query #−10(3(Critical(x, y) ∧ #3Critical(x, y))), where Critical(x, y) := Server(x) ∧ Process(y) ∧ executes(x, y) ∧ Running(y) ∧

IncreasingWorkload(y) ∧ AlmostOverloaded(x).

In this example, it is essential that future and past operators can be nested arbitrarily. One might argue that, as we are looking at the time line from the point of view of the current time point, and nothing is known about the future, having only past operators is sufficient. We will even show that in our setting it is always possible to construct an equivalent query using only past operators. However, the resulting query is not very concise and it is not easy to see the situation that is to be recognized. This is similar to propositional LTL, where eliminating the past operators from a formula incurs a blowup that is at least exponential and no constructions smaller than triply exponential are known [16].

Temporal extensions of DL-Lite [ 9 ] have been considered in the context of conceptual modeling [ 2,3,4 ], where the focus lies on checking concept satisfiability. OBDA, the second major use case of DL-Lite, with query answering as the most important reasoning problem [ 8 ], has not yet been studied in a temporal setting. Investigations of temporal query languages based on a combination of DL queries such as conjunctive queries (CQs) and temporal logics such as LTL have started only quite recently. In [ 14 ], a framework is developed that combines the two without much interference. The algorithm for query answering in this setting is an LTL-satisfiability test using a sub-procedure to answer (atemporal) CQs. In [ 5 ], a similar query language, a combination of LTL and CQs over the DL ALC, is proposed. Its temporal component, however, is allowed to influence the DL queries via the notion of rigid names. The complexity increases depending on whether only rigid concept names or also rigid role names are allowed. Additionally, the latter paper also studies the so-called data complexity, where the complexity is measured only w.r.t. the size of the sensor data.

In this paper, we follow an approach suggested in [ 14 ] to combine the firstorder rewriting techniques for atemporal query answering in logics of the DL-Lite family with a temporal component. The main idea is to use optimized database techniques to answer the actual queries. However, the existing techniques for answering temporal queries over temporal databases do not perfectly suit our purposes. In [ 12 ], the authors describe a temporal extension of the SQL query language that can answer temporal queries over a complete temporal database. However, in our setting the database containing all previous observations may grow huge very fast, but not all past observations are relevant for a particular query. In [ 11 ], an approach is described that reduces the amount of space needed; but the query language considered there allows only for past operators. In addition to describing how these approaches can be applied to our problem, we propose a new algorithm that extends the one from [ 11 ] and can also deal with future operators. An extended version of this paper has been accepted for publication in [ 6 ]. The formal proofs of our results can be found in [ 7 ].

Preliminaries We first describe the DL component, and then the temporal component of our query language. The DL-Lite family consists of various DLs that are tailored towards conceptual modeling and allow to realize query answering using classical database techniques. We only consider DL-Litecore as a prototypical example. Definition 1. Let NC, NR, and NI be non-empty, pairwise disjoint sets of concept, role, and individual names, respectively. A role expression is either a role name P1 ∈ NR or an inverse role P2− with P2 ∈ NR. A basic concept is of the form A or ∃R, where A ∈ NC and R is a role expression. A general concept is of the form B or ¬B, where B is a basic concept.

A concept inclusion is of the form B v C, where B is a basic concept and C is a general concept. An assertion is of the form A(a) or P (a, b), where A ∈ NC, P ∈ NR, and a, b ∈ NI. A TBox (or ontology) is a finite set of concept inclusions, and an ABox is finite set of assertions.

The semantics of DL-Litecore is defined through the notion of an interpretation. Definition 2. An interpretation is a pair I = (ΔI , ·I ), where ΔI is a nonempty set (called domain) and ·I is a function that assigns to every A ∈ NC a set AI ⊆ ΔI , to every P ∈ NR a binary relation P I ⊆ ΔI × ΔI , and to every a ∈ NI an element aI ∈ ΔI . This function is extended to role expressions, basic concepts, and general concepts as follows: (P −)I := {(e, d) | (d, e) ∈ P I }, (∃R)I := {d | there is an e ∈ ΔI such that (d, e) ∈ RI }, and (¬C)I := ΔI \ CI .

I is a model of B v C if BI ⊆ CI , of A(a) if aI ∈ AI , and of P (a, b) if (aI , bI ) ∈ P I . We write I |= T if I is a model of all concept inclusions in the TBox T , and I |= A if I is a model of all assertions in the ABox A. We assume that all interpretations I satisfy the unique name assumption (UNA), i.e. for all a, b ∈ NI with a 6= b, we have aI 6= bI .

We now introduce the notion of temporal knowledge bases. Intuitively, they contain sensor data (ABoxes) for all previous time points, and a global TBox. Definition 3. A temporal knowledge base (TKB) K = h(Ai)0≤i≤n, T i consists of a finite sequence of ABoxes Ai and a TBox T , where the ABoxes Ai can only contain concept names that also occur in T . Let I = (Ii)0≤i≤n be a sequence of interpretations Ii = (Δ, ·Ii ) over a fixed non-empty domain Δ. Then I is a model of K (written I |= K) if Ii |= Ai and Ii |= T for all i, 0 ≤ i ≤ n. Similar to what was done in [ 5,14 ], our temporal query language is based on conjunctive queries [ 1,10 ]. The main difference is that we do not allow negation, as also in DL-Lite arbitrary negation is not allowed. The reason is that the reductions in Section 3 do not work in the presence of negation. Definition 4. Let NV be a set of variables. A conjunctive query (CQ) is of the form φ = ∃y1, . . . , ym.ψ, where y1, . . . , ym ∈ NV and ψ is a (possibly empty) finite conjunction of atoms of the form A(z) for A ∈ NC and z ∈ NV ∪ NI ( concept atom); or r(z1, z2) for r ∈ NR and z1, z2 ∈ NV ∪ NI ( role atom). The empty conjunction is denoted by true.

Temporal conjunctive queries (TCQs) are built from CQs as follows: each CQ is a TCQ, and if φ1 and φ2 are TCQs, then so are φ1 ∧ φ2 (conjunction), φ1 ∨ φ2 (disjunction), #φ1 (strong next), •φ1 (weak next), #−φ1 (strong previous), •−φ1 (weak previous), φ1 U φ2 (until), and φ1 S φ2 (since). The symbols #−, •−, and S are called past operators, the symbols #, • , and U are future operators. All results also hold in the presence of the additional temporal operators 2 (always), 2− (always in the past), 3 (eventually), and 3− (some time in the past) [ 7 ], but we omit them here for space reasons.

We denote the set of variables occurring in a TCQ φ by Var(φ), and the set of free variables in φ by FVar(φ). A TCQ φ is called Boolean if FVar(φ) = ∅. We further denote by Sub(φ) the set of all TCQs occurring as subqueries in φ (including φ itself). A union of conjunctive queries (UCQ) is a disjunction of CQs. For our purposes, it is sufficient to define the semantics for Boolean CQs and TCQs. As usual, it is given using the notion of a homomorphism [ 10 ]. Definition 5. Let I = (Δ, ·I ) be an interpretation and ψ be a Boolean CQ. A mapping π : Var(ψ) ∪ NI → Δ is a homomorphism of ψ into I if π(a) = aI for all a ∈ NI, π(z) ∈ AI for all concept atoms A(z) in ψ, and (π(z1), π(z2)) ∈ rI for all role atoms r(z1, z2) in ψ. We say that I is a model of ψ (written I |= ψ) if there is such a homomorphism.

Let now φ be a Boolean TCQ. For a sequence of interpretations I = (Ii)0≤i≤n and i with 0 ≤ i ≤ n, we define I, i |= φ by induction on the structure of φ: I, i |= ∃y1, . . . , ym.ψ iff Ii |= ∃y1, . . . , ym.ψ I, i |= φ1 ∧ φ2 iff I, i |= φ1 and I, i |= φ2 I, i |= φ1 ∨ φ2 iff I, i |= φ1 or I, i |= φ2 I, i |= #φ1 iff i < n and I, i + 1 |= φ1 I, i |= •φ1 iff i < n implies I, i + 1 |= φ1 I, i |= #−φ1 iff i > 0 and I, i − 1 |= φ1 I, i |= •−φ1 iff i > 0 implies I, i − 1 |= φ1 I, i |= φ1 U φ2 iff there is some k, i ≤ k ≤ n such that I, k |= φ2 and I, j |= φ1 for all j, i ≤ j < k I, i |= φ1 S φ2 iff there is some k, 0 ≤ k ≤ i such that I, k |= φ2 and I, j |= φ1 for all j, k < j ≤ i.

Here we assume that there is no time point before 0 or after n, similar to the temporal semantics used for LTL in [20] or for temporal query languages for databases [ 11,15,18 ]. As in classical LTL, one can show that φ1 S φ2 is equivalent to φ2 ∨ (φ1 ∧ #−(φ1 S φ2)), and a similar equivalence holds for U.

We are now ready to introduce the central reasoning problem of this paper, namely finding certain answers to TCQs.

Definition 6. Let φ be a TCQ, I = (Ii)0≤i≤n a sequence of interpretations, and i ≥ 0. The mapping a : FVar(φ) → NI is an answer to φ w.r.t. I at time point i if I, i |= a(φ), where a(φ) denotes the Boolean TCQ that is obtained from φ by replacing the free variables according to a. Let further K = h(Ai)0≤i≤n, T i be a TKB. A mapping a : FVar(φ) → NI is a certain answer to φ w.r.t. K at time point i if for every J |= K, we have J, i |= a(φ).

The set of all answers to φ w.r.t. I at time point i is denoted by Ans(φ, I, i), and the set of all certain answers to φ w.r.t. K is denoted by Cert(φ, K, i). Recall that our main interest lies in finding answers to queries at the last time point, i.e. computing the sets Ans(φ, I) := Ans(φ, I, n) or Cert(φ, K) := Cert(φ, K, n).

We will sometimes use the abbreviation false := A(x) ∧ A0(x), where A, A0 are new concept names for which we assume that the concept inclusion A v ¬A0 is contained in the global TBox T . 3

Answering Temporal Conjunctive Queries For computing the set of certain answers for a conjunctive query, the rewriting approach [ 8 ] can be employed. It compiles the information contained in the TBox into the query and evaluates the query w.r.t. the ABox (viewed as database) using classical database techniques. A similar approach is possible for TCQs. Definition 7. For an ABox A, the interpretation DB(A) := (NI, ·DB(A)) is defined as follows: – aDB(A) := a for all a ∈ NI; – ADB(A) := {a | A(a) ∈ A} for all A ∈ NC; and – P DB(A) := {(a, b) | P (a, b) ∈ A} for all P ∈ NR.

As shown in [ 8 ], this interpretation is the smallest model of A. In order to employ database techniques, we must assume NI and DB(A) to be finite. Proposition 8 ([ 8 ]). Let ψ be a CQ, A be an ABox, and T be a TBox. There is a canonical model IA,T of A and T and a UCQ ψT such that

Cert(ψ, hA, T i) = Ans(ψ, IA,T ) = Ans(ψT , DB(A)).

We now use this proposition to show a similar result for TCQs. Let φ be a TCQ and K = h(Ai)0≤i≤n, T i be a TKB. The TCQ φT is obtained by replacing each CQ ψ occurring in φ by ψT . Note that φT is again a TCQ since ψT is always a UCQ. Let furthermore IK := (IAi,T )0≤i≤n and DB(K) := (DB(Ai))0≤i≤n. The following theorem can be shown by a straightforward induction on the structure of φ.

Theorem 9. For every TCQ φ, TKB K = h(Ai)0≤i≤n, T i, and i ≥ 0, we have Cert(φ, K, i) = Ans(φ, IK, i) = Ans(φT , DB(K), i).

More importantly, for every TCQ φ and TKB K = h(Ai)0≤i≤n, T i, it holds that Cert(φ, K) = Ans(φT , DB(K)). It thus remains to show how to compute the set Ans(φ, I) for a TCQ φ and a sequence I = (Ii)0≤i≤n of interpretations over a finite domain. A first possibility is to view I as a temporal database and rewrite φ into an ATSQL query [ 12 ]. However, since our goal is to monitor processes that produce new data in very short time intervals, storing all the data for all previous time points is not feasible. Therefore, we describe two different approaches that reduce the amount of space necessary to compute Ans(φ, I). Since we are interested in the answers at the last time point, the idea is to keep only the past information necessary to answer the query φ.

In the first approach (Section 4), we rewrite φ into a TCQ φ0 without future operators, employing a construction described in [ 13 ]. We then compute Ans(φ0, I) using an algorithm described in [ 11,19 ] that uses a so-called bounded history encoding, which means that the space required by the algorithm is constant w.r.t. the number n of previous time points. Only the current state of the database and some auxiliary relations have to be stored.

In Section 5, we generalize the algorithm from [ 11 ] to directly deal with the future operators. The main difference is that we do not consider negation or arbitrary first-order queries. Unfortunately, the space required by this algorithm is in general unbounded w.r.t. n and thus does not constitute a bounded history encoding in the sense of [ 11,19 ]. However, it allows us to circumvent the nonelementary blow-up of the formula resulting from the reduction in [ 13 ]. 4

Eliminating Future Operators In this section, we rewrite a TCQ φ into an equivalent TCQ φ0 that does not contain future operators, but may contain negation as in [ 11 ]. We then apply the algorithm described in [ 11 ] to iteratively compute the sets Ans(φ0, I, i). The reduction uses the separation theorem for propositional LTL [ 13 ]. However, this theorem cannot be applied directly since our temporal semantics differs from that in [ 13 ]. The only temporal operators in [ 13 ] are strict versions of U and S. Moreover, the semantics is defined w.r.t. bounded past and unbounded future. Definition 10. Let P be a set of propositional variables. LTL-formulae are built from P using the constructors φ1 ∧ φ2, φ1 ∨ φ2, ¬φ1, φ1 U< φ2, and φ1 S< φ2. An LTL-structure is an infinite sequence J = (wi)i≥0 of worlds wi ⊆ P , i ≥ 0, and it satisfies an LTL-formula φ at i ≥ 0 (written J, i |= φ) if

J, i |= p for p ∈ P iff p ∈ wi J, i |= φ1 ∧ φ2 iff J, i |= φ1 and J, i |= φ2 J, i |= φ1 ∨ φ2 iff J, i |= φ1 or J, i |= φ2 J, i |= ¬φ1 iff not J, i |= φ1 J, i |= φ1 U< φ2 iff there is some k > i such that J, k |= φ2

and J, j |= φ1 for all j, i < j < k J, i |= φ1 S< φ2 iff there is some k, 0 ≤ k < i, such that J, k |= φ2 and J, j |= φ1 for all j, k < j < i.

We define the constants true and false by p ∨ ¬p and p ∧ ¬p, respectively, for an arbitrary p ∈ P . We also define first := ¬(true S< true) with the semantics that J, i |= first iff i = 0, i.e. this formula is satisfied exactly at the first time point.

Let from now on φ be an arbitrary but fixed TCQ containing only the CQs α1, . . . , αm. Let furthermore {p1, . . . , pm, p} be the set of propositional variables. For a finite sequence I = (Ii)0≤i≤n of interpretations, its propositional abstraction is the LTL-structure bI := (wi)i≥0, where wi := {pj | Ii |= αj } ∪ {p} if 0 ≤ i ≤ n, and wi := ∅ otherwise. We first transform φ into an LTL-formula fφ that behaves similarly to φ w.r.t. the propositional abstractions of sequences of interpretations I. It is defined inductively on the structure of φ: – fαj := pj for a CQ αj ; – fφ1∧φ2 := fφ1 ∧ fφ2 ; fφ1∨φ2 := fφ1 ∨ fφ2 ; – f#φ1 := false U<(fφ1 ∧ p); f#−φ1 := false S< fφ1 ; – f•φ1 := false U<(fφ1 ∨ ¬p); f•−φ1 := first ∨ false S< fφ1 ; – fφ1 U φ2 := fφ2 ∨ (fφ1 ∧ fφ1 U<(fφ2 ∧ p)); and – fφ1 S φ2 := fφ2 ∨ (fφ1 ∧ fφ1 S< fφ2 ).

We now use the separation theorem from [ 13 ] to transform fφ into an equivalent LTL-formula f φ0 which is a Boolean combination of temporal subformulae that either contain only S< operators or only U< operators. In the proof of this theorem, subformulae of fφ are copied and rearranged, but no additional propositional variables are introduced.

Since we are interested in evaluating φ (and thus fφ and f 0 ) at n, we can φ now reduce f φ0 as follows: First, we replace all variables that are in the scope of a U< by false. The reason for this is that such variables are only evaluated at time points after n, where all variables are false in all propositional abstractions. The resulting formula is then simplified using the simple equivalences ¬true ≡ false, ¬false ≡ true, true ∧ ψ ≡ ψ, true ∨ ψ ≡ true, false ∧ ψ ≡ false, false ∨ ψ ≡ ψ, ψ U< false ≡ false, true U< true ≡ true, and false U< true ≡ true.

This yields a formula f φ00 that does not contain any U< operators and is equivalent to f φ0 at time point n in every LTL-structure of the form bI. This formula is now translated back into a Boolean TCQ φf00 . Recall that the goal φ is to use the algorithm presented in [ 11 ], where negation is allowed in the query language. Furthermore, in that paper a slightly different operator S∗ is used instead of S. The semantics of ¬ and S∗, as employed in [ 11 ], is as follows: I, i |= ¬φ1 iff not I, i |= φ1 I, i |= φ1 S∗ φ2 iff there is some k, 0 ≤ k < i such that I, k |= φ2

and I, j |= φ1 for all j, k < j ≤ i.

In the following, we call any TCQ built using the operators ∧, ∨, ¬, #−, and S∗ a Past-TCQ, which is in particular a temporal query in the sense of [ 11 ]. We can now define the final translation recursively as follows: – φpj := αj for j, 1 ≤ j ≤ m; φp := true; – φf1∧f2 := φf1 ∧ φf2 ; φf1∨f2 := φf1 ∨ φf2 ; – φf1 S< f2 := #−(φf2 ∨ φf1 S∗ φf2 ). φ¬f1 := ¬φf1 ; In [ 7 ], we use the above constructions to show the following result. Theorem 11. For every Boolean TCQ φ there is a Boolean Past-TCQ ψ such that for all I = (Ii)0≤i≤n, we have I, n |= φ iff I, n |= ψ.

Recall that in the above construction the Boolean CQs αj were only copied and rearranged inside the structure of φ. Thus, it is easy to see from Definition 6 that this result also holds for computing the sets of answers of non-Boolean TCQs. Corollary 12. For every TCQ φ there is a Past-TCQ ψ such that FVar(ψ) = FVar(φ) and for all I = (Ii)0≤i≤n, we have Ans(φ, I) = Ans(ψ, I). Let now I = (Ii)i≥0 be an infinite sequence of interpretations representing the observations over all time points. At each time point i ≥ 0, we only have access to the finite prefix I(i) := (Ij )0≤j≤i of I of length i + 1. Let Δ be the shared domain of the interpretations in I. The algorithm from [ 11 ] works as follows on the TCQ ψ constructed in Corollary 12. On input I0, it computes a first-order interpretation I00 of several auxiliary predicates. Intuitively, for each subformula ψ0 of ψ beginning with a past operator, the algorithm stores the 0 answers Ans(ψ0, I(0)) ⊆ ΔFVar(ψ0) for ψ0 in a new relation AIψ00 ⊆ Δk of arity k := |FVar(ψ0)|. The set Ans(ψ, I(0)) can then easily be computed from I0 and I00. Afterwards, the algorithm disregards I0 and keeps only the information computed in I00. On input I1, it then updates I00 to a new interpretation I10, which allows it to compute Ans(ψ, I(1)), and so on.

The memory requirements of this algorithm are bounded by the maximal size of one pair (Ii, Ii0), which is polynomial in the size of Δ, in the number of concept and role names, and in the number of past operators occurring in ψ, and exponential in the number of free variables occurring below past operators. However, the memory requirements do not depend on the length of the sequence of interpretations I(i) seen so far. This is called a bounded history encoding in [ 11 ].

The presented construction has several drawbacks. First, the translations from φ to fφ and from f φ00 to φf00 = ψ may duplicate subformulae, which can φ cause exponential blowups in the size of φ. This could be avoided by applying a reduction similar to the one for propositional LTL in [ 13 ] directly to the TCQ φ. However, since the reduction in [ 13 ] is already non-elementary in the size of the formula (basically one exponential for each U< nested inside a S<, and vice versa), this is not much more efficient. The approach presented in this section is thus best suited for answering simple, small queries φ over large data sets I. 5

A New Algorithm In this section, we present an algorithm that computes the set Ans(φ, I) without the need to eliminate the future operators beforehand, thereby avoiding the non-elementary blowup of the construction described in the previous section. However, the memory requirements of this new algorithm are not independent of the number of previous time points. From now on, let φ be a fixed TCQ and I = (Ii)i≥0 be a fixed infinite sequence of interpretations over the same finite domain Δ. For i ≥ 0, we denote by I(i) := (Ij )0≤j≤i the finite prefix of I of length i + 1. Our algorithm iteratively computes the sets Ans(φ, I(i)). It uses as data structure so-called answer formulae, which represent TCQs in which some parts have already been evaluated. In particular, they contain no more CQs, but rather sets of already computed answers to subqueries. Additionally, they may contain variables (different from those in NV) that serve as place-holders for subqueries that have to be evaluated at the next time point.

For ease of presentation, we assume in the following that NV is finite and that answers are of the form a : NV → Δ instead of a : FVar(φ) → Δ. In an implementation, one would of course already restrict the intermediate computations of answers for subqueries ψ ∈ Sub(φ) to FVar(ψ). But then one has to be more careful when combining answers to different subqueries. Thus, when we talk about answers, we mean mappings a : NV → Δ, and in particular Ans(. . .) refers to a set of such mappings, i.e. a subset of ΔNV .

Definition 13. Let FSub(φ) denote the set of all subqueries of φ of the form #ψ1, •ψ1, or ψ1 U ψ2. For j ≥ 0, we denote by Varjφ the set of all variables of the form xjψ for ψ ∈ FSub(φ). The set AFiφ of all answer formulae for φ at i ≥ 0 is the smallest set satisfying the following conditions: – Every set A ⊆ ΔNV is an answer formula for φ at i. – Every xjψ ∈ Varjφ with j ≤ i is an answer formula for φ at i.

– If α1 and α2 are answer formulae for φ at i, then so are α1 ∩ α2 and α1 ∪ α2. In order to evaluate these answer formulae, we introduce the notion of correctness. Intuitively, an answer formula α for φ at i is correct for i if we obtain the set Ans(φ, I(i)) by replacing the variables xjψ in α by appropriate sets of answers and evaluating ∩ and ∪ as set intersection and union, respectively. Definition 14. We define the function evaln : AFφn → 2ΔNV , n ≥ 0, as follows: – evaln(A) := A if A ⊆ ΔNV ; Ans(ψ1, I(n), j + 1) if j < n and ψ = #ψ1 or ψ = •ψ1; Ans(ψ, I(n), j + 1) if j < n and ψ = ψ1 U ψ2; – evaln(xjψ) := ∅ if j = n and ψ = #ψ1 or ψ = ψ1 U ψ2;  ΔNV if j = n and ψ = •ψ1; – evaln(α1 ∩ α2) := evaln(α1) ∩ evaln(α2); and – evaln(α1 ∪ α2) := evaln(α1) ∪ evaln(α2).

We say that a mapping Φ : Sub(φ) → AFiφ is correct for i ≥ 0 if for all n ≥ i and for all ψ ∈ Sub(φ), we have evaln(Φ(ψ)) = Ans(ψ, I(n), i).

In particular, if Φ : Sub(φ) → AFiφ is correct for i, then evali(Φ(φ)) = Ans(φ, I(i)), which is the set we want to compute. The algorithm works as follows. It first computes a mapping Φ0 that is correct for 0, which is used to compute the next mapping Φ1 when the interpretation I1 becomes available. This mapping is correct for 1 and can be used to compute the next mapping Φ2, and so on. In each step, to compute Φi+1, we only need Φi and the interpretation Ii+1. Definition 15. We recursively define the mapping Φ0 : Sub(φ) → AF0φ: – Φ0(ψ1) := Ans(ψ1, I(0)) if ψ1 is a CQ; – Φ0(ψ1 ∧ ψ2) := Φ0(ψ1) ∩ Φ0(ψ2); Φ0(ψ1 ∨ ψ2) := Φ0(ψ1) ∪ Φ0(ψ2); – Φ0(#ψ1) := x0#ψ1 ; Φ0(#−ψ1) := ∅; – Φ0(•ψ1) := x0•ψ1 ; Φ0(•−ψ1) := ΔNV ; – Φ0(ψ1 U ψ2) := Φ0(ψ2) ∪ Φ0(ψ1) ∩ x0ψ1 U ψ2 ; Φ0(ψ1 S ψ2) := Φ0(ψ2).

We assume for this definition that CQs ψ1 are answered using a different mechanism, e.g. by evaluating the first-order query ψ1 over the “database” I0 [ 1 ].

Assume now that Φi−1 : Sub(φ) → AFiφ−1 is a function containing only variables with index i − 1. We proceed as follows to construct a new function that contains only variables with index i. We first define a function Φ0 : Sub(φ) → AFiφ i similarly to Definition 15 that may still contain variables with index i − 1. We then iteratively replace these variables until only variables with index i are left. Definition 16. Let i > 0 and Φi−1 : Sub(φ) → AFiφ−1. We recursively define the mapping Φi0 : Sub(φ) → AFiφ as follows: – Φi0(ψ1) := Ans(ψ1, I(i)) if ψ1 is a CQ; – Φi0(ψ1 ∧ ψ2) := Φi0(ψ1) ∩ Φi0(ψ2); – Φi0(#ψ1) := xi#ψ1 ; Φi0(#−ψ1) := Φi−1(ψ1); – Φi0(•ψ1) := xi•ψ1 ; Φi0(•−ψ1) := Φi−1(ψ1); – Φi0(ψ1 U ψ2) := Φi0(ψ2) ∪ Φi0(ψ1) ∩ xiψ1 U ψ2 ; and – Φi0(ψ1 S ψ2) := Φi0(ψ2) ∪ Φi0(ψ1) ∩ Φi−1(ψ1 S ψ2) .

Φi0(ψ1 ∨ ψ2) := Φi0(ψ1) ∪ Φi0(ψ2) In order to remove the “old” variables with index i − 1, we now substitute them appropriately. For example, since xi#−ψ1 is a place-holder for the answers to ψ w.r.t. I(n) at i, we can now replace it by Φi0(ψ). However, this formula may itself contain another old variable, and thus we have to be careful about the order in which we do these substitutions. Since each Φi0(ψ) can contain only variables that refer to subqueries of ψ, by replacing the variables for “smaller” subqueries first, we ensure that all variables are eliminated. The details of this construction can be found in [ 7 ]. We obtain a mapping Φi : Sub(φ) → AFiφ that is correct for i. Lemma 17. For each i ≥ 0, the mapping Φi is correct for i.

Consider now the algorithm, which, on input φ and I, computes the mappings Φi as described above, and outputs evali(Φi(φ)) for each i ≥ 0. The following is a trivial consequence of the correctness of these mappings.

Theorem 18. Given a TCQ φ and an infinite sequence I = (Ii)i≥0 of interpretations, the algorithm outputs Ans(φ, I(i)) for each i ≥ 0.

It is now easy to compute the sets evali(Φi(φ)) = Ans(φ, I(i)) for i ≥ 0 since each of the variables xiψ in Φi(φ) simply has to be replaced by either ∅ or ΔNV (see Definition 14). However, as mentioned earlier, the size of the formula Φi(φ) may depend exponentially on the length i of the current sequence of interpretations. For example, the answer formula Φ10(φ) for φ = C(x) S(A(x) U B(x)) is Φ10(ψ) ∪ (C1 ∩ (B0 ∪ (A0 ∩ x0ψ))), where ψ := A(x) U B(x), Φ10(ψ) = B1 ∪ (A1 ∩ x1ψ), A0 := Ans(A(x), I(0)), and similarly for the other CQs and time points. After replacing x0ψ by Φ10(ψ), the variable x1ψ occurs twice in Φ1(φ). In general, Φi(φ) will contain 2i occurrences of the variable xiψ. However, applying equivalences like the associativity, commutativity, distributivity, and absorption laws for ∩ and ∪ does not affect the semantics of an answer formula (which is given by eval), and hence Φ1(φ) ≡ Φ10(ψ) ∪ (C1 ∩ (B0 ∪ (A0 ∩ Φ10(ψ)))) ≡ Φ10(ψ) ∪ (C1 ∩ B0) ∪ (C1 ∩ A0 ∩ Φ10(ψ)) ≡ Φ10(ψ) ∪ (C1 ∩ B0)

ψ ≡ ((C1 ∩ B0) ∪ B1) ∪ (A1 ∩ x1 ) The resulting formula contains x1ψ only once. In general, the formula Φi(φ) is equivalent to Di ∪ (Ai ∩ xiψ), where D0 := B0 and Di := (Ci ∩ Di−1) ∪ Bi for all i > 0. Thus, the algorithm only has to store the two sets Ai, Di ⊆ ΔNV at each time point, i.e. we achieve a bounded history encoding, as in [ 11 ]. If the formula φ contains no future operators, then the answer formulae contain no variables and can always be fully evaluated to a subset of ΔNV . In this case, our algorithm can be seen as a variant of the one from [ 11 ] for less expressive queries.

The example demonstrates that it is important that the computed answer formulae are simplified at each step, while preserving their semantics under eval. However, this does not guarantee a bounded history encoding as in [ 11 ]. 6

Conclusions We have introduced the reasoning task of temporal OBDA over DL-Lite knowledge bases and shown how to reduce this task to answering queries over temporal databases, similar to what was done for the atemporal case [ 8 ]. We then presented three approaches to solve the latter problem. The first involves storing the whole history of the database and re-evaluating the query at each time point using a temporal database query language like ATSQL [ 12 ].

The second approach works by eliminating the future operators and evaluating the resulting query using the algorithm of [ 11 ], which achieves a bounded history encoding. Although independent of the length of the history, this involves a non-elementary blow-up in the size of the query. Finally, we presented an algorithm that works directly with the future operators. We showed that the algorithm computes exactly the desired answers, but its space requirements are in general not independent of the length of the history. In future work, we will try to achieve a bounded history encoding for certain classes of TCQs, and compare the performance of all three approaches on temporal databases. 15. Hülsmann, K., Saake, G.: Theoretical foundations of handling large substitution sets in temporal integrity monitoring. Acta Informatica 28(4), 365–407 (1991) 16. Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past.

In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science (LICS’02). pp. 383–392. IEEE Press (2002) 17. Pnueli, A.: The temporal logic of programs. In: Proc. of the 18th Annual Symp.

on Foundations of Computer Science (SFCS’77). pp. 46–57 (1977) 18. Saake, G., Lipeck, U.W.: Using finite-linear temporal logic for specifying database dynamics. In: Börger, E., Büning, H.K., Richter, M.M. (eds.) Proc. of the 2nd Workshop on Computer Science Logic (CSL’88), Lecture Notes in Computer Science, vol. 385, pp. 288–300. Springer-Verlag (1989) 19. Toman, D.: Logical data expiration. In: Chomicki, J., van der Meyden, R., Saake, G. (eds.) Logics for Emerging Applications of Databases, chap. 6, pp. 203–238.

Springer-Verlag (2004) 20. Wilke, T.: Classifying discrete temporal properties. In: Proc. of the 16th Annual Symp. on Theoretical Aspects of Computer Science (STACS’99). Lecture Notes in Computer Science, vol. 1563, pp. 32–46. Springer-Verlag (1999)

References

1. Abiteboul , S. , Hull , R. , Vianu , V. : Foundations of Databases. Addison-Wesley ( 1995 )

2. Artale , A. , Kontchakov , R. , Ryzhikov , V. , Zakharyaschev , M.: DL-Lite with temporalised concepts, rigid axioms and roles . In: Ghilardi, S. , Sebastiani , R . (eds.) Proc. of the 6th Int. Symp. on Frontiers of Combining Systems (FroCoS'09). Lecture Notes in Computer Science , vol. 5749 , pp. 133 - 148 . Springer-Verlag ( 2009 )

3. Artale , A. , Kontchakov , R. , Ryzhikov , V. , Zakharyaschev , M. : Temporal conceptual modelling with DL-Lite . In: Proc. of the 2010 Int. Workshop on Description Logics (DL'10) . CEUR-WS , vol. 573 ( 2010 )

4. Artale , A. , Kontchakov , R. , Ryzhikov , V. , Zakharyaschev , M.: A cookbook for temporal conceptual data modelling with description logics . CoRR abs/1209 .5571 ( 2012 ), http://arxiv.org/abs/1209.5571

5. Baader , F. , Borgwardt , S. , Lippmann, M.: Temporalizing ontology-based data access . In: Bonacina, M.P. (ed.) Proc. of the 24th Int. Conf. on Automated Deduction (CADE'13). Lecture Notes in Artificial Intelligence , vol. 7898 , pp. 330 - 344 . Springer-Verlag ( 2013 )

6. Borgwardt , S. , Lippmann, M. , Thost , V. : Temporal query answering in the description logic DL-Lite . In: Fontaine, P. , Ringeissen , C. , Schmidt , R.A . (eds.) Proc. of the 9th Int. Symp. on Frontiers of Combining Systems (FroCoS'13). Lecture Notes in Computer Science , Springer-Verlag, Nancy, France ( 2013 ), to appear.

7. Borgwardt , S. , Lippmann, M. , Thost , V. : Temporal query answering w .r. t. DL-Liteontologies. LTCS-Report 13-05 , Chair of Automata Theory, TU Dresden, Dresden, Germany ( 2013 ), see http://lat.inf.tu-dresden.de/research/reports.html.

8. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Poggi , A. , RodriguezMuro , M. , Rosati , R.: Ontologies and databases: The DL-Lite approach . In: Tessaris, S. , Franconi , E. , Eiter , T. , Gutierrez , C. , Handschuh , S. , Rousset , M.C. , Schmidt , R.A . (eds.) Reasoning Web, 5th Int. Summer School 2009 , Tutorial Lectures, Lecture Notes in Computer Science, vol. 5689 , pp. 255 - 356 . Springer-Verlag ( 2009 )

9. Calvanese , D. , Giacomo , G.D. , Lembo , D. , Lenzerini , M. , Rosati , R. : DL-Lite: Tractable description logics for ontologies . In: Proc. of the 20th Nat. Conf. on Artificial Intelligence (AAAI'05) . pp. 602 - 607 . AAAI Press ( 2005 )

10. Chandra , A.K. , Merlin , P.M.: Optimal implementation of conjunctive queries in relational data bases . In: Hopcroft, J.E. , Friedman , E.P. , Harrison , M.A . (eds.) Proc. of the 9th Annual ACM Symp. on Theory of Computing (STOC'77) . pp. 77 - 90 . ACM Press ( 1977 )

11. Chomicki , J.: Efficient checking of temporal integrity constraints using bounded history encoding . ACM Transactions on Database Systems 20 ( 2 ), 148 - 186 ( 1995 )

12. Chomicki , J. , Toman , D. , Böhlen , M.H. : Querying ATSQL databases with temporal logic . ACM Transactions on Database Systems 26 ( 2 ), 145 - 178 ( 2001 )

13. Gabbay , D. : Declarative past and imperative future . In: Banieqbal, B. , Barringer , H. , Pnueli , A . (eds.) Proc. of the 1987 Coll. on Temporal Logic in Specification. Lecture Notes in Computer Science , vol. 398 , pp. 409 - 448 . Springer-Verlag ( 1989 )

14. Gutiérrez-Basulto , V. , Klarman , S. : Towards a unifying approach to representing and querying temporal data in description logics . In: Krötzsch, M. , Straccia , U . (eds.) Proc. of the 6th Int. Conf. on Web Reasoning and Rule Systems (RR'12). Lecture Notes in Computer Science , vol. 7497 , pp. 90 - 105 . Springer-Verlag ( 2012 )