=Paper=
{{Paper
|id=Vol-2373/paper-2
|storemode=property
|title=Temporal DL-Lite over Finite Traces (Preliminary Results)
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-2.pdf
|volume=Vol-2373
|authors=Alessandro Artale,Andrea Mazzullo,Ana Ozaki
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleMO19
}}
==Temporal DL-Lite over Finite Traces (Preliminary Results)==
<pdf width="1500px">https://ceur-ws.org/Vol-2373/paper-2.pdf</pdf>
<pre>
           Temporal DL-Lite over Finite Traces
                 (Preliminary Results)

              Alessandro Artale, Andrea Mazzullo, and Ana Ozaki

          KRDB Research Centre, Free University of Bozen-Bolzano, Italy
                           surname@inf.unibz.it




      Abstract. 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-LiteN bool , distinguishing the case of global ax-
      ioms from the case where axioms are interpreted locally. We also consider
      satisfiability on traces bounded by a fixed number of time points.



1   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 [9, 10, 5]. A renewed interest in LTL interpreted over finite
traces, i.e., over structures based on finite initial segments of the natural num-
bers [7], has recently motivated the study of temporal formalisms for knowledge
representation interpreted on a finite, or even bounded, temporal dimension [3,
4]. Logics in the temporal DL-Lite family, suitable for temporal conceptual data
modelling, have only been investigated over infinite temporal structures [1, 2].
    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, defin-
ing 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.
2    Temporal DL-Lite

We define the language of TU DL-LiteN   bool as follows [1, 2]. Let NC , NI be count-
able sets of concept and individual names, respectively, and let NL and NG be
countable and disjoint sets of local and global role names, respectively. The union
NL ∪ NG is the set NR of role names. TU DL-LiteN     bool roles R, basic concepts B,
concepts C, and temporal concepts D are given by the following grammar:

           R ::= L | L− | G | G− ,                   B ::= ⊥ | A | ≥ qR,
           C ::= B | D | ¬C | C1 u C2 ,              D ::= C | C1 U C2

where L ∈ NL , G ∈ NG , A ∈ NC , and q ∈ 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 ∈ NL , and global, if it is
of the form G or G− , with G ∈ NG . A TU DL-LiteN     bool 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-LiteN  bool concepts, R is a role, and a, b ∈ NI .
TU DL-LiteN bool formulas have the form


                    ϕ, ψ ::= α | C1 v C2 | ¬ϕ | ϕ ∧ ψ | ϕ U ψ.

We will use the following standard equivalences for concepts: > ≡ ¬⊥; (C1 t
C2 ) ≡ ¬(¬C1 u ¬C2 ); #C ≡ ⊥ U C; #n+1 C ≡ # #n C, with n ∈ N (we set
#0 C ≡ 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 con-
junctions of CIs (globally interpreted, cf. e.g. [2]) and assertions. In this case, a
TfU DL-LiteN                                        f        N
            bool TBox T is a finite set of CIs. A TU DL-Litebool ABox A is a finite
set of assertions of the of the form

                 #n A(a),    #n ¬A(a),    #n S(a, b),   #n ¬S(a, b)

where A ∈ NC , S ∈ NR , and a, b ∈ NI . A TfU DL-LiteN
                                                     bool knowledge base (KB) K
is a pair (T , A).


Semantics. A TU DL-LiteN                                             M
                           bool interpretation is a structure M = (∆ , (In )n∈T ),
where T is an interval of the form [0, ∞) or [0, l], with l ∈ N, and each In is
a classical DL interpretation with domain ∆M (or simply ∆). We have that
AIn ⊆ ∆M and S In ⊆ ∆M × ∆M , for all A ∈ NC and S ∈ NR : in particular, for
all G ∈ NG and i, j ∈ N, GIi = GIj (denoted simply by GI ). Moreover, aIi =
aIj ∈ ∆M for all a ∈ NI and i, j ∈ 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 ∈ NR ):
           (S − )In = {(d0 , d) ∈ ∆M × ∆M | (d, d0 ) ∈ S In },       ⊥In = ∅,
              (≥ qR)In = {d ∈ ∆M | |{d0 ∈ ∆M | (d, d0 ) ∈ RIn }| ≥ q},
                (¬C)In = ∆M \ C In ,          (C1 u C2 )In = C1In ∩ C2In ,
    (C1 U C2 )In = {d ∈ ∆M | ∃m ∈ T, m > n : d ∈ C2Im ∧ ∀i ∈ (n, m) : d ∈ C1Ii }.
