We transfer results on the temporal DL-Lite family of logics, moving from infinite models of linear time to the case of finite traces. In particular, we investigate the complexity of the satisfiability problem in various fragments of TU DL-LitebNool, distinguishing the case of global axioms from the case where axioms are interpreted locally. We also consider satisfiability on traces bounded by a fixed number of time points.
Introduction
Temporal description logics based on linear temporal logic (LTL) are interpreted
over a flow of time which is generally represented by the infinite linear order of
the natural numbers [
We provide first results for the complexity of lightweight temporal description logics when interpreted over finite traces. In particular, we consider the problem of formula satisfiability (where formulas are intended to hold locally, at the first time point), and knowledge base satisfiability (in which concept inclusions hold globally, i.e., at all time points). Many of the complexity results presented in this work are obtained by adapting proofs from the infinite case to the finite traces case. However, straightforward adaptations are not always applicable. In particular, our lower bound in Theorem 8 is based on a new encoding of arithmetic progressions.
In Section 2, we introduce the syntax of a family of TDL-LiteN logics, defining their semantics on finite temporal structures. Preliminary complexity results for the formula and the knowledge base satisfiability problems over finite traces are given in Section 3. Section 4 studies reasoning over traces with a fixed bound on the number of instants, given in binary as part of the input. In Section 5 we point directions for future work.
Temporal DL-Lite
We define the language of TU DL-LitebNool as follows [
j G j G ; C ::= B j D j :C j C1 u C2;
B ::= ? j A j D ::= C j C1 U C2 qR; where L 2 NL, G 2 NG, A 2 NC, and q 2 N; q > 0, given in binary. A role R is said to be local, if it is of the form L or L , with L 2 NL, and global, if it is of the form G or G , with G 2 NG. A TU DL-LitebNool axiom is either a concept inclusion (CI) of the form C1 v C2, or an assertion, , of the form C(a) or R(a; b), where C; C1; C2 are TU DL-LitebNool concepts, R is a role, and a; b 2 NI. TU DL-LitebNool formulas have the form '; ::= j C1 v C2 j :' j ' ^ j ' U : We will use the following standard equivalences for concepts: > :?; (C1 t C2) :(:C1 u :C2); #C ? U C; #n+1C # #n C, with n 2 N (we set #0C C); 3C > U C; 2C :3:C; 3+C C t 3C; and 2+C :3+:C (similarly for formulas).
We consider also the restricted setting where formulas are limited to
conjunctions of CIs (globally interpreted, cf. e.g. [
Semantics. A TU DL-LitebNool interpretation is a structure M = ( M; (In)n2T), where T is an interval of the form [0; 1) or [0; l], with l 2 N, and each In is a classical DL interpretation with domain M (or simply ). We have that AIn M and SIn M M, for all A 2 NC and S 2 NR: in particular, for all G 2 NG and i; j 2 N, GIi = GIj (denoted simply by GI ). Moreover, aIi = aIj 2 M for all a 2 NI and i; j 2 N, i.e., constants are rigid designators (with fixed interpretation, denoted simply by aI ). The stipulation that all time points share the same domain M is called the constant domain assumption (meaning that objects are not created nor destroyed over time). The interpretation of roles and concepts at instant n is defined as follows (where S 2 NR): (S )In = f(d0; d) 2 ( qR)In = fd 2
M
M j (d; d0) 2 SIn g;
?In = ;; M j jfd0 2
M j (d; d0) 2 RIn gj qg; (:C)In =
M n CIn ; (C1 u C2)In = CIn 1 \ C2In ; (C1 U C2)In = fd 2
M j 9m 2 T; m > n : d 2 C2Im ^ 8i 2 (n; m) : d 2 C1Ii g: We say that a concept C is satisfied in M if CI0 6= ;. Satisfaction of a formula ' in M at time point n 2 T (written M; n j= ') is inductively defined as follows: M; n j= C v D iff CIn DIn ; M; n j= C(a) iff aI 2 CIn ; M; n j= R(a; b) iff (aI ; bI ) 2 RIn ;
M; n j= : M; n j= M; n j= ^ U iff not M; n j= ; iff M; n j= and M; n j= ; iff 9m 2 T; m > n : M; m j= ; and 8i 2 (n; m) : M; i j= :
(2#) (horn) (krom) (core) We say that ' is satisfied in M, writing M j= ', if M; 0 j= ', and that it is satisfiable if it is satisfied in some M. For a KB K = (T ; A), we say that K is satisfied in M if all CIs in T are satisfied in M at all time points, i.e., M j= C v D iff CIn DIn ; for all n 2 T (they are globally satisfied), and all assertions in A are satisfied in M at time point 0. K is satisfiable if it is satisfied in some M. In the following, we call finite trace an interpretation with T = [0; l], often denoted by F = ( F; (Fn)n2[0;l]), while infinite traces, based on T = [0; 1), will be denoted by I = ( I; (In)n2[0;1)). We say that a TU DL-LitebNool formula ' or KB K is satisfiable on infinite, finite, or k-bounded traces, if it is satisfied in a trace in the class of infinite, finite, or finite traces with at most k 2 N; k > 0 (given in binary) time points, respectively.
We consider the (2#)-fragment, denoted T2#DL-LitebNool, with temporal concepts of the form
D ::= C j 2C j #C Furthermore, we define TU DL-LitehNorn, TU DL-LitekNrom, and TU DL-LitecNore as the fragments of TU DL-LitebNool having, respectively, CIs of the form D1 v D2;
D1 u : : : u Dk v D
:D1 v D2; D1 v D2;
D1 u D2 v ?
D1 v :D2 and the respective (2#)-fragments where temporal concepts D are defined from concepts C of the form
C ::= B j D: We present complexity results for the finite satisfiability checking problem, distinguishing the case where formulas are allowed from the case with just knowledge bases (where axioms are interpreted globally).
finite traces
k-bounded traces bool horn ' K ' K
ExpSpace ExpSpace
Th. 2 Th. 2 PSpace PSpace
Th. 6 Th. 7 ExpSpace ExpSpace
Th. 2 Th. 2
PSpace PTShpa.c7e krom K core K
PSpace PSpace
Th. 6 ?
NP Th. 8
NExpTime
Th. 9 PSpace
Th. 12 NExpTime
Th. 10 PSpace PSpace PSpace
Th. 11
Formula satisfiability. Following [
(:C)y 7! :Cy (C u D)y 7! Cy u Dy (C U D)y 7! Cy U (Dy u :E) (C v D)y 7! Cy v Dy
(C(a))y 7! Cy(a) (R(a; b))y 7! R(a; b)
(:')y 7! :'y (' ^ )y 7! 'y ^ y (' U )y 7! 'y U ( y ^ > v :E) We obtain the reduction to the infinite traces case with the following lemma, that will be used to show the ExpSpace upper bound in Theorem 2. Lemma 1. A TU DL-LitebNool formula ' is satisfiable on finite traces iff is satisfiable on infinite traces. f ^ 'y Theorem 2. TU DL-LitebNool and T2#DL-LitehNorn formula satisfiability on finite traces is ExpSpace-complete.
Proof. The upper bound follows from the reduction in Lemma 1 to the same
problem in TU DL-LitebNool on infinite traces, which is known to be
ExpSpacecomplete [
A first-order temporal model on a finite trace (or simply a first-order finite trace) is a structure M = (D ; (In)n2T), where T is an interval of the form [0; l], with l 2 N, and each In is a classical first-order interpretation with domain D . We have P In D ar(P ), for each P 2 NP, and for all a 2 NI and i; j 2 N, aIi = aIj 2 D (denoted simply by aI ). An assignment in M is a function a from terms to D : a( ) = a(x), if = x, and a( ) = aI , if = a 2 NI Satisfaction of a formula ' in M at time point n 2 T under assignment a (written M ; n j=a ') is inductively defined as:
M ; n j=a P ( 1; : : : ; ar(P )) iff M ; n j=a :' iff M ; n j=a ' ^ iff M ; n j=a 9x' iff M ; n j=a ' U iff a( 1); : : : ; a( ar(P )) 2 P In ; not M ; n j=a '; M ; n j=a ' and M ; n j=a ; M ; n j=a0 ' for some assignment a0 that can differ from a only on x; 9m 2 T; m > n : M ; m j=a and 8i 2 (n; m) : M ; i j=a ': The standard abbreviations are used for other connectives. We say that ' is satisfied in M (and M is a model of '), writing M j= ', if M ; 0 j=a ', for some a. Moreover, ' is said to be satisfiable if it is satisfied in some M . If a formula ' contains no free variables (i.e., ' is a sentence), then we omit the assignment a in M ; n j=a ' and write M ; n j= '. If ' has a single free variable x, then we write M ; n j= '[a] in place of M ; n j=a ' with a(x) = a.
Reduction to TU QL1 formula satisfiability. Here we show how to adapt to the
finite traces case the reduction of KB satisfiability to the one-variable fragment
of first order temporal logic, given in [
A = A(x); (C1 U C2) = C1 U C2 ;
? = ?; (C1 u C2) = C1 ^ C2 ; ( q R) = EqR(x); (:C) = :C :
For a TBox T , we consider the following sentence, saying that the CIs in
T hold globally (the reflexive box 2+ plays here the role of the ‘always’ box
operator in [
T y =
^ C1vC22T
2+8x C1 (x) ! C2 (x) : Now we have to ensure that the predicates EqR(x) behave similarly to the number restrictions they replace. Denote by QT the set of numerical parameters in number restrictions of T :
QT = f 1 g [ f q j q H occurs in T g: Then, the following three properties hold in TU DL-LitebNool finite traces, for all roles R at all instants: (i) every individual with at least q0 R-successors has at least q R-successors, for q < q0; (ii) if R is a global role, then every individual with at least q R-successors at some moment has at least q R-successors at all moments of time; (iii) if the domain of a role is not empty, then its range is not empty either. These conditions can be encoded by the following TU QL1 sentences: (1) (2) (3) ^
^ R2roleK q;q02QT
q<q0 :9q002QT : q<q00<q0 ^ ^ h 2
+ 8x RR2grloolbeKal q2QT
^
R2roleK
+ 9x (9R) (x) ! 9x (9invR) (x) ;
2+8x ( q0 R) (x) ! ( q R) (x) ;
( q R) (x) ! 2( q R) (x) ^
#( q R) (x) ! ( q R) (x) i;
where invR is the inverse of R, i.e., invS = S and invS = S, for a role name S.
Since we lack the past operators, to encode the condition on global roles, in (2)
we use both the 2 and the # operators, instead of the as in [
The above reduction is extended to the ABox as in [
R(a; b) j #nR(a; b) 2 A ;
The translation Ay of the TU DL-LitebNool ABox A is now defined as follows: Ay = ^
#nA(a) ^ #nA(a)2A
^ #n:A(a) ^ ^ #n( qAR;(na) R) (a) ^ ^ ?; #n:A(a)2A #nR(a;b)2A #n:S(a;b)2SA S(a;b)2An where qAR;(na) is the number of distinct R-successors of a in A at moment n: qAR;(na) = max q 2 QT j R(a; b1); : : : ; R(a; bq) 2 AnR; for distinct b1; : : : ; bq : Finally, we define the TU QL1 translation Ky of K = (T ; A) as the conjunction of T y, Ay and formulas (1)–(3). The size of T y and Ay does not exceed the size of T and A, respectively. Thus, the size of Ky is linear in the size of K. Moreover, we have that K and Ky are equisatisfiable.
Lemma 3. On finite traces, a TU DL-LitebNool KB K is satisfiable iff the TU QL1 sentence Ky is satisfiable.
Reduction to LTL. As in [
Ky0 = 2+8x'(x) ^ ;
#R = 2+8x (9R) (x) ! 9x(9invR) (x) ; for a quantifier-free first-order temporal formula '(x) with a single variable x and unary predicates only, and a variable-free formula . In order to show that it is possible to replace #R by a formula without existential quantifiers, we require the following lemma.
Lemma 4. For every TU DL-LitebNool KB K, if there is a first-order finite trace M = (D ; (In)n2[0;l]) satisfying Ky0 such that M ; n0 j= (9R) [d], for some n0 2 [0; l] and d 2 D , then there is a first-order finite trace M 0 extending M with new elements and satisfying Ky0 such that, for each n 2 [0; l], there is dn 2 D 0 with M 0; n j= (9R) [dn].
Next, for each R 2 roleK, we take a fresh constant dR and a fresh propositional variable pR (recall that invR is also in roleK), and consider the following TU QL1
Kz = Ky0 ^
^ #0R; with
#0R = 2+8x (9R) (x) ! 2+pR ^
# pR ! pR
^ pinvR ! (9R) (dR)
(pinvR and pR indicate that invR and R are non-empty whereas dR and dinvR
witness that at 0). Notice that in #0R we again use both 2 and # operators,
instead of the used in [
Lemma 5. On finite traces, a TU DL-LitebNool KB K is satisfiable iff the TU QL sentence Kz is satisfiable.
Theorem 6. TU DL-LitebNool and TU DL-LitecNore KB satisfiability on finite traces is PSpace-complete.
Proof. The PSpace-hardness for TU DL-LitecNore is obtained by observing that
the PSpace-hardness proof in [2, Theorem 4.5] works also in the case of finite
traces. For PSpace-membership, we have that Kz can be considered as a LTL
formula (as it does not contain existential quantifiers, and because all the
universally quantified variables can be instantiated by all the constants in the formula,
which only results in a polynomial blow-up). Moreover, the translation z can be
done in logarithmic space in the size of K [
Similar complexity results can be obtained restricting the temporal operators to just 2 and # combined with the horn fragment.
Theorem 7. The T2#DL-LitebNool and T2#DL-LitehNorn KB satisfiability on finite traces is PSpace-complete.
Proof. The upper bound follows from Theorem 6. The lower bound can be obtained from the PSpace result in [2, Theorem 4.5] noting that the only axiom requiring the U operator has the form Sia v Sia U Di which can be replaced by the horn axiom Hiq u Sja v #Sja, for i 6= j. The proof then proceeds similarly to Theorem 6.
When we further reduce to the core fragment we can obtain the following hardness result. The proof is by reduction of 3SAT as in [2, Theorem 5.4], however, we cannot directly adapt such proof as it relies on an encoding of arithmetic progressions. In this encoding, each time point may represent an assignment satisfying a propositional formula in 3CNF. A symbol d is used to mark time points which do not represent a satisfying assignment. The 3CNF formula is satisfiable iff d does not hold at some time point. On finite traces, we cannot explictly encode all (infinitely many) values of the arithmetic progressions. We solve this by encoding a finite portion of the arithmetic progressions backwards. Essentially, we mark the last time point using a concept expression of the form 2?, which is only true at the last time point. Then, we check whether there is an arbitrarily large but finite trace where d does not hold at time point zero. 1 tu tu Theorem 8. T2#DL-LitecNore (and T2#DL-LitekNrom) KB satisfiability on finite traces is NP-hard.
Proof. The proof is by reduction of 3SAT. Let f = Vin=1 Ci be a 3CNF with m variables p1; : : : ; pm and n clauses C1; : : : ; Cn. By a propositional assignment for f we understand a function : fp1; : : : ; pmg ! f0; 1g. We will represent such assignments by sets of positive natural numbers. More precisely, let P1; : : : ; Pm be the first m prime numbers; it is known that Pm does not exceed O(m2). We say that a natural number k represents an assignment if k modulo Pi is equivalent to (pi), for all i, 1 i m.
Not every natural number represents an assignment. Consider the following
arithmetic progressions:
j + Pi N;
for 1
i
m and 2
j < Pi:
Every element of j + Pi N is equivalent to j modulo Pi, and so, since j 2,
cannot represent an assignment. Moreover, every natural number that cannot
represent an assignment belongs to one of these arithmetic progressions (see Fig.
1 from [
Let Ci be a clause in f , for example, Ci = pi1 _ :pi2 _ pi3 . Consider the following progression:
Pi01 Pi12 Pi03 + Pi1 Pi2 Pi3 N: (4) (5) where by Pi01 Pi12 Pi03 we denote the least natural number, say P , such that P modulo Pi1 is equivalent to 0, P modulo Pi2 is equivalent to 1, and P modulo Pi3 is equivalent to 0. Then a natural number represents an assignment making Ci true iff it does not belong to the progressions (4) and (5). Thus, a natural number represents a satisfying assignment for f iff it does not belong to any of the progressions of the form (4) and (5), for clauses in f .
We now show how to encode arithmetic progressions as T2#DL-LitecNore KBs. We use a concept name D signalling a truth assignment for f whenever D does not hold. To take advantage of the finite traces for KBs in T2#DL-LitecNore we encode arithmetic progressions starting from the last point of the finite trace and then going backwards, halting whenever D becomes false. To express that D cannot be true in all instants we use the following axioms, with the concept 2? being true just at the last point of the finite trace and F a newly introduced concept name: 2? v D;
D u F v ? together with the ABox assertion F (a). Each of the arithmetic progressions (4) and (5) have the form a + bN (with a > 0 and b > 1) and can be encoded with the following axioms: 2? v U0; Ua v V0; Vb v V0; # Uj 1 v Uj ; for j = 1; : : : ; a; # Vj 1 v Vj ; for j = 1; : : : ; b; where U0; : : : ; Ua and V0; : : : ; Vb are fresh atomic concepts. Note that the size of the resulting T2#DL-LitecNore KB is O(n m6). One can check that the above KB is satisfiable on finite traces iff f is satisfiable.
The NP upper bound presented in [2, Theorem 4.7], using a translation to the krom fragment of LTL on infinite traces, cannot be immediately applied in the finite case, since the complexity of this fragment on finite traces is unknown. 4
Satisfiability on Bounded Traces In this section we consider satisfiability of TU DL-LiteN formulas and KBs on traces with at most k time points, with k given in binary. We start by considering the formula satisfiability problem. We establish that the complexity of the satisfiability problem for TU DL-LitebNool (and consequently for TU DL-LitehNorn) is in NExpTime for traces bounded by k (in binary, given as part of the input). We formalise this result with the following theorem.
Theorem 9. TU DL-LitebNool formula satisfiability on k-bounded traces is in NExpTime.
Proof. (Sketch) Our result follows from the fact that one can translate any
TU DL-LitebNool formula into an equisatisfiable TU QL1 formula [
Theorem 10. TU DL-LitehNorn formula satisfiability on k-bounded traces is NExpTime-hard.
Proof. (Sketch) Suppose we are given a finite set T of tile types, a t0 2 T and a
natural number k in binary. We can assume w.l.o.g. that k = 2n. The problem
is to decide whether T tiles the grid 2n 2n in such a way that t0 is placed at
(0; 0). We construct essentially the same TU DL-LitehNorn formula 'T;t0;n as in
Theorem 10 in [
Theorem 11. TU DL-LitecNore KB satisfiability on k-bounded traces is PSpacehard.
The upper bound for TU DL-LitebNool (and consequently for its fragments) is obtained in the same way as for TU DL-LitebNool (Theorems 6 and 7), with a translation to LTL. The important point here is that the procedure is adapted to ensure that the number of time points is bounded by k. The exact number of time points t k can be guessed and stored in binary using polynomial space w.r.t. the size of k (as a string). Then the procedure is as for LTL, with the difference that when we reach t we have to check whether all the ‘until’s have been realised, that is, whether the finite trace can finish at this time point. Theorem 12. TU DL-LitebNool KB satisfiability on k-bounded traces is in PSpace. 5
Conclusion We presented preliminary results on the complexity of reasoning in the TDL-LiteN family of languages interpreted on finite traces. Our results show that in terms of complexity, there is not much change between reasoning on finite and infinite traces (except when there is a bound on the time points). However, on the semantical side, there are several expressions that, on finite traces, become satisfiable (2?) and unsatisfiable (2+ # >).
We plan to investigate syntactical and semantical ways of characterising the distinction between reasoning on finite and infinite traces. Also, we plan to improve the landscape of complexity results, in particular, to study satisfiability on finite traces in sub-boolean fragments of TU DL-LitebNool, such as the krom and core fragments.