=Paper=
{{Paper
|id=Vol-477/paper-17
|storemode=property
|title=Extending DL-Lite Sometime in the Future
|pdfUrl=https://ceur-ws.org/Vol-477/paper_53.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleKRZ09
}}
==Extending DL-Lite Sometime in the Future==
https://ceur-ws.org/Vol-477/paper_53.pdf
Extending DL-Lite Sometime in the Future
A. Artale,1 R. Kontchakov,2 V. Ryzhikov,1 and M. Zakharyaschev2
1 2
KRDB Research Centre School of Comp. Science and Inf. Sys.
Free University of Bozen-Bolzano Birkbeck College
I-39100 Bolzano, Italy London WC1E 7HX, UK
lastname @inf.unibz.it {roman,michael}@dcs.bbk.ac.uk
1 Introduction
Many types of temporalised description logics (DLs) have been suggested and
investigated in the past 15 years. We refer the reader to the survey papers and
monograph [9, 14, 3, 16], where the history of the development of both interval
and point-based temporal extensions of DLs is discussed in full detail.
Temporal operators can be applied in various ways in order to introduce a
temporal dimension to a DL. In particular, they can be used as constructors
for concepts, roles, TBox and ABox axioms (such concepts, roles or axioms are
called temporalised). Alternatively, one may declare a certain concept, role or
axiom to be regarded as rigid in the sense that its interpretation does not change
in time—usually, the rigidity can be expressed if temporal operators are allowed
to be applied to the respective construct. A number of complexity results have
been obtained for different combinations of temporal operators and DLs. For
instance, the following is known for combinations of ALC with the linear-time
temporal logic LT L: the satisfiability problem for the temporal ALC is
1. undecidable if temporalised concepts with rigid axioms and roles are allowed
in the language (actually, a single rigid role is enough); see [14] and references
therein;
2. 2ExpTime-complete if the language allows rigid concepts and roles with
temporalised axioms [10];
3. ExpSpace-complete if the language allows temporalised concepts and ax-
ioms (but no rigid or temporalised roles) [14];
4. ExpTime-complete if the language allows only temporalised concepts and
rigid axioms (but no rigid or temporalised roles) [17, 4].
In other words, as long as one wants to express the temporal behaviour of only
axioms and concepts (but not roles), then the resulting combination is likely to
be decidable. As soon as the combination allows reasoning about the temporal
behaviour of binary relations it becomes undecidable, unless we limit the means
to describe the temporal behaviour of concepts. Furthermore, we notice that
better computational behaviour is exhibited in cases where rigid axioms are
used instead of more general temporalised ones.
In this paper, we are interested in the scenario where axioms are rigid, con-
cepts are temporalised and roles may be rigid or local (i.e., can change arbitrar-
ily). To regain decidability in this case one has to restrict either the temporal [8]
or the DL component [7]. The decidable (in fact 2ExpTime-complete) logic
S5ALCQI [8] is obtained by combining the modal logic S5 with ALCQI. This
approach weakens the temporal dimension to the much simpler S5, which can
nevertheless represent rigid concepts and roles, and allows one to state that
concept and role memberships change in time (however, without discriminating
between changes in the past and in the future).
Temporal extensions of various dialects of DL-Lite have also been stud-
ied [7]. The most interesting result of [7] is the combination TDL-Litebool of
DL-LiteN bool [1, 2]—i.e., DL-Lite extended with full Booleans over concepts and
cardinality restrictions on roles—with LT L, which allows rigid roles and tempo-
ralised axioms and concepts and which was shown to be ExpSpace-complete.
In this paper, we consider another temporal extension TDL-Lite3 bool of the
3
logic DL-LiteN bool . The logic TDL-Litebool weakens TDL-Litebool of [7] in two ways:
(i ) axioms can be only rigid, and (ii ) the temporal component is limited to the
operators 3 (sometime in the future) and 2 (always in the future). We show that
reasoning in TDL-Lite3 3 3
bool and TDL-Litecore (a sub-language of TDL-Litebool that
allows only very primitive concept inclusions) is NP-complete. Thus, allowing
only 3 and 2 as temporal operators, and forbidding temporalised axioms reduces
the complexity from ExpSpace—for TDL-Litebool as in [7]—to NP. This result
matches the minimal complexity of the two components: in case of TDL-Lite3 bool
both components (DL-LiteN bool and LT L with 3 only) are NP-complete; in case
of TDL-Lite3 N
core one component, DL-Litecore , is NLogSpace-complete, while
the other is NP-complete. It should be noted, however, that TDL-Lite3 bool is not
simply a fusion (or independent join) of its components.
2 TDL-Lite3
bool : a Simple Temporal Description Logic
We begin by defining the description logic TDL-Lite3 bool as a temporalisation of
DL-LiteN bool [1, 2], which extends the original DL-Liteu,F language [11–13] with
full Booleans between concepts and cardinality restrictions on roles.
The language of TDL-Lite3 bool contains object names a0 , a1 , . . . , concept names
A0 , A1 , . . . , local role names P0 , P1 , . . . and rigid role names G0 , G1 , . . . ; roles
R, basic concepts B and concepts C, D are defined as follows:
R ::= Pi | Pi− | Gi | G−
i ,
B ::= ⊥ | Ai | ≥ q R,
C, D ::= B | ¬C | C uD | 3C,
where q ≥ 1 is a natural number. A TDL-Lite3 bool TBox T consists of concept
inclusions of the form C v D, and an ABox A of the assertions of the form:
n
B(a), n R(a, b), 2B(a) and 2R(a, b), where B is a basic concept, R a role,
a, b object names and n denotes the sequence of n next-time operators , for
n ≥ 0. The TBox and ABox together form the knowledge base (KB) K = (T , A).
A TDL-Lite3 bool interpretation I is a function on natural numbers N:
I(n) I(n) I(n)
I(n) = ∆I , aI0 , . . . , A0 , . . . , P0 , . . . , G0 , . . . ,
I(n)
where ∆I is a non-empty set, the domain of I, aIi ∈ ∆I , Ai ⊆ ∆I and
I(n) I(n)
Pi , Gi ⊆ ∆I × ∆I , for all i and all n ∈ N. Furthermore, aIi 6= aIj for i 6= j
I(n) I(m)
(which means that we adopt the unique name assumption) and Gi = Gi ,
for all n, m ∈ N. The role and concept constructs are interpreted in I as follows:
for each moment of time n ∈ N,
I(n)
(Ri− )I(n) = (y, x) ∈ ∆I × ∆I | (x, y) ∈ Ri ⊥I(n) = ∅,
,
(≥ q R)I(n) = x ∈ ∆I | ]{y | (x, y) ∈ RI(n) } ≥ q , (¬C)I(n) = ∆I \ C I(n) ,
[
(C u D)I(n) = C I(n) ∩ DI(n) , (3C)I(n) = C I(k) ,
k>n
where ]X is the cardinality of X; note that the 3 is interpreted in the strong
sense, i.e., it does not include the present. We will use standard abbreviations
such as C1 t C2 = ¬(¬C1 u ¬C2 ), > = ¬⊥, ∃R = (≥ 1 R) and 2C = ¬3¬C.
The satisfaction relation |= is defined as follows:
I |= C v D iff C I(n) ⊆ DI(n) for all n ≥ 0,
I |= n
B(a) iff aI ∈ B I(n) ,
I |= 2B(a) iff aI ∈ B I(n) for all n > 0,
I |= n
R(a, b) iff (aI , bI ) ∈ RI(n) ,
I |= 2R(a, b) iff (aI , bI ) ∈ RI(n) for all n > 0.
We say an interpretation I is a model of a KB K if I |= α for all α in K. In
this case we also say that K is consistent and we write I |= K. A concept A
(role R) is satisfiable w.r.t. K if there exists a model I of K and n ≥ 0 such that
AI(n) 6= ∅ (RI(n) 6= ∅).
Note that TDL-Lite3 bool is not a simple fusion of the two component logics,
DL-LiteN bool and LT L. Indeed, let K = ({3∃R− v ⊥, ∃R v 3∃R}, {∃R(a)}). It
is easy to see that K is not satisfiable in TDL-Lite3 bool . However, it is satisfiable
both in DL-LiteN bool (if we substitute the temporal concepts by fresh DL-LiteN bool
concepts) and in LT L (by substituting ∃R concepts with fresh atomic proposi-
tions).
3 Satisfiability of TDL-Lite3
bool KBs is NP-complete
To prove the NP complexity result we first establish in Section 3.1 a relation
between TDL-Lite3 1
bool and the one-variable fragment QT L of first-order tem-
poral logic. This will allow us to polynomially reduce the satisfiability problem
in TDL-Lite3 3
bool to that in TDL-Lite0 , a language that has neither rigid roles
nor role assertions. Next, in Section 3.2, we show that a TDL-Lite3 0 KB K is
satisfiable iff there exists a quasimodel for it. Then we show that if there is a
quasimodel for K then there exists an ultimately periodic quasimodel for it such
that both the length of the prefix and the length of the period are polynomial
in the length of K. Finally, in Section 3.3, we describe an algorithm that checks
(in non-deterministic polynomial time) the existence of an ultimately periodic
quasimodel for a given TDL-Lite3 0 KB.
3.1 TDL-Lite3
bool in the context of First-Order Temporal Logic
For a TDL-Lite3 bool KB K = (T , A), let ob(A) be the set of all object names
occurring in A. Let role± (K) be the set of all (local and rigid) role names,
together with their inverses, occurring in K, and grole± (K) the set of rigid role
names, together with their inverses, occurring in K. For R ∈ role± (K), let QR K
be the set of natural numbers containing 1 and all the numerical parameters q
for which ≥ q R occurs in K. Denote by ev(K) the set of all concepts of the form
3C occurring in K and, finally, let NK = {n | n B(a) ∈ A or n R(a, b) ∈ A};
without loss of generality, we assume that NK is non-empty.
With every object name a ∈ ob(A) we associate the individual constant a
of QT L1 , the one variable fragment of first-order temporal logic over (N, <),
and with every concept name A the unary predicate A(x) from the signature of
QT L1 . For each R ∈ role± (K), we also introduce |QR K | fresh unary predicates
Eq R(x), for q ∈ QR K . Intuitively, for each n ≥ 0, E 1 R(x) and E1 R− (x) repre-
sent the domain and range of R at moment n (i.e., E1 R(x) and E1 R− (x) are
interpreted by the sets of points with at least one R-successor and at least one
R-predecessor at moment n, respectively), while Eq R(x) and Eq R− (x) repre-
sent the sets of points with at least q distinct R-successors and at least q distinct
R-predecessors at moment n.
By induction on the construction of a TDL-Lite3 bool concept C we define the
QT L1 - formula C ∗ :
⊥∗ = ⊥, (A)∗ = A(x),
(≥ q R)∗ = Eq R(x), (¬C)∗ = ¬C ∗ (x),
(C1 u C2 ) ∗
= C1∗ (x) ∧ C2∗ (x), (3C)∗ = 3C ∗ (x),
and then extend this translation to TDL-Lite3
bool TBoxes T :
^
T∗= 2+ ∀x (C1∗ (x) → C2∗ (x)),
C1 vC2 ∈T
where 2+ ϕ = ϕ ∧ 2ϕ. The following formulas express some natural properties of
the role domains and ranges. For R ∈ role± (K), we need two QT L1 -sentences:
εR = ∃x E1 R(x) → ∃x inv(E1 R)(x), (1)
^
δR = ∀x Eq0 R(x) → Eq R(x) , (2)
q,q 0 ∈QR 0
K , q >q
q 0 >q 00 >q for no q 00 ∈QR
K
where inv(E1 R) is the predicate E1 P − (x) if R = P and E1 P (x) if R = P − .
Sentence (1) says that if the domain of R is non-empty then its range is non-
empty either.
Without loss of generality we may assume that if R is a rigid role and A
contains n R(a, b) or 2R(a, b) then it also contains both R(a, b) and 2R(a, b).
Then we define ‘temporal slices’ of the ABox A by taking:
A2 = R(a, b) | 2R(a, b) ∈ A or 2inv(R)(b, a) ∈ A ,
An = R(a, b) | n R(a, b) ∈ A or n inv(R)(b, a) ∈ A ∪
R(a, b) | n > 0 and either 2R(a, b) ∈ A or 2inv(R)(b, a) ∈ A .
The QT L1 translation of the ABox A is defined as follows:
^ ^ ^
A∗ = n ∗
B (ai ) ∧ n
EqR,a,An R(a) ∧ 2EqR,a,A2 R(a),
n
B(ai )∈A R(a,b)∈An R(a,b)∈A2
where, for a role R, a ∈ ob(A) and any ABox A0 ,
0
qR,a,A0 = max({0} ∪ {q ∈ QR
K | R(a, ai ) ∈ A , 1 ≤ i ≤ q & ai1 6= ai2 if i1 6= i2 }).
Finally, we set
^ ^ ^
K‡ = T ∗ ∧ 2+ εR ∧δR ∧ 2+ ∀x Eq T (x) ↔ 2Eq T (x) ∧ A∗ .
R∈role± (K) T ∈grole± (K) q∈QT
K
Observe that the length of K‡ is polynomial in the length of K. It can be shown
(for details see [7, Theorem 2 and Corollary 3]) that we have:
Theorem 1. A TDL-Lite3 1 ‡
bool KB K is satisfiable iff the QT L -sentence K is
satisfiable.
Denote by TDL-Lite3 3
0 the fragment of TDL-Litebool without rigid roles and
ABox assertions of the form 2R(a, b) or n R(a, b). By Theorem 1, this fragment
is of the same complexity as TDL-Lite3bool :
Lemma 1. Given a TDL-Lite3 bool KB K one can construct (in polynomial time)
a TDL-Lite3
0 KB K 0
such that K and K0 are equisatisfiable.
Proof. Let A0 be the part of A that contains no assertions of the form 2R(a, b)
or n R(a, b). Then we set K0 = (T ∪ T 0 , A0 ∪ A0 ), where
T 0 = 2(≥ q T ) v (≥ q T ), (≥ q T ) v 2(≥ q T ) | q ∈ QTK , T ∈ grole± (K) ,
A0 ={ n
(≥ qR,a,An R)(a) | R(a, b) ∈ An } ∪ {2(≥ qR,a,A2 R)(a) | R(a, b) ∈ A2 }.
Clearly, K‡ = (K0 )‡ . Then the claim immediately follows from Theorem 1. q
3.2 Quasimodels for TDL-Lite3
0
In this section, we define a notion of a quasimodel for a TDL-Lite3 0 KB and show
that a TDL-Lite3 0 KB is satisfiable iff there is an ultimately periodical quasi-
model with the length of both the prefix and period bounded by a polynomial
function in the length of K. It will follow then that the satisfiability problem for
TDL-Lite3 3
0 , and thus for TDL-Litebool , is in NP.
Let K = (T , A) be a TDL-Lite3 0 KB. We introduce, for every concept of the
form 3C, a fresh concept name FC , the surrogate of 3C, and then, for a concept
D, denote by D the result of replacing each 3C in D with the surrogate FC . For
a TDL-Lite3 N
0 TBox T , denote by T the DL-Litebool TBox obtained by replacing
every concept C in T with C.
Let cl(K) be the closure under negation of all concepts occurring in T together
with the ∃R, for R ∈ role± (K), and the B, for n B(a) ∈ A or 2B(a) ∈ A. A
type for K is a subset t of cl(K) such that
– C u D ∈ t iff C, D ∈ t, for every C u D ∈ cl(K);
– ¬C ∈ t iff C 6∈ t, for every C ∈ cl(K).
d
A type t for K is realisable if the concept C∈t C is satisfiable w.r.t. T .
A function r mapping N to types for K is called a coherent and saturated run
for K if the following conditions are satisfied:
(real) r(i) is realisable, for all i ≥ 0;
(coh) for all i ≥ 0 and 3C ∈ ev(K), if C ∈ r(i) then 3C ∈ r(j), for all j with
0 ≤ j < i;
(sat) for all i ≥ 0 and 3C ∈ ev(K), if 3C ∈ r(i) then there is j > i such that
C ∈ r(j).
A witness for K is a pair of the form (r, Ξ), where r is a coherent and saturated
run for K, Ξ ⊆ N and |Ξ| ≤ 1.
Given a run r and a finite sequence s = (s(0), . . . , s(n)) of types for K, we
set:
r 0;
(role) for all i ≥ 0 and R ∈ role± (K), if ∃R− ∈ r(i), for some (r, Ξ) ∈ W , then
(rR , {iR }) ∈ W , ∃R ∈ rR (iR ) and either i ≤ iR < K or K ≤ iR < L.
Theorem 2. A TDL-Lite3 0 KB K is satisfiable iff there exists a quasimodel
Q = hW, K, Li for K such that L ≤ max NK + |ev(K)| · (|role± (K)| + 2) + 3.
Proof. (⇒) Suppose I |= K. For m ≥ 0, let
Fm = R ∈ role± (K) | there is i ≥ m with RI(i) 6= ∅ .
Lemma 2. For all n, v ≥ 0, there exists m such that n ≤ m ≤ n + v · |F0 | and,
for every role R ∈ F0 , either R ∈ Fm+v+1 or R ∈
/ Fm+1 .
Proof. If a role R is non-empty infinitely often then R ∈ Fm+v+1 , for any m.
So we have to consider only those roles that are non-empty finitely many times.
Let
FG = R ∈ role± (K) | there is i ≥ 0 such that R ∈ / Fi .
For R ∈ FG∩F0 , let iR = min i | R ∈ / Fi+1 (i.e., iR is the last moment when R
is non-empty). If max{iR | R ∈ FG} ≤ n + v · |F0 |, we take m = max({n} ∪ {iR |
R ∈ FG}). Clearly, FG ∩ Fm+1 = ∅ (so all roles in FG are empty after m).
Otherwise, FG ∩ F0 6= ∅ and without loss of generality we may assume that
FG ∩ F0 = {R1 , . . . , Rs } and iR1 ≤ iR2 ≤ · · · ≤ iRs . If iR1 > n + v, we take
m = n; then FG∩F0 ⊆ Fm+v+1 (all roles in FG∩F0 are non-empty after m+v).
Otherwise, iR1 ≤ n + v and iRs > n + v · |F0 |, whence iRs − iR1 > (v − 1) · |F0 |.
Let j0 be the smallest j, 1 ≤ j < s, such that iRj ≥ n and iRj+1 − iRj > v (it
exists as s ≤ |F0 |) and set m = iRj0 . We then have R1 , . . . , Rj0 ∈ / Fm+1 and
Rj0 +1 , . . . , Rs ∈ Fm+v+1 . q
Let N = max NK and V = |ev(K)|. By Lemma 2, there exists M with
N ≤ M ≤ N + V · |F0 | such that, for every role R ∈ F0 , either R ∈ FK or
R∈ / FM +1 , where K = M + V + 1. We then set iR = min{i ≥ K | RI(i) 6= ∅},
for each R ∈ FK , and iR = max{i | RI(i) 6= ∅}, for each R ∈ F0 \ FM +1 .
Clearly, for each R ∈ F0 , either iR ≤ M or iR ≥ K. For d ∈ ∆I , denote
rd : i 7→ {C ∈ cl(K) | d ∈ C I(i) } (it evidently is a coherent and saturated run).
For each R ∈ F0 , we fix some dR ∈ (∃R)I(iR ) and set rR = rdR . Let
W = (rR , {iR }) | R ∈ F0 ∪ (raI , ∅) | a ∈ ob(A) .
Clearly, both (runs) and (obj) hold. We also have ∃R− ∈ r(i) iff ∃R ∈ rR (iR )
and (rR , {iR }) ∈ W , for all (r, Ξ) ∈ W and i ≥ 0.
We now transform W by expanding and pruning runs in such a way that the
r(i) are never thrown out, for (r, Ξ) ∈ W and i ∈ Ξ.
Lemma 3. For each coherent and saturated run r,
|{i | r(i) is not stutter-invariant}| ≤ |ev(K)|.
Proof. Suppose there are 0 ≤ i1 < · · · < in such that n > |ev(K)| and
r(i1 ), . . . , r(in ) are not stutter-invariant, i.e., for each 1 ≤ j ≤ n, there are
3Cj ∈ ev(K) with ¬3Cj , Cj ∈ r(ij ). Then there is 3C ∈ ev(K) such that
¬3C, C ∈ r(ij ) and ¬3C, C ∈ r(ij 0 ) for some 0 ≤ ij < ij 0 . As C ∈ r(ij 0 ), we
obtain, by (coh), 3C ∈ r(ij ), contrary to ¬3C ∈ r(ij ). q
Step 1. By Lemma 3, for each (r, Ξ) ∈ W , there is jr , M < jr ≤ K, such
that r(jr ) is stutter-invariant. Set
r0 = r jr }.
It should be clear that r0 is a coherent and saturated run. Denote by W 0 the set
of all (r0 , Ξ 0 ) constructed as above. Clearly, r0 (K) is stutter-invariant, for each
(r0 , Ξ 0 ) ∈ W 0 . It is easy to see that, for each R ∈ F0 , we have (rR 0
, {i0R }) ∈ W 0
0 0
and either iR ≤ M or iR ≥ K.
Step 2. For (r0 , Ξ 0 ) ∈ W 0 , let Ξ 0 = {i > K | r0 (i) not stutter-invariant}. By
Lemma 3, |Ξ 0 | ≤ |ev(K)|. We prune the run r0 , if Ξ 0 ∪ Ξ 0 6= ∅, by removing all
stutter-invariant r0 (i) with K < i < max(Ξ 0 ∪ Ξ 0 ). Denote the resulting run by
r00 . It should be clear that r00 is coherent and saturated. Set
Ξ 00 = {i | i ∈ Ξ 0 , i ≤ K} ∪ {K + |{j ∈ Ξ 0 ∪ Ξ 0 | j ≤ i}| | i ∈ Ξ 0 , i > K}.
Let W 00 be the set of all witnesses (r00 , Ξ 00 ) constructed as above and L = K +
V + 2. It follows that, for each (r00 , Ξ 00 ) ∈ W 00 , all the types r00 (i) are stutter-
invariant, for i ≥ L, and thus (stuttr) holds. It is also easy to see that, for each
00
R ∈ F0 , we have (rR , {i00R }) ∈ W 00 and K ≤ i00R < L, if R ∈ FK , and i00R ≤ M , if
R∈ / FM +1 . Therefore, we have (role). So, Q = hW 00 , K, Li is as required.
(⇐) Let Q = hW, K, Li be a quasimodel for K. We construct a model for K‡
which, by Theorem 1, is enough to show that K is satisfiable. Let
≥i
R = ra | (ra , ∅) ∈ W ∪ rR | (rR , {iR }) ∈ W, 0 ≤ i ≤ iR ∪
iR ≥ K .
Clearly, each r ∈ R is a coherent and saturated run for K. Moreover, if we have
(rR , {iR }) ∈ W and iR < K then there is r0 ∈ R with ∃R ∈ r0 (i), for all i,
0 ≤ i ≤ iR . And if (rR , {iR }) ∈ W and iR ≥ K then there is r0 ∈ R with
∃R ∈ r0 (i), for all i ≥ 0. As follows from (role), for each R ∈ Ω, we have either
iR ≥ K and iR− ≥ K or iR = iR− < K. So, for all i ≥ 0 and r ∈ R,
if ∃R− ∈ r(i) then there is r0 ∈ R such that ∃R ∈ r0 (i).
We construct a first-order temporal model M based on the domain D = R by
M,i
taking aM = ra , for each a ∈ ob(A), and (B ∗ ) = {r ∈ R | B ∈ r(i)}, for each
B ∈ cl(K) and i ≥ 0. It should be clear that (M, 0) |= K‡ . q
Theorem 3. If there is a quasimodel Q = hW, K, Li for K then there is an
ultimately periodical quasimodel Q0 = hW 0 , K, Li, that is, there is P ≤ |ev(K)|
such that r0 (i + P ) = r0 (i), for all i > L and (r0 , Ξ 0 ) ∈ W 0 .
Proof. We begin the proof with the following observation:
Lemma 4. Let r be a coherent and saturated run and let l ≥ 0 be such that
every r(i) is stutter-invariant, i ≥ l. Then there are i1 , . . . , i|ev(K)| ≥ l such that
ω
r0 = r≤l · r(i1 ) · . . . · r(i|ev(K)| ) is a coherent and saturated run.
Proof. First we show that
r(l) ∩ ev(K) = r(j) ∩ ev(K), for all j > l. (3)
Assume there is j > l and 3C ∈ r(l) such that 3C 6∈ r(j). As r(j) is stutter-
invariant, we have C 6∈ r(j) and, by (coh), 3C 6∈ r(j − 1). By repeating this
argument sufficiently many times, we obtain 3C 6∈ r(l), contrary to our assump-
tion. The converse direction—i.e., for each j > l, if 3C ∈ r(j) then 3C ∈ r(l)—
follows immediately from (coh).
For each 3C ∈ ev(K), we can select an i, i ≥ l, such that C ∈ r(i) whenever
3C ∈ r(l). Let i1 , . . . , i|ev(K)| be all such i. It remains to show that r0 is coherent
and saturated.
For coherency, suppose that C ∈ r0 (i), for i ≥ 0. By (coh) for r, we have
3C ∈ r0 (j), for each 0 ≤ j < i such that j ≤ l. It remains to consider j with
l < j < i. It follows that r0 (i) = r(ik ), for some 1 ≤ k ≤ |ev(K)|, from which,
by (coh) for r, 3C ∈ r(l) = r0 (l) and, by (3), 3C ∈ r0 (j).
For saturation of r0 , suppose 3C ∈ r0 (i), for i ≥ 0. If 3C ∈ r(l) then
C ∈ r(ik ) for 1 ≤ k ≤ |ev(K)| and, by the construction of r0 , there is j > i such
that r0 (j) = r(ik ). Thus C ∈ r0 (j). If 3C 6∈ r(l) then, by (3), i < l, from which
3C ∈ r(i). By (sat) of r, there is j > i with C ∈ r(j) and, by (3), j ≤ l. Thus
C ∈ r(j) = r0 (j). q
Let P = |ev(K)|. For (r, Ξ) ∈ W , take r0 = r≤L ·(r(i1 )·. . . r(iP ))ω provided by
Lemma 4. Denote the set of all such (r0 , Ξ) by W 0 . It follows that Q0 = hW 0 , K, Li
is an ultimately periodical quasimodel for K (with period P ). q
3.3 Decision Procedure for TDL-Lite3
bool
As shown in Section 3.1, there is a polynomial-time reduction of the satisfiability
problem for TDL-Lite3 3
bool KBs to the satisfiability problem for TDL-Lite0 KBs.
So it suffices to present an NP decision algorithm for the latter problem.
Our algorithm, given a TDL-Lite3 0 KB K = (T , A), guesses the ‘prefix’ of
length L + 1 and the period of length P of an ultimately periodical quasimodel
Q0 = hW 0 , K, Li for K as in Theorem 3, and then checks whether conditions
(runs), (stuttr), (obj) in Section 3.2 hold and whether the types in positions
L + 1 and L + P + 1 of the prefix coincide for every run.
More precisely, first we guess and store numbers K, L and P such that
K ≤ L, L ≤ max NK + |ev(K)| · (|role± (K)| + 2) + 3 and P ≤ |ev(K)|. Then we
guess a set Ω ⊆ role± (K) and numbers {iR < L | R ∈ Ω}. For every R ∈ Ω,
we also guess a sequence rR of length L + P + 2 of types for K and, for every
a ∈ ob(K), a sequence ra of length L + P + 2 of types for K.
Let W0 = {(rR , {iR }) | R ∈ Ω} ∪ {(ra , ∅) | a ∈ ob(K)}. The set W0 can be
regarded as a finite representation of the witnesses W 0 from Q0 . Now we check
that the following conditions hold:
1. r(K) and the r(i), for L ≤ i ≤ L + P + 1, are stutter-invariant, for each
(r, Ξ) ∈ W0 ;
2. if n B(a) ∈ A then B ∈ ra (n); if 2B(a) ∈ A then B ∈ ra (i), for all
0 < i ≤ L + P + 1;
3. for all i ≤ L + P + 1 and R ∈ role± (K), if ∃R− ∈ r(i), for some (r, Ξ) ∈ W0 ,
then (rR , {iR }) ∈ W0 , ∃R ∈ rR (iR ) and either i ≤ iR < K or K ≤ iR < L;
4. r(L + 1) = r(L + P + 1), for all (r, Ξ) ∈ W0 ;
5. r(i) is realisable, for all (r, Ξ) ∈ W0 and i ≤ L + P + 1;
6. for all (r, Ξ) ∈ W0 , i ≤ L + P + 1 and 3C ∈ r(i)
– if i ≤ L then there is j, i < j ≤ L + P + 1, with C ∈ r(j);
– if L < i ≤ L + P + 1 then there is j, L < j ≤ L + P + 1, with C ∈ r(j);
7. 3C ∈ r(j), for all (r, Ξ) ∈ W0 , i ≤ L + P + 1, C ∈ r(i) and j < i.
The algorithm returns ‘yes’ iff all the conditions above are satisfied.
The presented algorithm is sound: indeed, if conditions 1–7 are satisfied we
can construct an ultimately periodical quasimodel for K which, by Theorem 2,
means that K is satisfiable. The algorithm is also complete: if K is satisfiable
then, by Theorems 2 and 3, there exists an ultimately periodical quasimodel
Q = hW 0 , K, Li with period P and K, L, P bounded by polynomial functions
in |K| as above; then W0 consisting of the prefixes of length L + P + 2 of runs
in W 0 satisfies conditions 1–7 and thus the algorithm returns ‘yes.’
Finally, it is easy to see that L, K, P and W0 can be constructed and con-
ditions 1–7 checked by a non-deterministic polynomial-time algorithm in |K|. In
particular, condition 5 can be verified by calling, for each r with (r, Ξ) ∈ W0
N
d i ≤ L + P + 1, a DL-Litebool satisfiability checking algorithm for the concept
and
C∈r(i) C w.r.t. the TBox T , which can be done in NP [1, 2].
Then, by Lemma 1 and because TDL-Lite3 bool ‘contains’ propositional logic,
we obtain the following:
Theorem 4. The satisfiability problem for TDL-Lite3
bool KBs is NP-complete.
3.4 NP-hardness of TDL-Lite3
core
Now we show NP-hardness of satisfiability in the fragment TDL-Lite3 core of
TDL-Lite3
bool that allows only concept inclusions of the form A 1 v A 2 , A 1 v ¬A2 ,
3A1 v A2 or A1 v 3A2 , where A1 and A2 are concept names.
Lemma 5. The satisfiability problem for TDL-Lite3
core KBs is NP-hard.
Proof. We prove this by reduction of the graph 3-colourability (3-Col) problem,
which is formulated as follows: given a graph G = (V, E), decide whether there
is an assignment of colours {1, 2, 3} to vertices V such that no two vertices
ai , aj ∈ V sharing the same edge, (ai , aj ) ∈ E, have the same colour. Let Ai , for
Ai ∈ V , Xi , for 0 ≤ i ≤ 3, and V , V 0 be concept names and a an object name.
Consider the KB KG = (TG , {V (a)}), where TG consists of the following axioms:
V v 3Ai , Ai v X3 , for all Ai ∈ V,
Ai v ¬Aj , for all (Ai , Aj ) ∈ E,
V v ¬V 0 , 3X0 v V 0 ,
3X3 v X2 , 3X2 v X1 , 3X1 v X0 .
It is easy to see that KG is satisfiable iff G is 3-colourable. Indeed, if G is 3-
colourable, then we take a colouring function c : V → {1, 2, 3} and define I by
I(n)
setting ∆I = {w}, aI = w, aI ∈ Ai iff c(Ai ) = n, for all Ai ∈ V , aI ∈ V I(n)
I(n) I(n)
iff n = 0, V 0 = ∅, for all n ≥ 0, and aI ∈ Xi iff i < n. It should be clear
that I |= KG . For the converse direction, observe that if KG is satisfiable then,
I(n ) I(n )
for all Ai ∈ V , there is ni ∈ {1, 2, 3} such that aI ∈ Ai i and aI 6∈ Aj i
whenever (Ai , Aj ) ∈ E. It is readily seen that c : Ai 7→ ni , for Ai ∈ V , is a
colouring function. q
As a consequence of Lemma 5 and Theorem 4 we obtain:
Theorem 5. The satisfiability problem for TDL-Lite3
core KBs is NP-complete.
4 Conclusions
The NP complexity result for TDL-Lite3 bool is encouraging in view of possible ap-
plications of this logic for reasoning about temporal conceptual data models [4].
Indeed, on the one hand, the logic DL-LiteN bool was shown to be adequate for
representing different aspects of conceptual models: ISA, disjointness and cover-
ing for classes, domain and range of relationships, n-ary relationships, attributes
and participation constraints are all expressible in DL-LiteN bool [6]. On the other
hand, the approach of [8] shows that rigid axioms and roles with temporalised
concepts are enough to capture temporal data models.
The logic TDL-Lite3 bool presented in this paper combines a much simpler DL
DL-LiteN bool (ALCQI used in [8] is able to capture ISA between relationships)
with a more powerful temporal component and uses rigid axioms and roles with
temporalised concepts as proposed in [8]. The resulting logic can capture some
form of evolution constraints [5, 18, 15] thanks to the 3 operator, e.g., to say
that students will become alumni we use the rigid axiom Student v 3Alumni.
Furthermore, it also captures snapshot classes—i.e., classes whose instances do
not change over time, e.g., that the extension of the class of human beings re-
mains constant can be represented by Human v 2Human and 2Human v Human.
However, by restricting the temporal component only to 3 and 2 (in conjunc-
tion with rigid axioms), we lose the ability to capture temporary entities and
relationships, i.e., entities and relationships such that each of their instances has
a limited lifespan. To overcome this limitation, we are considering, as a future
work, to extend the logic presented here with either past temporal operators or
with a special kind of axioms that hold over finite prefix.
References
1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. DL-Lite in the
light of first-order logic. In Proc. of AAAI, pages 361–366, 2007.
2. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite fam-
ily and relations. Technical Report BBKCS-09-03, SCSIS, Birkbeck College, Lon-
don, 2009 (available at http://www.dcs.bbk.ac.uk/research/techreps/2009/
bbkcs-09-03.pdf).
3. A. Artale and E. Franconi. Temporal description logics. In M. Fisher, D. Gab-
bay, and L. Vila, editors, Handbook of Time and Temporal Reasoning in Artificial
Intelligence, pages 375–388. Elsevier, 2005.
4. A. Artale, E. Franconi, F. Wolter, and M. Zakharyaschev. A temporal description
logic for reasoning about conceptual schemas and queries. In S. Flesca, S. Greco,
N. Leone, and G. Ianni, editors, Proc. of JELIA-02, volume 2424 of LNAI, pages
98–110. Springer, 2002.
5. A. Artale, C. Parent, and S. Spaccapietra. Evolving objects in temporal infor-
mation systems. Annals of Mathematics and Artificial Intelligence, 50(1-2):5–38,
2007.
6. A. Artale, D. Calvanese, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev.
Reasoning over extended ER models. In Proc. of ER’07, volume 4801 of LNCS,
pages 277–292. Springer, 2007.
7. A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalis-
ing tractable description logics. In Proc. of TIME 07, pages 11–22. IEEE Computer
Society, 2007.
8. A. Artale, C. Lutz, and D. Toman. A description logic of change. In Proc. of
IJCAI-07, 2007.
9. F. Baader, R. Küsters, and F. Wolter. Extensions to description logics. In De-
scription Logic Handbook, pages 219–261. Cambridge University Press, 2003.
10. F. Baader, S. Ghilardi, and C. Lutz. LTL over description logic axioms. In Proc.
of KR 2008, 2008.
11. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. DL-Lite:
Tractable description logics for ontologies. In Proc. of AAAI 2005, pages 602–607,
2005.
12. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Data
complexity of query answering in description logics. In Proc. of KR 2006, pages
260–270, 2006.
13. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Tractable
reasoning and efficient query answering in description logics: The DL-Lite family.
J. of Automated Reasoning, 39(3):385–429, 2007.
14. D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional
Modal Logics: Theory and Applications. Elsevier, 2003.
15. G. Hall and R. Gupta. Modeling transition. In Proc. of ICDE’91, pages 540–549,
1991.
16. C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal description logics: A survey.
In Proc. of TIME 08. IEEE Computer Society Press, 2008.
17. K. Schild. Combining terminological logics with tense logic. In Proc. of EPIA’93,
October 1993.
18. S. Spaccapietra, C. Parent, and E. Zimanyi. Conceptual Modeling for Traditional
and Spatio-Temporal Applications—The MADS Approach. Springer, 2006.