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, T it turns out that reasoning in our temporally attributed description logic ALCH@ is highly undecidable; thus we establish restrictions where it becomes decidable, and even tractable.
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 [
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
[
The paper is self-contained. Details on some long proofs can be found in the appendix
of the extended online version [
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 [
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 N2 . We represent time points T 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 N2 . Moreover, we require T that there are the following seven special individual names, called temporal attributes: time; before; after; until; since; during; between 2 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 2 NI for this purpose: during and between have value type N2 , all other temporal attributes have value type NT, and all other individuals
T have value type NI. An attribute-value pair is an expression a: v where a 2 NI and v 2 vt¹aº. Now, concept and role assertions of ALCHT@ have the following form:
C; D F > j A@S j :C j ¹C u Dº j 9R:C (1) with A 2 NC, S 2 S and R an ALCHT@ role expression. We use abbreviations ¹C t Dº, ?, and 8R:C for :¹:C u :Dº, :>, and :¹9R::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 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 2 S are closed or open specifiers, and X1; : : : ; Xn 2 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
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 I and a function I . Individual names a 2 NI are interpreted as elements aI 2 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 2 NC is interpreted as a set CI I I of elements with annotations, and each role name r 2 NR is interpreted as a set rI 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º@bda1 : v1; : : : ; an : vnce if ¹aI; f¹a1I; v1I º; : : : ; ¹anI; vnI ºgº 2 CI , and likewise for role assertions. Expressions with free set variables are interpreted using variable assignments Z : NV ! I . A specifier S 2 S is interpreted as a set SI;Z I of matching annotation sets. We set XI;Z B fZ¹Xºg for variables X 2 NV. The semantics of closed specifiers is defined as follows:
(i) bda: bceI;Z B ff¹aI; bI ºgg ((iiiii)) bdbdaa1: :Xv:1b; ce:I:;:Z; aBn : fvfn¹ceaII;Z; Bºj f¹ÐbIin;=1ºF2i gZw¹hXeºreggfFi g = bdai : viceI;Z for all i 2 f1; : : : ; ng. SI;Z therefore is a singleton set for variables and closed specifiers. For open specifiers, however, we define ba1 : v1; : : : ; an : vncI;Z to be the set fF 2
I j F
G for fGg = bda1 : v1; : : : ; an : vnceI;Z g: Now given A 2 NC, r 2 NR, and S 2 S, we define: ¹A@SºI;Z B f j ¹ ; Fº 2 AI for some F 2 SI;Z g; ¹r@SºI;Z B f¹ ; º j ¹ ; ; Fº 2 rI for some F 2 SI;Z g: Further DL expressions are defined as usual: >I;Z = I , :CI;Z = I n CI;Z , ¹C u DºI;Z = CI;Z \ DI;Z , and ¹9R:CºI;Z = f j there is ¹ ; º 2 RI;Z with 2 CI;Z g.
I satisfies a concept inclusion of the form (2) if, for all variable assignments Z that satisfy Z ¹Xi º 2 SiI;Z for all 1 i n, we have CI;Z DI;Z . Satisfaction of role inclusions is defined analogously. I satisfies an ontology if it satisfies all of its axioms. As usual, j= denotes both satisfaction and the induced logical entailment relation. Adding Time Time points t 2 NT are encodings of natural numbers, which we denote by tI . Analogously, vI denotes a pair of numbers for a time interval v 2 N2 . To T represent time, we consider intervals of natural numbers, which can be finite intervals »k; `¼ = fn 2 N j k n `g or infinite intervals »k; 1º = fn 2 N j k ng. A temporal domain TI is a finite or infinite interval such that tI 2 TI for all t 2 NT and vI 2 TI TI for all v 2 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 [ 2IT , where II is the abstract domain, TI is a temporal domain, and 2IT = TI TI . We interpret individual names a 2 NI as elements aI 2 II . A pair ¹ ; º 2 II I is well-typed, if one of the following holds: (i) (ii) (iii) = aI for a temporal attribute a of value type NT and = aI for a temporal attribute a of value type N2 and T , aI for all temporal attributes a and 2 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º@bdafter: 1993ce holds whereas A¹cº@bdtime: tce does not hold for any time t 2 NT with tI > 1993. To ensure consistency, we would like to view an interpretation with temporal domain TI as a sequence ¹Ii ºi 2 TI of regular (unsorted) interpretations that 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 2 TI be a sequence of ALCH@ interpretations with domain II , such that, for all a 2 NI, we have aIi = aIj for all i; j 2 TI .
We define a global interpretation for ¹Ii ºi 2 TI as a multisorted interpretation I = ¹ I; I º as follows. Let aI = aIi for all a 2 NI. For any finite set F 2 I , let FI B F \ ¹ II II º denote its abstract part without any temporal attributes. For any A 2 NC, 2 I , and F 2 I with F n FI , ;, we have ¹ ; Fº 2 AI if and only if2 ¹ ; FI º 2 AIi for some i 2 TI , and the following conditions hold for all ¹aI; xº 2 F: 2 ‘for some i 2 TI ’ is useful for attributes which universally quantify time points (e.g., until). – if a = time, then ¹ ; FI º 2 AIx , – if a = before, then ¹ ; FI º 2 AIj for some j < x, – if a = after, then ¹ ; FI º 2 AIj for some j > x, – if a = until, then ¹ ; FI º 2 AIj for all j x, – if a = since, then ¹ ; FI º 2 AIj for all j x, – if a = between, then ¹ ; FI º 2 AIj for some j 2 »x¼, – if a = during, then ¹ ; FI º 2 AIj for all j 2 »x¼, where »x¼ for an element x 2 2IT denotes the finite interval represented by the pair of numbers x, and j 2 TI . For roles r 2 NR, we define ¹ ; ; Fº 2 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 2 TI as in Definition 3.
A model of an ALCHT@ ontology O is an ALCHT@ interpretation that satisfies O, and O entails an axiom , written O j= , if is satisfied by all models of O. T
By virtue of the syntax and semantics of ALCH@ 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:
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º@bduntil: 10ce and C@bdbefore: 5ce 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.
T Reasoning in ALCH@ T . Our first result, In this section, we study the expressivity and decidability in ALCH@ 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 [
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: Every element in A must be marked in at most one time point (in fact, exactly one): (3) Every element representing a grid position can be associated with exactly one tile type at the same time point: Ä 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: To vertically connect subsequent rows of the grid, we have: I v B and B v 9s:B: We add, for each t 2 T , the following inclusion to ensure compatibility between vertically adjacent tile types: Ä We also have: 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: For each node, P keeps the time points associated with previous columns in the grid (finitely many). We also have: to ensure that P keeps only those previous time points. Finally, for each t 2 T , we add to OT;t0 the inclusion: Ä ¹t;t0º2H
At0º: 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 [
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 [
We translate O into an AOLCHb ontology Oy as follows. First, Oy 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 , ;, Oy contains the equivalences (as usual, refers to bidirectional v here):
AS
/ ¹a:bº2ST ¹AS¹a:bºº ] and rS / ¹rS¹a:bºº
] ¹a:bº2ST (4) where the concept/role expressions ¹HS¹a:bºº] for H 2 f A; r g are defined as follows: – ¹HS¹during:vºº] = .u 2NOv HS¹during:uº – ¹HS¹between:vºº] = Ãk 2¹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 2 fkmin; kmaxg then we set ¹HS¹a:kºº] = HS¹a:kº. Only polynomially many inclusions in the size of O are introduced by (4) in Oy.
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º@bda : bce j= A¹eº@bdc : dce for some arbitrary A 2 NC and e 2 NI. Based on a given NI, this implication relationship is computable in polynomial time. We then extend Oy with all inclusions AS v AT and rS v rT , where AS; AT and rS; rT are concept and role names occurring in Oy, 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 Oy. As shown in the appendix, O is satisfiable iff Oy 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 [
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) [
Theorem 13. Satisfiability of ground E LHT@ 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 E LHT@ 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@bbefore : 1c v B; A@bafter : 0c v C:
It is known that the entailment problem for E L ontologies with concept and role
names annotated with time intervals over finite models is in PTime [
Theorem 14. Satisfiability of ground E LHT@ ontologies without the temporal attributes between, before and after is PTime-complete.
Proof. Hardness follows from the PTime-hardness of E L [
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 [
Other authors have also considered extending ALC with Metric Temporal Logic
(MTL) [
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.