Introduction
Temporal description logics (TDLs) extend classical DLs, providing built-in means to
represent and reason about temporal aspects of knowledge. The importance of TDLs
stems from the need of relevant applications to capture temporal and dynamic aspects
of knowledge, e.g., in medical and life science ontologies, which are very large but
still demand efficient reasoning, such as SNOMED CT and FMA [
A notable approach to designing TDLs is to combine DLs with temporal logics
commonly used in software/hardware verification such as LTL, CTL( ), and to provide a
two-dimensional product-like semantics [
Alas, TDLs based on the Boolean-complete DL ALC with rigid roles cannot be
effectively used since they become undecidable when temporal operators are applied to
concepts and a general TBox is allowed [
Interestingly, no research has been yet devoted to TDLs based on EL in the presence
of restricted TBoxes, such as classical TBoxes, which consist solely of definitions of the
form A C with A atomic and unique, or acyclic TBoxes, which additionally forbid
syntactic cycles in definitions. This is surprising since in the presence of general TBoxes
TDLs based on EL tend to be as complex as the ALC variant [
These considerations lead us to investigating TDLs with rigid roles based on EL and the (branching-time) CTL allowing for temporal concepts and acyclic TBoxes. We are convinced that TDLs designed in this way are suitable for temporal extensions of biomedical ontologies: large parts of SNOMED CT and GO are acyclic EL-TBoxes.
Our main contributions are algorithms for standard reasoning problems and (mostly
tight) complexity bounds. We begin by showing that the combination of CTL and ALC
with empty and acyclic TBoxes is decidable. Our nonelementary upper bound is optimal
even when the set of temporal operators is restricted to E3 (“possibly eventually”) or
E (“possibly next”). We then replace ALC with EL and maintain the restriction to
E3; E and empty TBoxes. We particularly show that the resulting TDLs are decidable
in PTIME with one of the two operators, and CONP-complete with both. To this aim, we
employ canonical models, together with expansion vectors [
Rigid roles? no TBoxes general yes general CTLALC
CTLEEL ;E3
=EXPTIME [
undecidable [
PTIME (6) PTIME (6) CONP, (2) CONEXPTIME (5) yes empty nonelem., decidable (1)
PTIME (6)
PTIME (6)
=CONP (2)
=PSPACE [
PSPACE (9)
The relatively low complexity that we obtain for EL-based TDLs over restricted
TBoxes are in sharp contrast with the undecidability and nonelementary lower bounds
known for the same logics over general TBoxes [
Additional technical notions and proofs are in a report: http://tinyurl.com/ijcai15tdl 2
Preliminaries We introduce CTLALC , a TDL based on the classical DL ALC. Let NC and NR be countably infinite sets of concept names and role names, respectively. We assume that NC and NR are partitioned into two countably infinite sets: NrCig and Nloc of rigid concept C names and local concept names, respectively; and, NrRig and Nloc of rigid role names and R local role names, respectively. CTLALC -concepts C are defined by the grammar
C := > j A j :C j C u D j 9r:C j E C j E2C j E(CU D)
where A ranges over NC, r over NR. We use standard DL abbreviations [
The semantics of classical DLs, such as ALC, is given in terms of interpretations
of the form I = ( ; I ), where is a non-empty set called the domain and I is an
interpretation function that maps each A 2 NC to a subset AI and each r 2 NR to
a binary relation rI . The semantics of CTLALC is given in terms of temporal
interpretations based on infinite trees [
We now define the semantics of CTLALC -concepts. A path in T = (W; E) starting at a node w is an infinite sequence = w0w1w2 with w0 = w and (wi; wi+1) 2 E. We write [i] for wi, and use Paths(w) to denote the set of all paths starting at the node w. The mapping I;w is extended from concept names to CTLALC -concepts as follows.
>I;w = (9r:C)I;w = fd 2 j 9e : (d; e) 2 rI;w ^ e 2 CI;wg
(C u D)I;w = CI;w \ DI;w
(E(CU D))I;w = fd j 9 2 Paths(w) : 9j
(E C)I;w = fd j 9 2 Paths(w) : d 2 CI; [
A temporal interpretation I is a model of a concept C if CI;" 6= ;; it is a model of an acyclic TBox T , written I j= T , if AI;w = CI;w for all A C 2 T and w 2 W ; it is a model of a concept inclusion C v D, written I j= C v D, if CI;w DI;w for all w 2 W .
The two main reasoning tasks we consider are concept satisfiability and subsumption. A concept C is satisfiable relative to an acyclic TBox T if there is a common model of C and T . A concept D subsumes a concept C relative to an acyclic TBox T , written T j= C v D, if I j= C v D for all models I of T . If T is empty, we write j= C v D. 3
First Observations
We start by observing that the combination of CTL and ALC with rigid roles relative to
empty and acyclic TBoxes is decidable and inherently nonelementary. In a nutshell, we
show the upper bounds using a variant of the quasimodel technique [11, Thm. 13.6]; the
lower bound follows from the fact that satisfiability for the product modal logics S4 K
and K K is inherently nonelementary [
With Theorem 1 and the third column of Table 1 in mind, we particularly set as our goal the identification of elementary (ideally tractable) TDLs. To this aim, we study combinations of (fragments of) CTL with the lightweight DL EL. CTLEL is the fragment of CTLALC that disallows the constructor : (and thus the abbreviations C t D, 8r:C, A2, . . . ). The standard reasoning problem for CTLEL, as for EL, is concept subsumption since each concept and TBox are trivially satisfiable. In what follows we consider various fragments of CTLEL obtained by restricting the available temporal operators. We denote the fragments by putting the allowed operators as a superscript. In this context, we view each of the operators E3, A2 as primitive instead of as an abbreviation.
In order to keep the presentation of our main results accessible, in Sections 5-6, we concentrate on the case where only rigid role names and local concept names are present. Later on, in Section 7, we explain how to deal with the general case. 4
EL We begin by investigating the complexity of subsumption relative to the empty TBox for a TDL whose subsumption relative to general TBoxes is undecidable: CTLE ;E3. EL Theorem 2. Concept subsumption relative to the empty TBox is CONP-complete for CTLEEL ;E3 with rigid roles and in PTIME for CTLEEL and CTLEEL3 with rigid roles. CONP-hardness is obtained by embedding EL plus transitive closure into CTLE ;E3; EL the jump in complexity comes from the ability to express disjunctions, e.g., j= E3C v C t E E3C: We next explain CONP-membership; the PTIME results are a byproduct and improved later.
We proceed in two steps: first we provide a characterization of j= C v D where C is an CTLE -concept and D an CTLE ;E3-concept. Next we generalize this characterization
ELE ;E3-concepts C. EL to CTLEL
Given a CTLE -concept C, the description tree tC = (VC ; LC ; EC ) for C is a
EL labeled graph corresponding to C’s syntax tree; we denote its root by xC . For example, if C = E (9r:A u 9s:B), then tC is given in Figure 1, left.
For plain EL, we have j= C v D if and only if there is a homomorphism from tD
to tC , which can be tested in polynomial time [
From (1), (2), and the preservation properties of homomorphisms, we obtain: Lemma 3. For all CTLE -concepts C and all CTLE ;E3-concepts D, we have j= C v D if and only if xC E2LDIC;xC . EL Now xC 2 DIC;xC can be verified by model-checking D in world xC and element xC of Ipre
C , which is the polynomial-sized modification of I where the lastly added infinite
path of worlds is replaced by a single loop, see Fig. 1, right. Since IC is the unraveling
of IpCre into the temporal dimension, IC and Ipre satisfy the same concepts in their roots.
C
TevheeroyreEm32infoCr CbTyLaEEL -ethdugse fionltloCwasn. dTahdeaCptTinLgEELt3hepanrottcioann obfeaohbotaminoemdobryphreispmre.senting
For CTLE ;E3, we use expansion vectors introduced in [
EL dimension. Let C be a CTLE ;E3-concept with n occurrences of E3. An expansion
EL vector for C is an n-tuple U = (u1; : : : ; un) of integers ui > 0. Intuitively, U fixes a specific number of temporal steps taken for each E3 in C when constructing tC and IC . More precisely, we denote with C[U ] the CTLE -concept obtained from C by replacing the i-th occurrence of E3 with (E )ui , i.e.E,Li times E . For example, if C = E39r:E3(A u E B) and U = (2; 0), then C[U ] = E E 9r:(A u E B).
Let UCm = f(u1; : : : ; un) j ui 6 m for all ig. We denote with tdepth(D) the nesting depth of temporal operators in D. We use expansion vectors with entries bounded by tdepth(D) to reduce 6j= C v D for CTLE ;E3 to the case where C is from CTLE .
EL EL Lemma 4. For all CTLE ;E3-concepts C; D, we have j= C v D if and only if
ELtdepth(D)+1. j= C[U ] v D for all U 2 UC Together with Lemma 3, this yields the desired polynomial-time guess-and-check procedure for deciding j= C v D.
CTLE
EL and CTLE3 relative to Acyclic TBoxes
EL
The results of Theorem 2 transfer to acyclic TBoxes with an exponential blowup due to
unfolding [
For the subfragments CTLE and CTLE3, we can even show polynomial complexity:
EL EL Theorem 6. Concept subsumption relative to acyclic CTLE - and CTLE3-TBoxes with EL EL rigid roles is in PTIME.
We first concentrate on the E3 case and explain below how to deal with the E one. We
focus w.l.o.g. on subsumption between concept names and assume that the input TBox
is in normal form (NF), i.e., each axiom is of the shape A A1 u A2, A E3A1, or
A 9r:A1, where Ai 2 NC [ f>g and r 2 NR. As usual, a subsumption-equivalent
TBox in NF can be computed in polynomial time [
To prove a PTIME upper bound, we devise a completion algorithm in the style
of those known for EL and (two-dimensional) extensions, cf. [
The algorithm for deciding subsumption initializes G as follows. For all r 2 ROL, set R(r) = ;. Set W = CN CN[fE3A j A 2 CNg. Set E = f(E3A; AA); (AB; A>) j A; B 2 CNg. For all A 2 CN, set Q(A; w) = f>; Bg if w = AB and Q(A; w) = f>g otherwise.
Intuitively, the unraveling of (W; E) is the temporal tree underlying the minimal model and the mappings Q and R contain condensed information on how to interpret concepts and roles, respectively. More specifically, the data stored in Q(A; ) describes the temporal evolution of an instance of A. For example, Q(A; AA) collects all concept names B such that T j= A v B; likewise, Q(A; E3A) captures everything that follows from E3A. Finally, Q(A; AB) contains concept names that are implied by B given that B appears in the temporal evolution of an instance of A, i.e., B0 2 Q(A; AB) implies T j= A u E3B v E3(B u B0).
After initialization, the algorithm extends G by applying the completion rules depicted in Figure 2 in three phases. In the first phase – also called FORWARD-phase, since definitions A C 2 T are read as A v C – rules F1-F3 are exhaustively applied in order to generate a fusion-like representation by adding witness-worlds and witnessexistentials as demanded. Most notably, rule F2 introduces a pointer to the structure representing the temporal evolution of an instance of B0. F1 If B 2 Q(A; AA0) & B F2 If B 2 Q(A; w) and B F3 If B 2 Q(A; w) & B
E3B0 2 T , then add (AA0; AB0) to E 9r:B0 2 T , then set (A; w) !r (B0; B0B0)
A1 uA2 2 T , then add A1;A2 to Q(A; w) C1 If (BB; w) 2 E and (A; w0) !r (B; BB), then add (w0; w) to E C2 If (A; w) !r (B; BB), then a) (A; w0) !r (B; E3B) for all w0 6= w with (w0; w) 2 E b) (A; w0) !r (B; w0) for all w0 with (w0; w) 2= E B1 If B 2 Q(A; w), (w0; w) 2 E , and A0 B2 If A 2 Q(B; w), (A0; w0) !r (B; w), and A00 B3 If A1; A2 2 Q(B; w) & A
A1 u A2 2 T then add A to Q(B; w)
E3B 2 T , then add A0 to Q(A; w0)
9r:A 2 T then add A00 to Q(A0; w0)
Subsequently, G is extended to conform with the constant domain assumption and reflect rigidity of roles by exhaustively applying rules C1, C2. Here read C2 as ‘if two points are connected via r in some world, then they should be connected in all worlds.’ Note that Q(B; E3B) is used as a representative for the entire “past” of B in part a).
In the final phase, BACKWARD-completion rules B1-B3 are exhaustively applied in order to respect the ‘backwards’-direction of definitions, i.e., definitions A C 2 T are read as A w C. This separation into a FORWARD and BACKWARD phase is sanctioned by acyclicity of the TBox. In fact, one run through each phase is enough; note that no new tuples are added to E or R in the BACKWARD-phase.
The following lemma shows correctness of our algorithm. To prove “(”, we show that (a certain unraveling of) G “embeds” into every model of A and T . For this purpose, we need to adapt the notion of a homomorphism to temporal interpretations and rigid roles. For “)”, we construct from G a model I of T with d 2 AI;w n BI;w for some d; w. The algorithm runs in polynomial time: the size of the data structures W , E, and R is clearly polynomial and the mapping Q( ; ) is extended in every rule application, so the algorithm stops after polynomially many steps.
Finally, we sketch two modifications of the algorithm such that it works for E instead of E3. First, we have to use a non-transitive version of B1. Second, and a bit more subtly, we have to replace E3A 2 W with E kA, 1 k jT j to capture what is implied by E kA; more precisely, B0 2 Q(A; E kA) implies T j= E kA v B0, where E k denotes E E k times.
We next show that there is a jump in the complexity if increasing domains are considered instead of constant ones. Intuitively, this can be explained by the fact that increasing domains allow rigid roles to mimic the behaviour of the A2-operator. In the next section, we show that adding A2 to fE3g indeed leads to PSPACE-hardness. Theorem 8. Concept subsumption relative to acyclic CTLE - and CTLE3-TBoxes with rigid roles and increasing domains is PSPACE-hard. EL EL
EL We now add A2 and observe an increase in complexity over acyclic TBoxes. Theorem 9. Concept subsumption relative to acyclic CTLE3;A2-TBoxes with rigid EL roles is PSPACE-complete.
The lower bound is obtained via a reduction from QBF validity. For the upper bound, we again consider w.l.o.g. subsumption between concept names and assume that the acyclic TBox is in normal form, i.e., axioms are of the shape A A1 u A2, A E3A1, A A2A1, or A 9r:A1, where Ai 2 NC [ f>g and r 2 NR. We also restrict ourselves again to only rigid roles. CN and ROL are used as before.
In contrast to the previous section, we cannot maintain the entire minimal model in memory since the added operator A2 can be used to enforce models of exponential size. Instead, we will compute all concepts implied by the input concept A (the left-hand side of the subsumption to be checked) by iteratively visiting relevant parts of the minimal model. Our main tool for doing so are traces.
Definition 10. A trace is a tuple ( ; E; R) where is a sequence (d0; w0) (dn; wn) such that for all 0 i < n one of the following is true. (1) di = di+1 and (wi; wi+1) 2 E. (2) wi = wi+1 and (di; di+1) 2 R(r) for some r 2 ROL.
Input: Acyclic TBox T , concept names A; B
Output: true if T j= A v B, false otherwise 1 := (d0; w0); Q(d0; w0) := fA; >g; 2 E := ;; R(r) := ; for all r 2 ROL; 3 expand( ; E; R); 4 return true if B 2 Q(d0;w0), false otherwise; Intuitively, traces represent paths through temporal interpretations, Algorithm 1: Subsumption in CTLEEL3;A2 which in each step follow either the temporal relation (Def. 10, 1) or a DL relation r (2); so, in a pair (d; w), d can be thought of as a domain element and w as a world.
Our algorithm, whose basic structure is given by Alg. 1, enu- 5 procedure expand ( ; E; R) : merates on input T ; A; B, in a sys- 6 complete ( ; E; R; Q); tematic tableau-like way, all traces 7 if ( ; Q) is periodic at (i; j) then that must appear in every model 8 add (wj 1; wi) to E; of A and T . Note that in the con- 9 truncate; text of Algorithm 1 a trace is used 10 complete ( ; E; R; Q); as the basis for inducing a richer 11 return; structure that conforms with the 12 (d; w) := last element of ; constant domain assumption and 13 captures rigidity; see Example 11 14 below. The algorithm also main- 15 tains an additional mapping Q that 16 labels each point (d; w) of the 17 trace (and all the induced points) 18
19 with a set Q(d; w) CN. The 20 set Q(d; w) captures all concept names that are satisfied in the minimal model at points represented by (d; w). foreach A 2 Q(d; w) with A 9r:B 2 T do
Q(d0; w) = fB; >g for a fresh d0; add (d; d0) to R(r); expand ( (d0; w); E; R); foreach A 2 Q(d; w) with A E3B 2 T do
Q(d; w0) = fB; >g for a fresh w0; add (w; w0) to E; expand ( (d; w0); E; R); R1 If A R2 If A
A1 u A2 2 T and A 2 Q ( ), then add A1; A2 to Q ( )
A1 u A2 2 T and A1; A2 2 Q ( ), then add A to Q ( ) R3 If (d; d0) 2 R(r), B 2 Q(d0; w), A R4 If B 2 Q(d; w), (w0; w) 2 E , A R5 If B 2 Q(d; w), (w; w0) 2 E , B
9r:B 2 T , then add A to Q(d; w) E3B 2 T , then add A to Q(d; w0)
A2A 2 T , then add B; A to Q(d; w0) R6 If (d; d0) 2 R(r), B 2 Qcert(d0), A
9r:B 2 T , then add A to Qcert(d) R7 If B 2 Qcert(d), A
A2B 2 T , then add A to Qcert(d) R8 If B 2 Qcert(d), then add B to Q(d; w) for all w R9 If B 2 QA2(d; w), A R10 If A 2 Q(d; w), A
A2B 2 T , add A to Q(d; w)
A2B 2 T , add A; B to QA2(d; w) R11 If (d; d0) 2 R(r), B 2 QA2(d0; w), A
9r:B 2 T , then add A to QA2(d; w) R12 If A 2 QA2(d; w), A E3B 2 T , w0 added due to
A 2 Q(d; w) in Line 18, B0 2 Q(d; w0), A0 E3B0 2 T , then add A0 to QA2(d; w)
The basics of Algorithm 1 are the following. In Lines 1 and 2, it creates a trace consisting of a single point representing A and initializes the necessary data structures. In Line 3, the systematic expansion is set off. When that is finished, the algorithm just returns whether or not B (the right-hand of the subsumption) has been added during the expansion. As for the expand procedure: – in Line 6 and 10, the algorithm updates the mapping Q; – Line 7 contains some termination condition; and finally, – the loops in Lines 13 & 17 enumerate all 9r:B and E3B that appear in the set
Q(d; w) of the last trace element and expand the trace to witness these concepts. This basic description of the algorithm leaves open several points: (i) the precise behavior of the subroutine complete, (ii) when a trace is periodic, and (iii) what happens inside the truncate command in Line 9. Let us start with describing the subroutine complete. It uses additional mappings Qcert(d) CN and QA2(d; w) CN, which intuitively contain all the concept names that d satisfies certainly, i.e., in all worlds, and starting from world w, respectively. It proceeds in two steps. (1) Initialize undefined Q(d; w) and Qcert(d) with f>g, and undefined QA2(d; w) with Qcert(d). (2) Apply rules R1-R12 in Figure 3 to Q( ), Qcert( ) and QA2( ).
The number of rules is indeed scarily high; however, they can be divided into four digestible groups: R1 and R2 are used to ensure that all sets Q are closed under conjunction; R3-R5 are used to complete Q( ). Note that R1-R4 are already known from the algorithm of the previous section. Furthermore, R6-R8 are used to deal with Qcert( ); and R9-R12 to update QA2( ). As an example of the interplay between the different mappings take R9: If B is certain for d starting in world w and A A2B, then we also know that d satisfies A in w; and R11 for the interplay between temporal operators and rigid roles: indeed, for r rigid, j= 9r:A2B v A29r:B. Example 11. Let T = fA E3A1; A1 9r:B; B E3A1g be the input TBox; and T j= A v A1 is to be checked. Figure 4 (left) shows the trace initiated at (d0; w0) with Q(d0; w0) = f>; Ag, and further expanded in Lines 13 and 17. The trace, as mentioned above, induces a richer structure, reflecting rigid roles and the constant domain assumption; see Fig. 4 (center). This richer structure is then completed to properly enrich the types Q(d; w) of each element. In particular, during completion, further concept names are added to the corresponding types (Fig. 4, right). One can now easily see that T j= A v A1 indeed holds. Furthermore, note that T 6j= A v A1, if r is local or increasing domains are assumed. This is the case since, in both cases, the r-connection is not necessarily present in the ‘root world’.
For the termination condition in Line 7, we take the following definition of periodicity. Definition 12. A trace ( ; E; R) together with a mapping Q is called periodic at (i; j) if = (d0; w0) (dn; wn), i < j, di = dj = dn, and Q(di; wi) = Q(dj ; wj ). This means that during the evolution of element d = di = dj , we find two different worlds wi, wj such that d has the same type in wi and wj . We can stop expanding worlds appearing after wj since their behavior is already captured by the successors of wi. If a trace periodic at (i; j) is found, we add an edge (wj 1; wi) to E reflecting the periodic behavior, see Line 8. Then, in truncate, the trace is shortened to (d0; w0) (dj 1; wj 1) and the relations E and R(r), r 2 ROL, and the mappings Q; Qcert; QA2 are restricted to those d and w that appear in the shortened trace. Lemma 13. On every input T ; A; B, Alg. 1 terminates and returns true iff T j= AvB. For termination, consider a trace with suffix (d; w1) (d; wn) and let A1; : : : ; An be the concept names such that E3Ai lead to wi, see Line 17 of Alg. 1. It is not difficult to show that if Ai = Aj for i < j, then Q(d; wi) Q(d; wj ) after application of complete. Since Q(d; w) CN, there are no infinite (strictly) increasing sequences. Hence, the expansion in Lines 17ff. will not indefinitely be applied. Also, the expansion in Lines 13ff. stops due to acyclicity of the TBox. Together, this guarantees termination.
Correctness is shown similar to Lemma 7. For “)”, we show that every trace together with the labeling so far computed in Q can be embedded into every model of A and T . For “(”, we present a model of T witnessing T 6j= A v B.
We finish the proof of Theorem 9 by noting that the termination argument indeed yields a polynomial bound on the length of the traces encountered by Alg. 1. (d1;w1) (d1;w2)
E r (d0;w0) E (d0;w1)
B B1 r r r
A A1
B
B B1;B r r r
A;A1 A1 A1 Fig. 4. An example trace and the induced structure
Local Roles and Rigid Concepts One can easily extend the above algorithms so as to deal with local roles. In fact, e.g., in Section 5 only B4 below needs to be added to the BACKWARD-rules in Figure 3. Note that F2 is only applied to rigid roles and C2 is therefore not applied to local ones. Clearly, the algorithm in Section 6 can be extended with a similar rule. B4 If A 2 Q(B; w), A 9r:A0, B0 2 Q(A0; A0A0), B00 9r:B0 2 T , add B00 to Q(B; w) RC If B 2 Q(A; w), B 2 CNrig, then add B to Q(A; w0), 8w0 2 W R13 If B 2 Q(d; w) or B 2 QA2(d; w) & B 2 CNrig, then add B to Qcert(d) A rigid concept has a constant interpretation over time. In the first example of Section 1, the concept Disorder should be rigid because we regard medical knowledge as static. PatientWithDisorder should be local because a disease history has begin and end.
In the presence of general TBoxes, rigid concepts can be simulated by rigid roles: replace each rigid concept name A with 9rA:>, where rA is a fresh rigid role. Alas, this simulation does not work in the context of acyclic TBoxes: the result of replacing A with 9rA:> in a CD A D is no longer a CD. Still, our algorithms can be extended, without increasing the complexity, to consider rigid concepts: e.g., the algorithm in Section 5 can be extended by adding RC above to the FORWARD and BACKWARD rules – CNrig denotes the set of rigid concepts occurring in the input TBox. Note that the intermediate phase remains the same, i.e., rules C1 and C2 are neither extended nor modified.
Rigid concepts can analogously be included in Section 6 by adding a new rule R13 above (recall: intuitively, Qcert(d) contains the concepts that hold for d in any world).
In the empty TBox case rigid roles can again simulate rigid concepts as above. 8
Conclusions and Future Work We have initiated the investigation of TDLs based on EL allowing for rigid roles and restricted TBoxes. We indeed achieved our main goal: we identified fragments of the combination of CTL and EL that have elementary, some even polynomial, complexity.
One important conclusion is that the use of acyclic TBoxes, instead of general ones, allows to design TDLs based on EL with dramatically better complexity than the ALC variant; e.g., for the fragment allowing only E the complexity drops from nonelementary to PTIME. As an important byproduct, the studied fragments of CTLEL can be seen as positive fragments of product modal logics with elementary complexity, e.g., implication for the positive fragment of K K is in PTIME.
TBoxes, e.g., consider non-convex fragments, such as CTLEEL ;E3EL, woritaht(cal)acsyscicliaclT(cByocxliecs).
Next, we plan to look at more expressive fragments of CTL We plan to incorporate temporal roles, too. It is also worth exploring how restricting TBoxes can help tame other TDLs with bad computational behavior over general TBoxes, such as TDLs based on LTL or the -calculus. We believe that the LTL case is technically easier than ours since it does not have the extra ‘ 12 -dimension’ introduced by branching. Acknowledgements The first author was supported by the M8 PostDoc Initiative project TS-OBDA and the second one by the DFG project LU1417/1-1. We thank the anonymous reviewers for their detailed and constructive suggestions.