We say that a concept C is satisfied in M if C I0 6= ∅. Satisfaction of a formula
ϕ in M at time point n ∈ T (written M, n |= ϕ) is inductively defined as follows:
M, n |= C v D iff C In ⊆ DIn ,             M, n |= ¬ψ    iff not M, n |= φ,
M, n |= C(a) iff aI ∈ C In ,               M, n |= ψ ∧ χ iff M, n |= ψ and M, n |= χ,
M, n |= R(a, b) iff (aI , bI ) ∈ RIn ,     M, n |= ψ U χ iff ∃m ∈ T, m > n : M, m |= χ,
                                                         and ∀i ∈ (n, m) : M, i |= ψ.
We say that ϕ is satisfied in M, writing M |= ϕ, if M, 0 |= ϕ, 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 |= C v D iff C In ⊆ DIn , for all n ∈ 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 )n∈[0,l] ), while infinite traces, based on T = [0, ∞),
will be denoted by I = (∆I , (In )n∈[0,∞) ). We say that a TU DL-LiteN      bool 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 ∈ N, k > 0
(given in binary) time points, respectively.
    We consider the (2#)-fragment, denoted T2# DL-LiteN       bool , with temporal con-
cepts of the form
                                  D ::= C | 2C | #C                               (2#)
Furthermore, we define TU DL-LiteN                  N                    N
                                   horn , TU DL-Litekrom , and TU DL-Litecore as
                           N
the fragments of TU DL-Litebool having, respectively, CIs of the form
                                  D1 u . . . u Dk v D                           (horn)
                     D1 v D2 ,           ¬D1 v D2 ,     D1 v ¬D2                (krom)
                             D1 v D2 ,        D 1 u D2 v ⊥                       (core)
and the respective (2#)-fragments where temporal concepts D are defined from
concepts C of the form
                                C ::= B | D.
Table 1 summarises the logics studied, and the corresponding complexity results.

3     Satisfiability on Finite Traces
We present complexity results for the finite satisfiability checking problem, dis-
tinguishing the case where formulas are allowed from the case with just knowl-
edge bases (where axioms are interpreted globally).
                                  finite traces       k-bounded traces
                                      N             N
                           TU DL-Lite T2# DL-Lite       TU DL-LiteN
                           ExpSpace        ExpSpace      NExpTime
                       ϕ
                              Th. 2           Th. 2        Th. 9
                bool
                            PSpace          PSpace        PSpace
                       K
                              Th. 6           Th. 7       ≤ Th. 12
                           ExpSpace        ExpSpace      NExpTime
                       ϕ
                              Th. 2           Th. 2        Th. 10
               horn
                                            PSpace
                       K    PSpace                        PSpace
                                              Th. 7
               krom K       PSpace            ?           PSpace
                            PSpace         ≥ NP           PSpace
               core K
                             Th. 6         Th. 8          ≥ Th. 11

Table 1. Complexity results for TDL-LiteN fragments on finite and bounded traces.



Formula satisfiability. Following [3], we define the end of time formula ψf
as the conjunction of the following T# DL-LiteN
                                              krom formulas (i.e., with temporal
concepts of the form D ::= C | #D):
     ψf1 = > v ¬E,         ψf2 = (> v ¬E) U (> v E),       ψf3 = 2+ (E v #E),
where E is a fresh concept name representing the end of time. The translation
·† from TU DL-LiteN                                         N
                    bool concepts and formulas to TU DL-Litebool concepts and
formulas, respectively, is defined as follows:
         (⊥)† 7→ ⊥                           (C v D)† 7→ C † v D†
         (A)† 7→ A                             (C(a))† 7→ C † (a)
      (≥ qR)† 7→ ≥ qR                        (R(a, b))† 7→ R(a, b)
        (¬C)† 7→ ¬C †                            (¬ϕ)† 7→ ¬ϕ†
     (C u D)† 7→ C † u D†                     (ϕ ∧ ψ)† 7→ ϕ† ∧ ψ †
     (C U D)† 7→ C † U (D† u ¬E)              (ϕ U ψ)† 7→ ϕ† U (ψ † ∧ > 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-LiteN       bool formula ϕ is satisfiable on finite traces iff ψf ∧ ϕ
                                                                                      †

is satisfiable on infinite traces.
Theorem 2. TU DL-LiteN                     N
                       bool and T2# DL-Litehorn 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-LiteN bool on infinite traces, which is known to be ExpSpace-
complete [1]. The lower bound is obtained by a reduction of the m × 2n corridor
tiling problem to satisfiability on finite traces of formulas in T2# DL-LiteN
                                                                            horn
(similar to [1, Theorem 10], modified for the finite traces case).             t
                                                                               u
Knowledge base satisfiability. In this section, TU DL-LiteN       bool KB satisfiability
on finite traces is reduced to LTL formula satisfiability on finite traces, which is
known to be PSpace-complete [7]. The proof is an adaptation of the reduction
of TU DL-LiteN  bool to LTL on infinite traces [2], and it proceeds in two steps.
First, the TU DL-LiteN  bool KB satisfiability problem is reduced to the formula
satisfiability problem in the one-variable fragment of first-order temporal logic on
finite traces, TU QL1 [8]. Then, the satisfiability of the resulting TU QL1 formulas
is reduced to satisfiability on finite traces of TU QL1 formulas without positive
occurrences of existential quantifiers, which are essentially LTL formulas.

First-order temporal logic on finite traces. The alphabet of TU QL consists of
countably infinite and pairwise disjoint sets of predicates NP (with ar(P ) ∈ N
being the arity of P ∈ NP ), constants (or individual names) NI , and variables
Var; the logical operators ¬, ∧; the existential quantifier ∃, and the temporal
operator U (until ). Formulas of TU QL have the form:

                         ϕ, ψ ::= P (τ̄ ) | ¬ϕ | ϕ ∧ ψ | ∃xϕ | ϕ U ψ,

where P ∈ NP , τ̄ = (τ1 , . . . , τar(P ) ) is a tuple of terms, i.e., constants or variables,
and x ∈ Var. We write ϕ(x1 , . . . , xm ) to indicate that the free variables of a
formula ϕ are in {x1 , . . . , xm }. For p ∈ N, the p-variable fragment of TU QL,
denoted by TU QLp , consists of TU QL formulas with at most p variables (TU QL0
is simply propositional LTL).
    A first-order temporal model on a finite trace (or simply a first-order finite
trace) is a structure M = (D, (In )n∈T ), where T is an interval of the form [0, l],
with l ∈ N, and each In is a classical first-order interpretation with domain
D. We have P In ⊆ D ar(P ) , for each P ∈ NP , and for all a ∈ NI and i, j ∈ N,
aIi = aIj ∈ 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 ∈ NI
Satisfaction of a formula ϕ in M at time point n ∈ T under assignment a
(written M , n |=a ϕ) is inductively defined as:

      M , n |=a P (τ1 , . . . , τar(P ) )   iff   a(τ1 ), . . . , a(τar(P ) ) ∈ P In ,
      M , n |=a ¬ϕ                          iff   not M , n |=a ϕ,
      M , n |=a ϕ ∧ ψ                       iff   M , n |=a ϕ and M , n |=a ψ,
                                                                0
      M , n |=a ∃xϕ                         iff   M , n |=a ϕ for some assignment a0
                                                  that can differ from a only on x,
      M , n |=a ϕ U ψ                       iff   ∃m ∈ T, m > n : M , m |=a ψ and
                                                  ∀i ∈ (n, m) : M , i |=a ϕ.

The standard abbreviations are used for other connectives. We say that ϕ is
satisfied in M (and M is a model of ϕ), writing M |= ϕ, if M , 0 |=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 |=a ϕ and write M , n |= ϕ. If ϕ has a single free variable x, then we
write M , n |= ϕ[a] in place of M , n |=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 [2]. For a TU DL-LiteNbool KB K = (T , A),
let indA be the set of all individual names occurring in A, and roleK the set of
global and local role names occurring in K and their inverses. In this reduction,
individual names a ∈ indA are mapped to constants a, concept names A to unary
predicates A(x), and number restrictions ≥ q R to unary predicates Eq R(x).
Recall that, for S ∈ NR , the predicates Eq S(x) and Eq S − (x) represent, at each
moment of time, the sets of elements with at least q distinct S-successors and
at least q distinct S-predecessors (in particular, E1 S(x) and E1 S − (x) represent
the domain and the range of S, respectively). By induction on the construction
of a TU DL-LiteN                                       1
                 bool concept C, we define the TU QL formula C (x):
                                                                   ∗


             A∗ = A(x),                          ⊥∗ = ⊥,              (≥ q R)∗ = Eq R(x),
              ∗
   (C1 U C2 )     = C1∗ U C2∗ ,      (C1 u C2 )   ∗
                                                      = C1∗ ∧ C2∗ ,     (¬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 [2], since we consider traces based on initial segments of the natural
numbers):                      ^
                      T†=             2+ ∀x C1∗ (x) → C2∗ (x) .
                                                              


                                C1 vC2 ∈T

Now we have to ensure that the predicates Eq R(x) behave similarly to the num-
ber restrictions they replace. Denote by QT the set of numerical parameters in
number restrictions of T :
                      QT = { 1 } ∪ { q | ≥ q H occurs in T }.
Then, the following three properties hold in TU DL-LiteN      bool finite traces, for all
roles R at all instants: (i) every individual with at least q 0 R-successors has at
least q R-successors, for q < q 0 ; (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:
                ^         ^
                                 2+ ∀x (≥ q 0 R)∗ (x) → (≥ q R)∗ (x) ,
                                                                         

                                                                                     (1)
              R∈roleK      q,q 0 ∈QT
                             q<q 0
                   ¬∃q 00 ∈QT : q<q 00 <q 0
                  ^      ^               h
                               2+ ∀x          (≥ q R)∗ (x) → 2(≥ q R)∗ (x) ∧
                                                                          


              R∈roleK q∈QT
              R global                                                                      (2)
                                                        ∗
                                                               
i       ∗
                                     #(≥ q R) (x) → (≥ q R) (x) ,
                  ^
                        2+ ∃x (∃R)∗ (x) → ∃x (∃invR)∗ (x) ,
                                                         

                                                                                            (3)
              R∈roleK
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 [2].
   The above reduction is extended to the ABox as in [2]. In particular, we
assume that A contains #n S − (b, a) whenever it contains #n S(a, b). For each
n ∈ [0, l] and each role R, the temporal slice AR n of A is defined by taking
            (
   R           R(a, b) | #m R(a, b) ∈ A for some m ∈ [0, l] , R is a global role,
 An =        
               R(a, b) | #n R(a, b) ∈ A ,                       R is a local role.

The translation A† of the TU DL-LiteN
                                    bool ABox A is now defined as follows:
         ^               ^                ^         R,n
                                                                     ^
  A† =      #n A(a) ∧       #n ¬A(a) ∧       #n (≥ qA(a) R)∗ (a) ∧       ⊥,
       #n A(a)∈A        #n ¬A(a)∈A           #n R(a,b)∈A                    #n ¬S(a,b)∈A
                                                                             S(a,b)∈ASn

        R,n
where qA(a) is the number of distinct R-successors of a in A at moment n:
   R,n
        = max q ∈ QT | R(a, b1 ), . . . , R(a, bq ) ∈ AR
               
  qA(a)                                                n , for distinct b1 , . . . , bq .


    Finally, we define the TU QL1 translation K† of K = (T , A) as the conjunction
of T † , A† and formulas (1)–(3). The size of T † and A† does not exceed the size
of T and A, respectively. Thus, the size of K† is linear in the size of K. Moreover,
we have that K and K† are equisatisfiable.
Lemma 3. On finite traces, a TU DL-LiteN
                                       bool KB K is satisfiable iff the TU QL
                                                                              1
          †
sentence K is satisfiable.

Reduction to LTL. As in [2], our next aim is to construct an LTL formula
that is equisatisfiable, on finiteVtraces, with K† . First, we have that K† can be
represented in the form K†0 ∧ R∈roleK ϑR , where

      K†0 = 2+ ∀xϕ(x) ∧ ψ,           ϑR = 2+ ∀x (∃R)∗ (x) → ∃x(∃invR)∗ (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-LiteN        bool KB K, if there is a first-order finite trace
M = (D, (In )n∈[0,l] ) satisfying K†0 such that M , n0 |= (∃R)∗ [d], for some
n0 ∈ [0, l] and d ∈ D, then there is a first-order finite trace M 0 extending M
with new elements and satisfying K†0 such that, for each n ∈ [0, l], there is
dn ∈ D 0 with M 0 , n |= (∃R)∗ [dn ].
   Next, for each R ∈ 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
formula:
                                           ^
                            K ‡ = K †0 ∧       ϑ0R , with
                                       R∈roleK

   ϑ0R = 2+ ∀x (∃R)∗ (x) → 2+ pR ∧ # pR → pR ∧ pinvR → (∃R)∗ (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 [2].
Lemma 5. On finite traces, a TU DL-LiteN
                                       bool KB K is satisfiable iff the TU QL
                                                                              1
          ‡
sentence K is satisfiable.
We can thus state the following result.
Theorem 6. TU DL-LiteN                  N
                     bool and TU DL-Litecore KB satisfiability on finite traces
is PSpace-complete.
Proof. The PSpace-hardness for TU DL-LiteN      core 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 K‡ can be considered as a LTL
formula (as it does not contain existential quantifiers, and because all the univer-
sally quantified variables can be instantiated by all the constants in the formula,
which only results in a polynomial blow-up). Moreover, the translation ·‡ can be
done in logarithmic space in the size of K [2]. Thus, from Lemma 5 and PSpace-
membership of LTL on finite traces [7], we get the matching upper bounds. t       u
    Similar complexity results can be obtained restricting the temporal operators
to just 2 and # combined with the horn fragment.
Theorem 7. The T2# DL-LiteN                       N
                              bool and T2# DL-Litehorn KB satisfiability on fi-
nite traces is PSpace-complete.
Proof. The upper bound follows from Theorem 6. The lower bound can be ob-
tained 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.                                                                t
                                                                             u
     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], how-
ever, 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 sat-
isfying 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 en-
code 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.
Theorem 8. T2# DL-LiteN                                    N
                               core (and T2# DL-Litekrom ) KB satisfiability on finite
traces is NP-hard.
                                                                Vn
Proof. The proof is by reduction of 3SAT. Let f = i=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 σ : {p1 , . . . , pm } → {0, 1}. 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 .                   (4)

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 [2]).
    Let Ci be a clause in f , for example, Ci = pi1 ∨ ¬pi2 ∨ pi3 . Consider the
following progression:
                          Pi01 Pi12 Pi03 + Pi1 Pi2 Pi3 · N.                   (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-LiteN    core 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-LiteN   core 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,      DuF 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 ,       # Uj−1 v Uj , for j = 1, . . . , a,
                    Ua v V0 ,      # Vj−1 v Vj , for j = 1, . . . , b,
                    Vb v V0 ,      V0 v D,
where U0 , . . . , Ua and V0 , . . . , Vb are fresh atomic concepts. Note that the size of
the resulting T2# DL-LiteN                             6
                                core KB is O(n · m ). 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 consider-
ing the formula satisfiability problem. We establish that the complexity of the
satisfiability problem for TU DL-LiteN                                     N
                                      bool (and consequently for TU DL-Litehorn )
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-LiteN
                     bool formula satisfiability on k-bounded traces is in
NExpTime.

Proof. (Sketch) Our result follows from the fact that one can translate any
TU DL-LiteN                                                1
            bool formula into an equisatisfiable TU QL formula [1]. Satisfiabil-
                1
ity of a TU QL formula can be solved using quasimodels [8, Theorem 11.30], a
classical technique used to abstract models. For finite traces, the same notions
can be adopted. In particular, one can show that there is a model for a TU QL1
formula with k time points if and only if there is a quasimodel for it where the
sequence of quasistates has lengh k [3]. If the number of time points is bouned by
k (in binary), then satisfiability of this translation can be decided in NExpTime
by guessing an exponential size sequence of sets of types and then checking in
exponential time that it forms a quasimodel.                                     t
                                                                                 u

The next theorem establishes a matching lower bound for TU DL-LiteN
                                                                  horn (and
consequently for TU DL-LiteN
                           bool ) on k-bounded traces.
Theorem 10. TU DL-LiteN
                      horn formula satisfiability on k-bounded traces is
NExpTime-hard.

Proof. (Sketch) Suppose we are given a finite set T of tile types, a t0 ∈ 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-LiteN  horn formula ϕT,t0 ,n as in
Theorem 10 in [1]. An exponential counter can be used to mark with a concept
name M the 2n −1 time points of the trace with 2n time points. One can then use
M on the left side of inclusions to ensure that the # operator on the right side is
only ‘applied’ when there is a next time point. We exclude axioms used to encode
that the top and bottom sides of the corridor are white, which are not needed for
the bounded tiling problem. The main difference is that in the mentioned proof,
the formula on infinite traces is used to prove ExpSpace-hardness by reduction
from the corridor problem. Here, the number of time points is bounded by k, and
so, we can only encode the bounded tiling problem, which gives us NExpTime-
hardness [6].                                                                 t
                                                                              u

We now consider the KB satisfiability problem. The same PSpace-hardness
proof for TU DL-LiteN                                 N
                     core can applied for TU DL-Litecore (see Theorems 6 and
7). The main point here is to show that the bound on the number of time
points does not affect this hardness proof. Indeed, the proof is by reduction
from a polynomial space bounded Turing machine, where each configuration
can be encoded in a time point. One can assume w.l.o.g. that the length of a
computation is exponential in the size of the input (by removing repetitions in
a sequence of configurations). Since k is given in binary, if the length of k is
polynomial in the size of the KB given as input, then traces may still have an
exponential number of time points (w.r.t the size of the formula). So, the same
encoding of the problem holds in this setting.

Theorem 11. TU DL-LiteN
                      core KB satisfiability on k-bounded traces is PSpace-
hard.

    The upper bound for TU DL-LiteN   bool (and consequently for its fragments) is
obtained in the same way as for TU DL-LiteN     bool (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-LiteN
                      bool 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 in-
finite 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 im-
prove the landscape of complexity results, in particular, to study satisfiability on
finite traces in sub-boolean fragments of TU DL-LiteN bool , such as the krom and
core fragments.
References
 1. Artale, A., Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporalising
    tractable description logics. In: TIME. pp. 11–22 (2007)
 2. Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: A cookbook for
    temporal conceptual data modelling with description logics. ACM Trans. Comput.
    Log. 15(3), 25:1–25:50 (2014)
 3. Artale, A., Mazzullo, A., Ozaki, A.: Temporal description logics over finite traces.
    In: DL. vol. 2211 (2018)
 4. Artale, A., Mazzullo, A., Ozaki, A.: Do you need infinite time? In: IJCAI (to
    appear) (2019)
 5. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM Trans.
    Comput. Log. 13(3) (2012)
 6. Boas, P.V.E.: The convenience of tilings. In: In Complexity, Logic, and Recursion
    Theory. pp. 331–363. Marcel Dekker Inc (1997)
 7. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on
    finite traces. In: IJCAI. pp. 854–860 (2013)
 8. Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional
    Modal Logics: Theory and Applications. Elsevier (2003)
 9. Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order
    temporal logics. Annals of Pure and Applied Logic 106(1-3), 85–134 (2000)
10. Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey.
    In: TIME. pp. 3–14 (2008)

</pre>