=Paper=
{{Paper
|id=Vol-1350/paper-23
|storemode=property
|title=The
Complexity of Temporal Description Logics with Rigid Roles and
Restricted TBoxes: In Quest of Saving a Troublesome Marriage
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-23.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/Gutierrez-Basulto15
}}
==The
Complexity of Temporal Description Logics with Rigid Roles and
Restricted TBoxes: In Quest of Saving a Troublesome Marriage==
https://ceur-ws.org/Vol-1350/paper-23.pdf
The Complexity of Temporal Description Logics
with Rigid Roles and Restricted TBoxes:
In Quest of Saving a Troublesome Marriage
Vı́ctor Gutiérrez-Basulto, Jean Christoph Jung, and Thomas Schneider
Department of Computer Science, Universität Bremen
{victor,jeanjung,ts}@cs.uni-bremen.de
1 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 S NOMED CT and FMA [9], and the gene
ontology (GO) [20]. A natural task is to model dynamic knowledge about patient
histories against static medical knowledge (e.g., about diseases): e.g., the temporal
concept C := E3∃ requiresTransfusion.> describes a patient who may need a blood
transfusion in the future, and the axiom Anemic v C says that this applies to anemic
people. In contrast, Anemia v Disorder represents static knowledge.
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 [19, 11, 17]. The combination allows various
design choices, e.g., we can restrict the scope of temporal operators to certain types
of entities (such as concepts, roles, axioms), or declare some DL concepts or roles as
rigid, meaning that their interpretation will not change over time. The need for rigid
roles in TDL applications, e.g., in biomedical ontologies to accurately capture life-time
relations, has been identified [7]. For example, the role hasBloodType should be rigid
since a human’s blood type does not change during their lifetime.
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 [11, 15]. This is the case even if we severely
restrict the temporal operators available and use the sub-Boolean DL EL, whose standard
reasoning problems are tractable, instead of ALC [1, 15]. In the light of these results,
several efforts have been devoted to design decidable TDLs with rigid roles [3, 2]; e.g.,
decidability can be recovered by using a lightweight DL component based on DL-Lite.
Both the EL and DL-Lite families underlie prominent profiles of the OWL standard.
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 [3, 13, 15].
2
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 S NOMED 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 PT IME with one of the two operators, and CO NP-complete with both. To this aim, we
employ canonical models, together with expansion vectors [16] in the case with both
E3, E . Next, we lift the PT IME upper bound to the case of acyclic TBoxes, employing
a completion algorithm in the style of those for EL and extensions, [5]. Finally, we show
that the combination of E3 with A2 (“always globally”) and acyclic TBoxes leads to
a PS PACE-complete TDL, again employing a completion algorithm. An overview of
existing and new results is given in Table 1, where CTLYX denotes the combination of
the DL X with the fragment of CTL restricted to the temporal operators Y . In particular,
all the new results hold even if rigid concepts are also included.
Rigid roles? no yes yes yes
TBoxes general general acyclic empty
CTLALC =E XP T IME [13] undecidable [15] nonelementary, nonelem.,
decidable (1) decidable (1)
CTLE3
EL ≤PT IME [13] nonelementary [15] ≤PT IME (6) ≤PT IME (6)
CTLE
EL
◦ ≤PT IME [13] undecidable [15] ≤PT IME (6) ≤PT IME (6)
CTLE ◦,E3
=E XP T IME [13, 15] undecidable [15] ≥CO NP, (2) =CO NP (2)
EL
≤CO NE XP T IME (5)
CTLE3,A2
EL =PS PACE [13] nonelementary [15] =PS PACE (9) ≤PS PACE (9)
Table 1. Previous and new complexity results. ≥ hardness, ≤ membership, = completeness.
(n) refers to our Theorem or Corollary n.
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 [15]. With the restriction to acyclic
TBoxes, we will thus identify the first computationally well-behaved TDLs with rigid
roles based on EL and classical temporal logics.
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: Nrig loc
C and NC of rigid concept
3
names and local concept names, respectively; and, Nrig loc
R and NR of rigid role names and
local role names, respectively. CTLALC -concepts C are defined by the grammar
C := > | A | ¬C | C u D | ∃r.C | E C | E2C | E(CUD)
where A ranges over NC , r over NR . We use standard DL abbreviations [6] and temporal
abbreviations E3C, A2C, A3C and A(C U D) [10].
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 ∈ NC to a subset AI ⊆ ∆ and each r ∈ NR to
a binary relation rI ⊆ ∆ × ∆. The semantics of CTLALC is given in terms of temporal
interpretations based on infinite trees [15]: A temporal interpretation based on an infinite
tree T = (W, E) is a structure I = (T, (Iw )w∈W ) such that, for each w ∈ W , Iw is a
DL interpretation with domain ∆; and, rIw = rIw0 and AIw = AIw0 for all r ∈ Nrig R ,
A ∈ Nrig
C and w, w 0
∈ W . We usually write A I,w
instead of A Iw
. The stipulation that
all worlds share the same domain is called the constant domain assumption (CDA). For
Boolean-complete TDLs, CDA is the most general: increasing, decreasing and varying
domains can all be reduced to it [11, Prop. 3.32]. For the sub-Boolean logics studied
here, CDA is not w.l.o.g. Indeed, we identify a logic in which reasoning with increasing
domains cannot be reduced to the constant domain case.
We now define the semantics of CTLALC -concepts. A path in T = (W, E) starting
at a node w is an infinite sequence π = w0 w1 w2 · · · with w0 = w and (wi , wi+1 ) ∈ 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 = ∆ (C u D)I,w = C I,w ∩ DI,w
I,w
(∃r.C) = {d ∈ ∆ | ∃e . (d, e) ∈ rI,w ∧ e ∈ C I,w }
(E C)I,w = {d | ∃π ∈ Paths(w) . d ∈ C I,π[1] }
(E2C)I,w = {d | ∃π ∈ Paths(w) . ∀j ≥ 0 . d ∈ C I,π[j] }
(E(CUD))I,w = {d | ∃π ∈ Paths(w) . ∃j ≥ 0 . (d ∈ DI,π[j] ∧ (∀k < j . d ∈ C I,π[k] ))}
An acyclic CTLALC -TBox T is a finite set of concept definitions (CDs) A ≡ D with
A ∈ NC and D a CTLALC concept, such that (1) no two CDs have the same left-hand
side, and (2) there are no CDs A1 ≡ C1 , . . . , Ak ≡ Ck in T such that Ai+1 occurs in
Ci for 1 ≤ i ≤ k, where Ak+1 = A1 .
A temporal interpretation I is a model of a concept C if C I,ε 6= ∅; it is a model of an
acyclic TBox T , written I |= T , if AI,w = C I,w for all A ≡ C ∈ T and w ∈ W ; it is a
model of a concept inclusion C v D, written I |= C v D, if C I,w ⊆ DI,w for all w ∈ 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 |= C v D, if I |= C v D for all models I of T . If T is empty, we write |= 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
4
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 [12]. Indeed, the fragment of CTLALC allowing
E3 (E ) as the only temporal operator is a notational variant of S4×K (K×K) [15].
Theorem 1. Concept satisfiability relative to acyclic and empty TBoxes for CTLALC
with rigid roles is decidable and 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, ∀r.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 CTLE◦,E3 relative to the Empty TBox
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 CO NP-complete for
CTLE ◦,E3 with rigid roles and in PT IME for CTLE◦ and CTLE3 with rigid roles.
EL EL EL
CO NP-hardness is obtained by embedding EL plus transitive closure into CTLEL
◦
E ,E3
;
the jump in complexity comes from the ability to express disjunctions, e.g., |= E3C v
C t E E3C. We next explain CO NP-membership; the PT IME results are a byproduct
and improved later.
We proceed in two steps: first we provide a characterization of |= C v D where C is an
◦ E◦,E3
CTLE EL -concept and D an CTLEL -concept. Next we generalize this characterization
E◦,E3
to CTLEL -concepts C.
Given a CTLE ◦
EL -concept C, the description tree tC = (VC , LC , EC ) for C is a
labeled graph corresponding to C’s syntax tree; we denote its root by xC . For example,
if C = E (∃r.A u ∃s.B), then tC is given in Figure 1, left.
For plain EL, we have |= C v D if and only if there is a homomorphism from tD
to tC , which can be tested in polynomial time [8]. This criterion cannot directly be
transferred to CTLE ◦
EL because tC does not explicitly represent all pairs of worlds and
domain elements whose existence is implied by tC , e.g., for |= E ∃r.A v ∃r.E A
with r rigid, there is no homomorphism from tD to tC . We overcome this problem
by transforming tC into a canonical model IC of C, i.e., (1) its distinguished root is
an instance of C and (2) IC homomorphically embeds into every model of C. The
5
◦
r A r A
r s s B s B
A B
..
tC . IC Ipre
C
Fig. 1. Description tree tC , canonical model IC , finite representation Ipre
C for C = E (∃r.A u ∃s.B)
construction of IC from tC is straightforward: for every node with an incoming -edge
(r-edge, r being a role) create a fresh world (domain element); for the root xC create
both a world and domain element. The temporal relation and the interpretation of r and
concept names is read off EC and LC . To transform (W, R) into an infinite tree, we add
an infinite path of fresh worlds to every world without R-successor. The canonical model
for the above concept C is shown in Fig. 1, center; the infinite path of worlds is dashed.
From (1), (2), and the preservation properties of homomorphisms, we obtain:
◦ E◦,E3
Lemma 3. For all CTLE EL -concepts C and all CTLEL -concepts D, we have |=
IC ,xC
C v D if and only if xC ∈ D .
Now xC ∈ 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 Ipre pre
C into the temporal dimension, IC and IC satisfy the same concepts in their roots.
E◦
Theorem 2 for CTLEL thus follows. The CTLE3 EL part can be obtained by representing
every E3 in C by a -edge in tC and adapting the notion of a homomorphism.
For CTLE ◦,E3 , we use expansion vectors introduced in [16], applied to the temporal
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 ◦
EL -concept obtained from C
ui
by replacing the i-th occurrence of E3 with (E ) , i.e., i times E . For example, if
C = E3∃r.E3(A u E B) and U = (2, 0), then C[U ] = E E ∃r.(A u E B).
Let UmC = {(u1 , . . . , un ) | ui 6 m for all i}. 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 6|= 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 |= C v D if and only if
EL
tdepth(D)+1
|= C[U ] v D for all U ∈ UC .
Together with Lemma 3, this yields the desired polynomial-time guess-and-check proce-
dure for deciding |= C v D.
6
5 CTLE◦ E3
EL and CTLEL relative to Acyclic TBoxes
The results of Theorem 2 transfer to acyclic TBoxes with an exponential blowup due to
unfolding [18], that is:
Corollary 5. Concept subsumption relative to acyclic CTLE ◦,E3 -TBoxes with rigid
EL
roles is in CO NE XP T IME.
For the subfragments CTLE ◦ E3
EL and CTLEL , we can even show polynomial complexity:
Theorem 6. Concept subsumption relative to acyclic CTLE ◦ E3
EL - and CTLEL -TBoxes with
rigid roles is in PT IME.
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 ≡ ∃r.A1 , where Ai ∈ NC ∪ {>} and r ∈ NR . As usual, a subsumption-equivalent
TBox in NF can be computed in polynomial time [4]. We use CN and ROL to denote the
sets of concept names and roles occurring in T .
To prove a PT IME upper bound, we devise a completion algorithm in the style
of those known for EL and (two-dimensional) extensions, cf. [5, 14], which build an
abstract representation of the ‘minimal’ model of the input TBox T (in the sense of
Horn logic). The main difficulty is that different occurrences of the same concept name
in the TBox cannot all be treated uniformly (as it is the case for, say, EL), due to the
two-dimensional semantics. Instead, we have to carefully choose witnesses for E3A and
∃r.A, respectively. Our algorithm constructs a graph G = (W, E, Q, R) based on a set
W , a binary relation E, a mapping Q that associates with each A ∈ CN and each w ∈ W
a subset Q(A, w) ⊆ CN, and a mapping R that associates with each rigid role r ∈ ROL
r
a relation R(r) ⊆ CN × W × CN × W . For brevity, we write (A, w) → (B, w0 ) instead
of (A, w, B, w0 ) ∈ R(r) and denote with E ∗ the reflexive, transitive closure of E.
The algorithm for deciding subsumption initializes G as follows. For all r ∈ ROL, set
R(r) = ∅. Set W = CN×CN∪{E3A | A ∈ CN}. Set E = {(E3A, AA), (AB, A>) |
A, B ∈ CN}. For all A ∈ CN, set Q(A, w) = {>, B} if w = AB and Q(A, w) = {>}
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 |= 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., B 0 ∈ Q(A, AB) implies
T |= A u E3B v E3(B u B 0 ).
After initialization, the algorithm extends G by applying the completion rules de-
picted in Figure 2 in three phases. In the first phase – also called F ORWARD-phase, since
definitions A ≡ C ∈ 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 witness-
existentials as demanded. Most notably, rule F2 introduces a pointer to the structure
representing the temporal evolution of an instance of B 0 .
7
F1 If B ∈ Q(A, AA0 ) & B ≡ E3B 0 ∈ T , then add (AA0, AB 0 ) to E
r
F2 If B ∈ Q(A, w) and B ≡ ∃r.B 0 ∈ T , then set (A, w) → (B 0 , B 0 B 0 )
F3 If B ∈ Q(A, w) & B ≡ A1 uA2 ∈ T , then add A1 ,A2 to Q(A, w)
r
C1 If (BB, w) ∈ E and (A, w0 ) → (B, BB), then add (w0, w) to E
r
C2 If (A, w) → (B, BB), then
r
a) (A, w0 ) → (B, E3B) for all w0 6= w with (w0, w) ∈ E ∗
r
b) (A, w0 ) → (B, w0 ) for all w0 with (w0 , w) ∈
/ E∗
B1 If B ∈ Q(A, w), (w0 , w) ∈ E ∗ , and A0 ≡ E3B ∈ T , then add A0 to Q(A, w0 )
r
B2 If A ∈ Q(B, w), (A0 , w0 ) → (B, w), and A00 ≡ ∃r.A ∈ T then add A00 to Q(A0 , w0 )
B3 If A1 , A2 ∈ Q(B, w) & A ≡ A1 u A2 ∈ T then add A to Q(B, w)
Fig. 2. Completion rules
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 ∈ T are
read as A w C. This separation into a F ORWARD 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.
Lemma 7. Let T be an acyclic CTLE3 EL -TBox in normal form. Then for all A, B ∈ CN,
we have T |= A v B iff, after exhaustive rule application, B ∈ Q(A, AA).
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 ∈ AI,w \ B I,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 ∈ W with E k A, 1 ≤ k ≤ |T | to capture what
is implied by E k A; more precisely, B 0 ∈ Q(A, E k A) implies T |= E k A v B 0 ,
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 {E3} indeed leads to PS PACE-hardness.
Theorem 8. Concept subsumption relative to acyclic CTLE ◦ E3
EL - and CTLEL -TBoxes with
rigid roles and increasing domains is PS PACE-hard.
8
6 CTLE3,A2
EL relative to Acyclic TBoxes
We now add A2 and observe an increase in complexity over acyclic TBoxes.
Theorem 9. Concept subsumption relative to acyclic CTLE3,A2
EL -TBoxes with rigid
roles is PS PACE-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 ≡ ∃r.A1 , where Ai ∈ NC ∪ {>} and r ∈ 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 ) ∈
E. (2) wi = wi+1 and (di , di+1 ) ∈ R(r) for some r ∈ ROL.
Intuitively, traces represent paths
Algorithm 1: Subsumption in CTLE3,A2 EL
through temporal interpretations,
which in each step follow either Input: Acyclic TBox T , concept names A, B
Output: true if T |= A v B, false otherwise
the temporal relation (Def. 10, 1)
or a DL relation r (2); so, in a pair 1 σ := (d0 , w0 ); Q(d0 , w0 ) := {A, >};
(d, w), d can be thought of as a 2 E := ∅; R(r) := ∅ for all r ∈ ROL;
3 expand(σ, E, R);
domain element and w as a world.
4 return true if B ∈Q(d0 ,w0 ), false otherwise;
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);
11 return;
as the basis for inducing a richer
12 (d, w) := last element of σ;
structure that conforms with the
constant domain assumption and 13 foreach A ∈ Q(d, w) with A ≡ ∃r.B ∈ T do
14 Q(d0 , w) = {B, >} for a fresh d0 ;
captures rigidity; see Example 11
15 add (d, d0 ) to R(r);
below. The algorithm also main-
16 expand (σ · (d0 , w), E, R);
tains an additional mapping Q that
17 foreach A ∈ Q(d, w) with A ≡ E3B ∈ T do
labels each point (d, w) of the
18 Q(d, w0 ) = {B, >} for a fresh w0 ;
trace (and all the induced points) 19 add (w, w0 ) to E;
with a set Q(d, w) ⊆ CN. The 20 expand (σ · (d, w0 ), E, R);
set Q(d, w) captures all concept
names that are satisfied in the minimal model at points represented by (d, w).
9
R1 If A ≡ A1 u A2 ∈ T and A ∈ Q∗ (·), then add A1 , A2 to Q∗ (·)
R2 If A ≡ A1 u A2 ∈ T and A1 , A2 ∈ Q∗ (·), then add A to Q∗ (·)
R3 If (d, d0 ) ∈ R(r), B ∈ Q(d0 , w), A ≡ ∃r.B ∈ T , then add A to Q(d, w)
R4 If B ∈ Q(d, w), (w0 , w) ∈ E ∗ , A ≡ E3B ∈ T , then add A to Q(d, w0 )
R5 If B ∈ Q(d, w), (w, w0 ) ∈ E ∗ , B ≡ A2A ∈ T , then add B, A to Q(d, w0 )
R6 If (d, d0 ) ∈ R(r), B ∈ Qcert (d0 ), A ≡ ∃r.B ∈ T , then add A to Qcert (d)
R7 If B ∈ Qcert (d), A ≡ A2B ∈ T , then add A to Qcert (d)
R8 If B ∈ Qcert (d), then add B to Q(d, w) for all w
R9 If B ∈ QA2 (d, w), A ≡ A2B ∈ T , add A to Q(d, w)
R10 If A ∈ Q(d, w), A ≡ A2B ∈ T , add A, B to QA2 (d, w)
R11 If (d, d0 ) ∈ R(r), B ∈ QA2 (d0 , w), A ≡ ∃r.B ∈ T , then add A to QA2 (d, w)
R12 If A ∈ QA2 (d, w), A ≡ E3B ∈ T , w0 added due to
A ∈ Q(d, w) in Line 18, B 0 ∈ Q(d, w0 ), A0 ≡ E3B 0 ∈ T , then add A0 to QA2 (d, w)
Fig. 3. Saturation rules. In R1, R2 the set Q∗ (·) ranges over all Q(d, w), Qcert (d), and 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 ∃r.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 {>}, 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, |= ∃r.A2B v A2∃r.B.
10
Example 11. Let T = {A ≡ E3A1 , A1 ≡ ∃r.B, B ≡ E3A1 } be the input TBox; and
T |= A v A1 is to be checked. Figure 4 (left) shows the trace initiated at (d0 , w0 )
with Q(d0 , w0 ) = {>, A}, 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 |= A v A1 indeed holds. Furthermore, note that T 6|= 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 reflect-
ing 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 ∈ 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 |= 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 6|= 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.
(d0 ,w0 ) A B A,A1
r r
E
(d1 ,w1 ) (d0 ,w1 ) B A1 B A1
r r r
E
(d1 ,w2 ) B1 B1 ,B A1
r r
Fig. 4. An example trace and the induced structure
11
7 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 ∈ Q(B, w), A ≡ ∃r.A0 , B 0 ∈ Q(A0 , A0 A0 ), B 00 ≡ ∃r.B 0 ∈ T , add B 00 to Q(B, w)
RC If B ∈ Q(A, w), B ∈ CNrig , then add B to Q(A, w0 ), ∀w0 ∈ W
R13 If B ∈ Q(d, w) or B ∈ QA2 (d, w) & B ∈ 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 ∃rA .>, 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
∃rA .> 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 F ORWARD 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 PT IME. 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 PT IME.
Next, we plan to look at more expressive fragments of CTLEL or at classical (cyclic)
TBoxes, e.g., consider non-convex fragments, such as CTLE ◦,E3 , with (a)cyclic TBoxes.
EL
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.
12
References
1. Artale, A., Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporalising tractable
description logics. In: Proc. TIME (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
(2014)
3. Artale, A., Lutz, C., Toman, D.: A description logic of change. In: Proc. IJCAI (2007)
4. Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proc.
IJCAI (2003)
5. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. IJCAI (2005)
6. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The De-
scription Logic Handbook: Theory, Implementation, and Applications. Cambridge University
Press (2003)
7. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. In: Proc. KR (2008)
8. Baader, F., Küsters, R., Molitor, R.: Computing least common subsumers in description logics
with existential restrictions. In: Proc. IJCAI (1999)
9. Bodenreider, O., Zhang, S.: Comparing the representation of anatomy in the FMA and
S NOMED CT. In: Proc. AMIA (2006)
10. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
11. Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics:
theory and applications, Studies in Logic, vol. 148. Elsevier (2003)
12. Göller, S., Jung, J.C., Lohrey, M.: The complexity of decomposing modal and first-order
theories. ACM Trans. Comput. Log. 16(1), 9:1–9:43 (2015)
13. Gutiérrez-Basulto, V., Jung, J.C., Lutz, C.: Complexity of branching temporal description
logics. In: Proc. ECAI (2012)
14. Gutiérrez-Basulto, V., Jung, J.C., Lutz, C., Schröder, L.: A closer look at the probabilistic
description logic Prob-EL. In: Proc. AAAI (2011)
15. Gutiérrez-Basulto, V., Jung, J.C., Schneider, T.: Lightweight description logics and branching
time: a troublesome marriage. In: Proc. KR (2014)
16. Haase, C., Lutz, C.: Complexity of subsumption in the EL family of description logics:
Acyclic and cyclic TBoxes. In: Proc. ECAI (2008)
17. Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey. In: Proc.
TIME (2008)
18. Nebel, B.: Terminological reasoning is inherently intractable. Artif. Intell. 43(2), 235–249
(1990)
19. Schild, K.: Combining terminological logics with tense logic. In: Proc. EPIA (1993)
20. The Gene Ontology Consortium: Gene ontology: Tool for the unification of biology. Nature
Genetics 25, 25–29 (2000)