Happy Ever After: Temporally Attributed Description Logics Ana Ozaki a , Markus Krötzsch b , Sebastian Rudolph c a KRDB Research Centre, Free University of Bozen-Bolzano, Italy b Center for Advancing Electronics Dresden (cfaed), TU Dresden, Germany c Computational Logic Group, TU Dresden, Germany Abstract. Knowledge graphs are based on graph models enriched with (sets of) attribute-value pairs, called annotations, attached to vertices and edges. Many application scenarios of knowledge graphs crucially rely on the frequent use of annotations related to time. Based on recently proposed attributed logics, we design description logics enriched with temporal annotations whose values are interpreted over discrete time. Investigating the complexity of reasoning in this new formalism, it turns out that reasoning in our temporally attributed description logic ALCHT@ is highly undecidable; thus we establish restrictions where it becomes decidable, and even tractable. 1 Introduction Graph-based data formats play an essential role in modern information management, since they offer schematic flexibility, ease information re-use, and simplify data integration. Ontological knowledge representation has been shown to offer many benefits to such data-intensive applications, e.g., by supporting integration, querying, error detection, or repair. However, practical knowledge graphs, such as Wikidata [24] or YAGO2 [13], are based on enriched graphs where edges are augmented with additional annotations. To model these enriched graphs, attributed logics have been proposed as a way of integrating annotations with logical reasoning [20,14,15]. Other formalisms for reasoning over annotated relations have been studied in the context of data modelling [6]. Annotations in practical knowledge graphs have many purposes, such as recording provenance, specifying context, or encoding n-ary relations. One of their most important uses, however, is to encode temporal validity of statements. In Wikidata, e.g., start/end time and point in time are among the most frequent annotations, used in 5.4 million statements overall.1 In YAGO2, time and space are the main types of annotations considered. Reasoning with time clearly requires an adequate semantics, and many approaches were proposed. Validity time points and intervals are a classical topic in data management [9,10], and similar models of time have also been studied in ontologies [2,16]. However, researchers in ontologies have most commonly focussed on abstract models of time as 1 As of October 2018, the only more common annotations are reference (provenance) and de- termination method (context); see https://tools.wmflabs.org/sqid/#/browse?type= properties&sortpropertyqualifiers=fa-sort-desc used in temporal logics [19,25,5]. Temporal reasoning in ALC with concrete domains was proposed by Lutz et. al [18]. It is known that satisfiability of ALC with a concrete domain consisting of a dense domain and containing the predicates = and < is ExpTime- complete [17]. In the same setting but for discrete time, the complexity of the satisfiability problem is open, a criterion which only guarantees decidability has been proposed by Carapelle and Turhan [7]. None of these approaches has been considered for attributed logics yet, and indeed support for temporal reasoning for knowledge graphs, such as Wikidata and YAGO2, is still missing today. In this paper, we address this shortcoming by endowing attributed description logics with a temporal semantics for annotations. Indeed, annotations are already well-suited for representing time-related data. Example 1. The fact that Johannes Gutenberg died in Mainz in 1468 could be encoded in attributed DLs as: diedIn(Gutenberg, Mainz)@[ time : 1468] Not all annotations are temporal, and we can also annotate concept assertions, e.g., to state that he lived in Strasbourg: Lived(Gutenberg)@[ loc : Strasbourg] Gutenberg’s early life is less certain, and we only know that he was born between 1394 and 1404 in Mainz. Such uncertainty about precise dates is very common in practice. Nevertheless, we would like to record the information available, which could be expressed as follows: bornIn(Gutenberg, Mainz)@[ between : [1394, 1404]] To deal with such temporally annotated data in a semantically adequate way and to specify temporal background knowledge, we propose the temporally attributed description logic ALCHT@ , enabling reasoning and querying support for such information. Beyond defining syntax and semantics of ALCHT@ , this paper’s contributions are the following: – We show that the full formalism is highly undecidable using an encoding of a recurring tiling problem. – We present three ways (of increasing reasoning complexity) for regaining decidability: disallowing variables altogether (ExpTime), disallowing the use of variables only for temporal attributes (2ExpTime), or disallowing the use of temporal attributes referencing time points in the future (3ExpTime). – Finally we single out a lightweight case based on the description logic EL which features PTime reasoning. The paper is self-contained. Details on some long proofs can be found in the appendix of the extended online version [21]. 2 Temporally Attributed DLs We first present the syntax and underlying intuition of temporally attributed description logics. In DL, a true fact corresponds to the membership of an element in a class, or of a pair of elements in a binary relation. Attributed DLs further allow each true fact to carry a finite set of annotations [14] , given as attribute-value pairs. As suggested in Example 1, the same relationship may be true with several different annotation sets, e.g., in case Gutenberg also lived elsewhere. We define our description logic ALCHT@ as a multi-sorted version of the attributed DL ALCH@ , thereby introducing datatypes for time points and intervals. Elements of the different types are represented by members of mutually disjoint sets of (abstract) individual names NI , time points NT , and time intervals N2T . We represent time points by natural numbers, and assume that elements of NT (N2T ) are (pairs of) numbers in binary encoding. We write [k, `] for a pair of numbers k, ` in N2T . Moreover, we require that there are the following seven special individual names, called temporal attributes: time, before, after, until, since, during, between ∈ NI . The intuitive meaning of temporal attributes is as one might expect: time describes individual times at which a statement is true, while the others describe (half-open) intervals. The meaning of before, after, and between is existential in that they require the statement to hold only at some time in the interval, while until, since, and during are universal and require something to be true throughout an interval. Axioms of ALCHT@ are further based on sets of concept names NC , role names NR , and (set) variables NV . Attributes are represented by individual names, and we associate a value type vt(a) with each individual a ∈ NI for this purpose: during and between have value type N2T , all other temporal attributes have value type NT , and all other individuals have value type NI . An attribute-value pair is an expression a: v where a ∈ NI and v ∈ vt(a). Now, concept and role assertions of ALCHT@ have the following form: C(a)@[a1 : v1, . . . , an : vn ] r(a, b)@[a1 : v1, . . . , an : vn ] where C ∈ NC , r ∈ NR , a, b ∈ NI , and ai : vi are attribute-value pairs. Role and concept inclusion axioms of ALCHT@ introduce additional expressive power to refer to partially specified and variable annotation sets. An (annotation set) specifier can be a set variable X ∈ NV , a closed specifier [a1 : v1, . . . , an : vn ], or an open specifier ba1 : v1, . . . , an : vn c, where ai ∈ NI and either vi ∈ vt(ai ) or vi = X.b with X ∈ NV , b ∈ NI , and vt(ai ) = vt(b). Intuitively speaking, closed specifiers define specific annotation sets whereas open specifiers merely provide lower bounds. The notation X.b is used to copy all of the zero or more b-values of annotation set X to a new annotation set. The set of all specifiers is denoted S. A specifier is ground if it does not contain variables. ALCHT@ role expressions have the form r@S with r ∈ NR and S ∈ S. ALCHT@ concept expressions C, D are defined recursively: C, D F > | A@S | ¬C | (C u D) | ∃R.C (1) with A ∈ NC , S ∈ S and R an ALCHT@ role expression. We use abbreviations (C t D), ⊥, and ∀R.C for ¬(¬C u ¬D), ¬>, and ¬(∃R.¬C), respectively. ALCHT@ axioms are essentially just DL inclusions between ALCHT@ role and concept expressions, which may, however, share variables. Example 2. In an ontology containing biographical information, we might want to make sure that children cannot be born before their parents. This can be expressed by the axiom ∃bornIn@X.> v ¬∃hasChild@b c.∃bornIn@bbefore : X.timec.>. Similar axioms can be used, e.g., to state that nobody has more than one birthday (“is born before being born”). It is sometimes useful to represent annotations by variables while also specifying some further constraints on their possible values. This can be accommodated by adding such constraints as (optional) prefixes to axioms. Hence we define an ALCHT@ concept inclusion as an expression of the form X1 : S1, . . . , Xn : Sn (C v D), (2) where C, D are ALCHT@ concept expressions, S1, . . . , Sn ∈ S are closed or open specifiers, and X1, . . . , Xn ∈ NV are set variables occurring in C, D or in S1, . . . , Sn . ALCHT@ role inclusions are defined analogously, but with role expressions instead of the concept expressions. An ALCHT@ ontology is a set of ALCHT@ assertions, and role and concept inclusions. To simplify notation, we sometimes omit the specifier b c (meaning “any annotation set”) in role or concept expressions. In this sense, any ALCH axiom is also an ALCHT@ axiom. 3 Formal Semantics We first recall the general semantics of attributed DLs without temporal attributes. The semantics of ALCHT@ can then be obtained as a multi-sorted extension that imposes additional restrictions on the interpretation of time. An interpretation I = (∆I , ·I ) of attributed logic consists of a non-empty domain ∆ and a function ·I . Individual names a ∈ NI are interpreted as elements aI ∈ ∆I . I To interpret annotation sets, we use the set ΦI B Pfin ∆I × ∆I of all finite binary relations over ∆I . Now each concept name C ∈ NC is interpreted as a set C I ⊆ ∆I × ΦI of elements with annotations, and each role name r ∈ NR is interpreted as a set r I ⊆ ∆I × ∆I × ΦI of pairs of elements with annotations. Note that each element (pair of elements) may appear with multiple different annotations. I satisfies a concept assertion C(a)@[a1 : v1, . . . , an : vn ] if (aI , {(a1I , v1I ), . . . , (anI , vnI )}) ∈ C I , and likewise for role assertions. Expressions with free set variables are interpreted using variable assignments Z : NV → ΦI . A specifier S ∈ S is interpreted as a set S I, Z ⊆ ΦI of matching annotation sets. We set X I, Z B {Z(X)} for variables X ∈ NV . The semantics of closed specifiers is defined as follows: (i) [a: b] I, Z B {{(aI , bI )}} (ii) [a: X.b] I, Z B {{(aI , δ) | (b Ðn, δ) ∈ Z(X)}} I (iii) [a1 : v1, . . . , an : vn ] I, Z B { i=1 Fi } where {Fi } = [ai : vi ] I, Z for all i ∈ {1, . . . , n}. S I, Z therefore is a singleton set for variables and closed specifiers. For open specifiers, however, we define ba1 : v1, . . . , an : vn c I, Z to be the set {F ∈ ΦI | F ⊇ G for {G} = [a1 : v1, . . . , an : vn ] I, Z }. Now given A ∈ NC , r ∈ NR , and S ∈ S, we define: (A@S)I, Z B {δ | (δ, F) ∈ AI for some F ∈ S I, Z }, (r@S)I, Z B {(δ, ) | (δ, , F) ∈ r I for some F ∈ S I, Z }. Further DL expressions are defined as usual: >I, Z = ∆I , ¬C I, Z = ∆I \ C I, Z , (C u D)I, Z = C I, Z ∩ DI, Z , and (∃R.C)I, Z = {δ | there is (δ, ) ∈ RI, Z with  ∈ C I, Z }. I satisfies a concept inclusion of the form (2) if, for all variable assignments Z that satisfy Z(Xi ) ∈ SiI, Z for all 1 ≤ i ≤ n, we have C I, Z ⊆ DI, Z . Satisfaction of role inclusions is defined analogously. I satisfies an ontology if it satisfies all of its axioms. As usual, |= denotes both satisfaction and the induced logical entailment relation. Adding Time Time points t ∈ NT are encodings of natural numbers, which we denote by t I . Analogously, v I denotes a pair of numbers for a time interval v ∈ N2T . To represent time, we consider intervals of natural numbers, which can be finite intervals [k, `] = {n ∈ N | k ≤ n ≤ `} or infinite intervals [k, ∞) = {n ∈ N | k ≤ n}. A temporal domain ∆TI is a finite or infinite interval such that t I ∈ ∆TI for all t ∈ NT and v I ∈ ∆TI ×∆TI for all v ∈ N2T . Note that ∆TI can be finite if NT and N2T are (which is always admissible, since any ontology mentions only finitely many time points). A time-sorted interpretation I = (∆I , ·I ) has a sorted domain ∆I that is a disjoint union ∆II ∪ ∆TI ∪ ∆I2T , where ∆II is the abstract domain, ∆TI is a temporal domain, and ∆I2T = ∆TI × ∆TI . We interpret individual names a ∈ NI as elements aI ∈ ∆II . A pair (δ, ) ∈ ∆II × ∆I is well-typed, if one of the following holds: (i) δ = aI for a temporal attribute a of value type NT and  ∈ ∆TI ; (ii) δ = aI for a temporal attribute a of value type N2T and  ∈ ∆I2T ; or (iii) δ , aI for all temporal attributes a and  ∈ ∆II . Then ΦI is the set of all finite sets of well-typed pairs. The remainder of the interpretation function is defined as in the unsorted case, based on this sorted definition of ΦI . Time-sorted interpretations can be used to interpret ALCHT@ ontologies, but they do not take the intended semantics of time into account yet. For example, we might find that A(c)@[after : 1993] holds whereas A(c)@[time : t] does not hold for any time t ∈ NT with t I > 1993. To ensure consistency, we would like to view an interpretation with temporal domain ∆TI as a sequence (Ii )i ∈∆I of regular (unsorted) interpretations that T define the state of the world at each point in time. Such a sequence represents a local view of time as a sequence of events, whereas the time-sorted interpretation represents a global view that can explicitly refer to time points. Axioms of ALCHT@ refer to this global view, but it should be based on an actual sequence of events. To simplify the relationship between local and global views, we assume that the underlying abstract domain ∆II and interpretation of constants remains the same over time. Definition 3. Consider a temporal domain ∆TI and an abstract domain ∆II , and let (Ii )i ∈∆I be a sequence of ALCH@ interpretations with domain ∆II , such that, for all T a ∈ NI , we have aIi = aI j for all i, j ∈ ∆TI . We define a global interpretation for (Ii )i ∈∆I as a multisorted interpretation I = T (∆I , ·I ) as follows. Let aI = aIi for all a ∈ NI . For any finite set F ∈ ΦI , let FI B F ∩ (∆II × ∆II ) denote its abstract part without any temporal attributes. For any A ∈ NC , δ ∈ ∆I , and F ∈ ΦI with F \ FI , ∅, we have (δ, F) ∈ AI if and only if2 (δ, FI ) ∈ AIi for some i ∈ ∆TI , and the following conditions hold for all (aI , x) ∈ F: 2 ‘for some i ∈ ∆TI ’ is useful for attributes which universally quantify time points (e.g., until). – if a = time, then (δ, FI ) ∈ AI x , – if a = before, then (δ, FI ) ∈ AI j for some j < x, – if a = after, then (δ, FI ) ∈ AI j for some j > x, – if a = until, then (δ, FI ) ∈ AI j for all j ≤ x, – if a = since, then (δ, FI ) ∈ AI j for all j ≥ x, – if a = between, then (δ, FI ) ∈ AI j for some j ∈ [x], – if a = during, then (δ, FI ) ∈ AI j for all j ∈ [x], where [x] for an element x ∈ ∆I2T denotes the finite interval represented by the pair of numbers x, and j ∈ ∆TI . For roles r ∈ NR , we define (δ, , F) ∈ r I analogously. In words: in a global interpretation all tuples are consistent with the given sequence of local interpretations. One can see a global interpretation as a snapshot of a local interpretation, with timestamps encoding the information of the temporal sequence. If a global interpretation does not contain temporal attributes the characterization of Definition 3 holds vacuously for any temporal sequence, meaning that without temporal attributes the semantics is essentially the same as for ALCH@ . Definition 4. An interpretation of ALCHT@ is a time-sorted interpretation I that is a global interpretation of an interpretation sequence (Ii )i ∈∆I as in Definition 3. T A model of an ALCHT@ ontology O is an ALCHT@ interpretation that satisfies O, and O entails an axiom α, written O |= α, if α is satisfied by all models of O. By virtue of the syntax and semantics of ALCHT@ we can express background knowledge that helps to maintain integrity of the annotated knowledge and allows us to derive new information from it. Example 5. Along the lines of Example 2, we can state, e.g., that people cannot live after their death: Lived@X u ∃diedIn@b before : X.timec.> v ⊥ ∃bornIn@X.> v Lived@X With these background axioms in place, we can infer from the time-annotated facts in Example 1, e.g., Lived(Gutenberg)@[ between :[1394,1468]] Some temporal attributes are closely related. Clearly, time can be captured by using during or between with singleton intervals. Conversely, during can be expressed by specifying all time points in the respective interval explicitly using time, but this incurs an exponential blow-up over the binary encoding of time intervals. Similarly, between could be expressed as a disjunction of statements with specific times. Since time can be infinite, since and after cannot be captured using finite intervals. It may seem as if until and before correspond to during and between using intervals starting at 0. However, it is not certain that 0 is the first element in the temporal domain of an interpretation, and the next example shows that this cannot be assumed in general. Example 6. The ontology with the two axioms C(a)@[until : 10] and C@[before : 5] v ⊥ is satisfiable in ALCHT@ , but it does not have models that have times before 5. Replacing until : 10 with during : [0, 10] would therefore lead to an inconsistent ontology. 4 Reasoning in ALCHT@ In this section, we study the expressivity and decidability in ALCHT@ . Our first result, Theorem 7, shows that reasoning is on the first level of the analytical hierarchy and therefore highly undecidable. Theorem 7. Satisfiability of ALCHT@ ontologies is Σ11 -hard, and thus not recursively enumerable. Moreover, the problem is Σ11 -hard even with at most one set variable per inclusion and with only the temporal attributes time and after. Proof. We reduce from the following tiling problem, known to be Σ11 -hard [12]: given a finite set of tile types T with horizontal and vertical compatibility relations H and V, respectively, and t0 ∈ T, decide whether one can tile N × N with t0 appearing infinitely often in the first row. We define an ALCHT@ ontology OT,t0 that expresses this property. In our encoding, we use the following symbols: – a concept name A, to mark individuals representing a grid position with a time point; – a concept name P to keep time points associated with previous columns in the grid; – concept names At , for each t ∈ T, to mark individuals with tile types; – an individual name a, to be connected with the first row of the grid; – an auxiliary concept name I, to mark the individual a, and a concept name B, used to create the vertical axis; – role names r, s, to connect horizontally and vertically the elements of the grid, respectively. We define OT,t0 as the set of the following ALCHT@ assertion and concept inclusions. We start encoding the first row of the grid with an assertion I(a) and the concept inclusions: I v ∃r.A@btime : 0c and ∃r.A@X v ∃r.A@bafter : X.timec. Every element in A must be marked in at most one time point (in fact, exactly one): A@X v ¬A@bafter : X.timec (3) Every element representing a grid position can be associated with exactly one tile type at the same time point: Ä A@X v At @btime : X.timec, t ∈T ∃r.At @X v ¬∃r.At 0 @btime : X.timec, for t , t 0 ∈ T . We also have: At @X v A@btime : X.timec, for each t ∈ T to ensure that elements are in At and A at the same time point (exactly one one, see Eq. 3). The condition that t0 appears infinitely often in the first row is expressed with: I v ∃r.(At0 @btime : 0c t At0 @bafter : 0c), I u ∃r.At0 @X v ∃r.At0 @bafter : X.timec. To vertically connect subsequent rows of the grid, we have: I v B and B v ∃s.B. We add, for each t ∈ T, the following inclusion to ensure compatibility between vertically adjacent tile types: Ä ∃r.At @X v ∀s.∃r.( At 0 @btime : X.timec) (t,t 0 )∈V We also have: ∃s.∃r.A@X v ∃r.A@btime : X.timec to ensure that the set of time points in each row is the same. We now encode compatibility between horizontally adjacent tile types. We first state that, given a node associated with a time point p, for every sibling node d, if d is associated with a time point after p then we mark d with P and p: ∃r.A@X v ∀r.(¬A@bafter : X.timec t P@btime : X.timec). For each node, P keeps the time points associated with previous columns in the grid (finitely many). We also have: ∃r.P@X v ∃r.A@btime : X.timec and P@X v A@bafter : X.timec to ensure that P keeps only those previous time points. Finally, for each t ∈ T, we add to OT,t0 the inclusion: Ä ∃r.At @X v ∀r.(¬A@bafter : X.timec t P@bafter : X.timec t At 0 ). (t,t 0 )∈H Intuitively, as P keeps the time points associated with previous columns in the grid, only the node representing the horizontally adjacent grid position of a node associated with a time point p will not be marked with P after p. Theorem 8 shows that even if after is only allowed in assertions reasoning is undecidable, though, in the arithmetical hierarchy [22]. Theorem 8. Satisfiability of ALCHT@ ontologies with the temporal attributes time, after and before but after only in assertions is Σ10 -complete (recall Σ10 stands for RE). The problem is Σ10 -hard even with at most one set variable per inclusion. To recover decidability, we need to restrict ALCHT@ in some way. A simple approach of doing so is to consider ground ALCHT@ where we disallow set variables altogether. It is clear from the known complexity of ALCH that reasoning is ExpTime-hard. We establish a matching membership result by providing a satisfiability-preserving polynomial time translation to ALCH extended with role conjunctions and disjunctions (denoted ALCHb), where satisfiability is known to be in ExpTime [23]. Theorem 9. Satisfiability of ground ALCHT@ ontologies is ExpTime-complete. Proof. Consider a ground ALCHT@ ontology O, and let k0 < . . . < k n be the ascending sequence of all numbers mentioned (in binary encoding) in time points or in time intervals in O. We define NO B {k i | 0 ≤ i ≤ n} ∪ {k i + 1 | 0 ≤ i < n}, and let kmin B min(NO ) and kmax = max(NO ), where we assume kmin = k max = 0 if NO = ∅. For a finite interval v v ⊆ N, let NO be the set of all finite, non-empty intervals u ⊆ v with end points in NO . v The number of intervals in NO then is polynomial in the size of O. We translate O into an ALCHb ontology O† as follows. First, O† contains every axiom from O, with each annotated concept name A@S and each annotated role name r@S replaced by a fresh concept name AS and a fresh role name rS , respectively. Second, given a ground specifier S, we denote by S(a: b) the result of removing all temporal attributes from S and adding the pair a: b. Moreover, let ST be the set of temporal attribute-value pairs in S. Then, for each AS and rS with ST , ∅, O† contains the equivalences (as usual, ≡ refers to bidirectional v here): / / AS ≡ (AS(a:b) )] and rS ≡ (rS(a:b) )] (4) (a:b)∈ST (a:b)∈ST where the concept/role expressions (HS(a:b) )] for H ∈ {A, r } are defined as follows: . – (HS(during:v) )] = u ∈NO v HS(during:u) ] – (HS(between:v) ) = k ∈(v∩NO ) HS(during:[k,k]) Ã – (HS(time:k) )] = (HS(during:[k,k]) )] – (HS(since:k) )] = (HS(during:[k,kmax ]) )] u HS(since:kmax ) – (HS(until:k) )] = (HS(during:[kmin,k]) )] u HS(until:kmin ) – (HS(after:k) )] = (HS(between:[k+1,kmax ]) )] t HS(after:kmax ) – (HS(before:k) )] = (HS(between:[kmin,k−1]) )] t HS(before:kmin ) where k , kmin and k , kmax . If k ∈ {k min, kmax } then we set (HS(a:k) )] = HS(a:k) . Only polynomially many inclusions in the size of O are introduced by (4) in O† . Finally, given attribute-value pairs a: b and c: d for temporal attributes a and b, we say that a: b implies c: d if A(e)@[a: b] |= A(e)@[c: d] for some arbitrary A ∈ NC and e ∈ NI . Based on a given NI , this implication relationship is computable in polynomial time. We then extend O† with all inclusions AS v AT and rS v rT , where AS, AT and rS, rT are concept and role names occurring in O† , including those introduced in (4), such that for each temporal attribute-value pair c: d in T there is a temporal attribute-value pair a: b in S such that a: b implies c: d and: – T is an open specifier and the set of non-temporal attribute-value pairs in S is a superset of the set of non-temporal attribute-value pairs in T; or – S, T are closed specifiers and the set of non-temporal attribute-value pairs in S is equal to the set of non-temporal attribute-value pairs in T. This finishes the construction of O† . As shown in the appendix, O is satisfiable iff O† is satisfiable. While ground ALCHT@ can already be used for some interesting conclusions, it is still rather limited. However, satisfiability of (non-ground) ALCH@ ontologies is also decidable [14], and indeed we can regain decidability in ALCHT@ by disallowing expressions of the form X.a to be used with temporal attributes a. Indeed, using a similar reasoning as in the case of ALCH@ , we obtain a 2ExpTime upper bound by constructing an equisatisfiable (exponentially larger) ground ALCHT@ ontology. Theorem 10. Satisfiability of ALCHT@ ontologies without expressions of the form X.a for temporal attributes a is 2ExpTime-complete. Another way for regaining decidability is by limiting the temporal attributes that make reference to time points in the future. Using this assumption, we can translate any ALCHT@ ontology into a ground ALCHT@ ontology. In this case, however, the resulting ground ontology is double-exponentially larger if we assume that the size of the temporal domain has been encoded in binary. We therefore obtain a 3ExpTime upper bound (using Theorem 9). Theorem 11. Satisfiability of ALCHT@ ontologies with only the temporal attributes during, time, before and until is in 3ExpTime. Our result in our next Theorem 12 below is that this upper bound is tight. The proof is by reduction from the word problem for double-exponentially space-bounded alternating Turing machines (ATMs) [8] to the entailment problem for ALCHT@ ontologies. The main challenge in this reduction is that we need a mechanism that allows us to transfer the information of a double-exponentially space bounded tape, so that each configuration following a given configuration is actually a successor configuration (i.e., tape cells are changed according to the transition relation). We encode our tape using time: we can have exponentially many time points in an interval with end points encoded in binary. So considering each time point as a bit position, we construct a counter with exponentially many bits, encoding the position of double-exponentially many tape cells. Theorem 12. Satisfiability of ALCHT@ ontologies with only time and before is 3ExpTime- hard. 5 Lightweight Temporal Attributed DLs In this section we investigate ELHT@ , the fragment of ALCHT@ which uses only ∃, u, > and ⊥ in concept expressions. Though, even for ground ontologies, the satisfiability problem for ELHT@ is not tractable. Theorem 13. Satisfiability of ground ELHT@ ontologies is ExpTime-complete. Proof. The upper bound follows from Theorem 9. For the lower bound, we show how one can encode disjunctions (i.e., inclusions of the form > v B t C), which allow us to reduce satisfiability of ground ALCHT@ to satisfiability of ground ELHT@ ontologies. In fact, several combinations of the temporal attributes time, between, before and after suffice to encode > v B t C. As an example, see the following inclusions using the temporal attributes time and between: > v A@bbetween : [1, 2]c, A@btime : 1c v B, A@btime : 2c v C. One can also obtain the same type of encoding with before and after: > v A@b c, A@b before : 1c v B, A@b after : 0c v C. It is known that the entailment problem for EL ontologies with concept and role names annotated with time intervals over finite models is in PTime [16]. Indeed, our temporal attribute during can be seen as a syntactic variant of the time intervals in the mentioned work and, if we restrict to the temporal attributes time, during, since and until, the complexity of the satisfiability problem for ground ELHT@ ontologies is in PTime. Our proof here (for ground ELHT@ over N or over a finite interval in N) is based on a polynomial translation to ELH extended with role conjunction, where satisfiability is PTime-complete [23]. Theorem 14. Satisfiability of ground ELHT@ ontologies without the temporal attributes between, before and after is PTime-complete. Proof. Hardness follows from the PTime-hardness of EL [4]. For membership, note that the translation in Theorem 9 for the temporal attributes during, since and until does not introduce disjunctions or negations. So the result of translating a ground ELHT@ ontology belongs to ELH extended with role conjunction. 6 Discussion and Conclusion We investigated decidability and complexities of attributed description logics enriched with special attributes whose values are interpreted over a temporal dimension. We discussed several ways of restricting the general, undecidable setting in order to regain decidability. Our complexity results range from PTime to 3ExpTime. Some of the statements used in our examples can also be naturally expressed in temporal DLs. For instance, the first statement of Example 5 is expressible by ALC extended with Linear Temporal Logic [19,25] with: Lived u ♦∃bornIn.> v ⊥. Other authors have also considered extending ALC with Metric Temporal Logic (MTL) [11,3], where the last statement of Example 1 can be expressed with: ♦[1394,1404] bornIn(Gutenberg, Mainz). However, the statement in Example 2 cannot be naturally expressed by temporal DLs. The complexity results can also be very different, for instance, the complexity of propositional MTL is already undecidable over the reals and ExpSpace-complete over the naturals [1], whereas in Theorem 9 of this paper we show that we can enhance ALC with many types of time related annotations with time points encoded in binary while keeping the same ExpTime complexity of ALC. As future work, we plan to study forms of generalising our logic to capture the semantics of other standard types of annotations in knowledge graphs, such as provenance and spatial information. Acknowledgements This work was partially supported by the DFG within the cfaed Cluster of Excellence, CRC 912 (HAEC), and Emmy Noether grant KR 4381/1-1, and by the ERC in Consolidator Grant DeciGUT. References 1. R. Alur and T.A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35 – 77, 1993. 2. Alessandro Artale, Roman Kontchakov, Frank Wolter, and Michael Zakharyaschev. Temporal description logic for ontology-based data access. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pages 711–717, 2013. 3. Franz Baader, Stefan Borgwardt, Patrick Koopmann, Ana Ozaki, and Veronika Thost. Metric temporal description logics with interval-rigid names. In Frontiers of Combining Systems - 11th International Symposium, FroCoS, pages 60–76, 2017. 4. Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, Proc. 19th Int. Joint Conf. on Artificial Intelligence (IJCAI’05), pages 364–369. Professional Book Center, 2005. 5. Franz Baader, Silvio Ghilardi, and Carsten Lutz. LTL over description logic axioms. ACM Trans. Comput. Log., 13(3), 2012. 6. Daniela Berardi, Diego Calvanese, and Giuseppe De Giacomo. Reasoning on UML class diagrams. Artif. Intell., 168(1-2):70–118, 2005. 7. Claudia Carapelle and Anni-Yasmin Turhan. Description logics reasoning w.r.t. general Tboxes is decidable for concrete domains with the EHD-property. In ECAI 2016 - 22nd European Conference on Artificial Intelligence, pages 1440–1448, 2016. 8. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. of the ACM, 28(1):114–133, 1981. 9. Jan Chomicki. Temporal query languages: A survey. In Dov M. Gabbay and Hans Jürgen Ohlbach, editors, Proc. 1st Int. Conf. on Database Theory (ICDT’94), volume 827 of LNCS, pages 506–534. Springer, 1994. 10. Michael David Fisher, Dov M. Gabbay, and Lluis Vila, editors. Handbook of Temporal Reasoning in Artificial Intelligence. Elsevier, 2005. 11. Víctor Gutiérrez-Basulto, Jean Christoph Jung, and Ana Ozaki. On metric temporal description logics. In Proc. of the 22nd Eur. Conf. on Artificial Intelligence (ECAI’16), pages 837–845. IOS Press, 2016. 12. David Harel. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM, 33(1):224–248, 1986. 13. Johannes Hoffart, Fabian M. Suchanek, Klaus Berberich, and Gerhard Weikum. YAGO2: A spatially and temporally enhanced knowledge base from Wikipedia. J. of Artif. Intell., 194:28–61, 2013. 14. Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Veronika Thost. Attributed description logics: Ontologies for knowledge graphs. In The Semantic Web - ISWC - 16th International Semantic Web Conference, pages 418–435, 2017. 15. Markus Krötzsch, Maximilian Marx, Ana Ozaki, and Veronika Thost. Attributed description logics: Reasoning on knowledge graphs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, pages 5309–5313, 2018. 16. Jared Leo, Ulrike Sattler, and Bijan Parsia. Temporalising EL concepts with time intervals. In Proc. 27th Int. Workshop on Description Logics (DL’14), volume 1193 of CEUR Workshop Proceedings, pages 620–632. CEUR-WS.org, 2014. 17. Carsten Lutz. Combining interval-based temporal reasoning with general tboxes. Artificial Intelligence, 152(2):235 – 274, 2004. 18. Carsten Lutz, Volker Haarslev, and Ralf Möller. A concept language with role-forming predicate restrictions. Technical report, University of Hamburg, 1997. 19. Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Temporal description logics: A survey. In 15th International Symposium on Temporal Representation and Reasoning, TIME, pages 3–14, 2008. 20. Maximilian Marx, Markus Krötzsch, and Veronika Thost. Logic on MARS: Ontologies for generalised property graphs. In Carles Sierra, editor, Proc. 26th Int. Joint Conf. on Artificial Intelligence (IJCAI’17), pages 1188–1194. IJCAI, 2017. 21. Ana Ozaki, Markus Krötzsch, and Sebastian Rudolph. Happy ever after: Temporally attributed description logics (extended technical report). Available online at https://iccl.inf. tu-dresden.de/web/Inproceedings3101, 2018. 22. Hartley Rogers, Jr. Theory of Recursive Functions and Effective Computability. MIT Press, paperback edition edition, 1987. 23. Sebastian Rudolph, Markus Krötzsch, and Pascal Hitzler. Cheap Boolean role constructors for description logics. In Steffen Hölldobler, Carsten Lutz, and Heinrich Wansing, editors, Proc. 11th European Conf. on Logics in Artificial Intelligence (JELIA’08), volume 5293 of LNAI, pages 362–374. Springer, 2008. 24. Denny Vrandečić and Markus Krötzsch. Wikidata: A free collaborative knowledgebase. Commun. ACM, 57(10), 2014. 25. Frank Wolter and Michael Zakharyaschev. Temporalizing description logics. Frontiers of Combining Systems, 2:379–402, 1999.