=Paper=
{{Paper
|id=Vol-1193/paper_60
|storemode=property
|title=Temporal OBDA with LTL and DL-Lite
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_60.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleKKRWZ14
}}
==Temporal OBDA with LTL and DL-Lite==
https://ceur-ws.org/Vol-1193/paper_60.pdf
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)