In contrast to qualitative linear temporal logics, which can be used to state that some property will eventually be satisfied, metric temporal logics allow to formulate constraints on how long it may take until the property is satisfied. While most of the work on combining Description Logics (DLs) with temporal logics has concentrated on qualitative temporal logics, there has recently been a growing interest in extending this work to the quantitative case. In this paper, we complement existing results on the combination of DLs with metric temporal logics over the natural numbers by introducing interval-rigid names. This allows to state that elements in the extension of certain names stay in this extension for at least some specified amount of time.
DL-based ontologies are employed in many application areas, but they are
particularly successful in the medical domain (see, e.g., the medical ontologies Galen
and SNOMED CT1). For example, the concept of a patient with a concussion
can be expressed as Patient u ∃finding.Concussion. This example, taken from [
To overcome this problem, a great variety of temporal extensions of DLs have
been investigated.2 In the present paper, we concentrate on ALC and combine it
with a metric variant of linear temporal logic (LTL), a point-based temporal logic
over a linear flow of time. But even if these two logics are fixed, there are several
other design decisions to be made. One can either apply temporal operators only
to axioms [
In this paper, we address a shortcoming of the qualitative temporal description
logics mentioned until now. The until-operator in our example does not say
anything about how long after the concussion that examination happened. However,
the above definition of “concussion with no loss of consciousness” is only sensible
if the examination took place shortly after the concussion. Otherwise, a loss of
consciousness could also have been due to other causes. As another example, when
formulating eligibility criteria for clinical trials, one needs to express quantitative
temporal patterns [
In Section 3, we extend the logic LTLbAinLC of Section 2 with interval-rigid
names, a means of expressiveness that has not been considered before. It allows
one to state that elements belonging to a concept belong to that concept for
at least k consecutive time points, and similarly for roles. For example,
according to the WHO, patients with paucibacillary leprosy should receive MDT as
treatment for 6 consecutive months,3 which can be expressed by making the
role getMDTagainstPB rigid for 6 time points (assuming that each time point
represents one month). In Section 4, we briefly discuss results for extensions of
the logic ALC-LTL of [
ALC-LTL
LTLbAinLC
LTLALC ALC-LTLbin
Interestingly, in the presence of rigid roles, interval-rigid concepts actually cause
undecidability. Without rigid roles, the addition of interval-rigid concepts and
roles leaves the logic decidable, but in some cases increases the complexity (see
Table 2). An overview of the logics considered and their relations is shown in
Figure 1. Detailed proofs of all results can be found in [
Related Work. Apart from the above references, we want to point out work on
combining DLs with Halpern and Shoham’s interval logic [
ALC
We first introduce the description logic ALC and its metric temporal extension
LTLbAinLC [
Syntax. Let NC, NR and NI be countably infinite sets of concept names, role names, and individual names, respectively. An ALC concept is an expression given by C, D ::= A | > | ¬C | C u D | ∃r.C, where A ∈ NC and r ∈ NR. LTLbin ALC concepts extend ALC concepts with the constructors #C and C UI D, where I is an interval of the form [c1, c2] or [c1, ∞) with c1, c2 ∈ N, c1 ≤ c2, given in binary. We may use [c1, c2) to abbreviate [c1, c2 − 1], and similarly for the left endpoint. For example, A U[2,5)B u ∃r.#A is an LTLbAinLC concept.
An LTLbAinLC axiom is either a general concept inclusion (GCI) of the form C v D, or an assertion of the form C(a) or r(a, b), where C, D are LTLbin concepts, r ∈ NR, and a, b ∈ NI. LTLbAinLC formulae are expressions of the foArLmC φ, ψ ::= α | > | ¬φ | φ ∧ ψ | #φ | φ UI ψ, where α is an LTLbAinLC axiom. Semantics. A DL interpretation I = (ΔI , ·I ) over a non-empty set ΔI , called the domain, defines an interpretation function ·I that maps each concept name A ∈ NC to a subset AI of ΔI , each role name r ∈ NR to a binary relation rI on ΔI and each individual name a ∈ NI to an element aI of ΔI , such that aIi 6= bIi whenever a 6= b, a, b ∈ NI (unique name assumption). As usual, we extend the mapping ·I from concept names to ALC concepts as follows: >Ii := ΔI, (¬C)Ii := ΔI \ CIi ,
(C u D)Ii := CIi ∩ DIi , (∃r.C)Ii := {d ∈ ΔI | ∃e ∈ CIi : (d, e) ∈ rIi }.
A (temporal DL) interpretation is a structure I = (ΔI, (Ii)i∈N), where each Ii = (ΔI, ·Ii ), i ∈ N, is a DL interpretation over ΔI (constant domain assumption) and aIi = aIj for all a ∈ NI and i, j ∈ N, i.e., the interpretation of individual names is fixed. The mappings ·Ii are extended to LTLbin concepts as follows: ALC (#C)Ii := {d ∈ ΔI | d ∈ CIi+1 }, (C UI D)Ii := {d ∈ ΔI | ∃k : k − i ∈ I, d ∈ DIk , and ∀j ∈ [i, k) : d ∈ CIj }. The concept C UI D requires D to be satisfied at some point in the interval I, and C to hold at all time points before that.
The validity of an LTLbAinLC formula φ in I at time point i ∈ N (written I, i |= φ) is inductively defined as follows:
I, i |= C v D iff CIi ⊆ DIi I, i |= C(a) iff aIi ∈ CIi I, i |= r(a, b) iff (aIi , bIi ) ∈ rIi I, i |= ¬φ iff not I, i |= φ
I, i |= φ ∧ ψ iff I, i |= φ and I, i |= ψ I, i |= #φ iff I, i + 1 |= φ I, i |= φ UI ψ iff ∃k : k − i ∈ I, I, k |= ψ, and ∀j ∈ [i, k) : I, j |= φ.
As usual, we define ⊥ := ¬>, C t D := ¬(¬C u ¬D), ∀r.C := ¬(∃r.¬C),
φ ∨ ψ := ¬(¬φ ∧ ¬ψ), α U β := α U[0,∞)β, I α := > UI α, 2I α := ¬ I ¬α,
α := > U α, and 2α := ¬ ¬α, where α, β are either concepts or formulae [
ALC
holds for a given LTLbAinLC formula φ. We also consider a syntactic restriction
from [
ALC complete w.r.t. global GCIs. In LTLALC , this problem is ExpSpace-complete, and ExpTime-complete w.r.t. global GCIs.
Note that ExpSpace-completeness for LTLALC with assertions has already
been shown in [
ALC Theorem 2. Any LTL0,∞ formula can be translated in polynomial time into an equisatisfiable LTLALC fAoLrCmula.
This reduction is quite modular; for example, if the formula has only global GCIs, then this is still the case after the reduction. In fact, the reduction applies to all sublogics of LTLbAinLC that we consider in this paper. Hence, in the following we do not explicitly consider logics with the superscript ·0,∞, knowing that they have the same complexity as the corresponding temporal DLs using only U . 3
ALC
with Interval-Rigid Names In many temporal DLs, rigid names are considered, whose interpretation does not change over time. Formally, we fix a finite set NRig ⊆ NC ∪ NR of rigid concept and role names, and require interpretations I = (ΔI, (Ii)i∈N) to respect these names, in the sense that XIi = XIj holds for all X ∈ NRig and i, j ∈ N. It turns out that LTLbAinLC can already express rigid concepts via the (global) GCIs C v #C and ¬C v #¬C. The same does not hold for rigid roles, which lead to undecidability even in LTL [15, Theorem 11.1]. Hence, it is not fruitful to consider rigid names in LTALLbAiCnLC (but they are meaningful for the logics of Section 4).
To augment the expressivity of temporal DLs while avoiding undecidability, we propose interval-rigid names. In contrast to rigid names, interval-rigid names only need to remain rigid for a limited period of time. Formally, we take a finite set NIRig ⊆ (NC ∪ NR) \ NRig of interval-rigid names, and a function iRig : NIRig → N≥2. An interpretation I = (ΔI, (Ii)i∈N) respects the interval-rigid names if the following holds for all X ∈ NIRig with iRig(X) = k, and i ∈ N:
For each d ∈ XIi , there is a time point j ∈ N such that i ∈ [j, j + k) and
d ∈ XI` for all ` ∈ [j, j + k).
LTLbin 2-ExpSpace ≤ [Th. 4] 2-ExpSpace ≥ [
We investigate the complexity of satisfiability w.r.t. (interval-)rigid names
(or (interval-)rigid concepts if NIRig ⊆ NC / NRig ⊆ NC), which is defined as
before, but considers only interpretations that respect (interval-)rigid names.
Note that (interval-)rigid roles can be used to simulate (interval-)rigid concepts
via existential restrictions ∃r.> (e.g., see [
The complexity of LTLbAinLC with interval-rigid roles is harder to establish.
We first show in Section 3.1 that the general upper bound of 2-ExpSpace
still holds, by a novel quasimodel construction. For global GCIs, we show
2ExpTime-hardness in [
For the 2-ExpSpace upper bound, we extend the notion of quasimodels from [
We now formalize this intuition. Let ϕ be an LTLbAinLC formula. Denote by csub(ϕ)/fsub(ϕ)/ind(ϕ)/rol(ϕ) the set of all concepts/formulae/individuals/roles occurring in ϕ, by clc(ϕ) the closure of csub(ϕ) ∪ {C U D | C U[c,∞)D ∈ csub(ϕ)} under single negations, and likewise for clf (ϕ) and fsub(φ). A concept type for ϕ is any subset t of clc(ϕ) ∪ ind(ϕ) such that T1 ¬C ∈ t iff C 6∈ t, for all ¬C ∈ clc(ϕ); T2 C u D ∈ t iff C, D ∈ t, for all C u D ∈ clc(ϕ); and T3 t contains at most one individual name.
Similarly, we define formula types t ⊆ clf (ϕ) by the following conditions: T1’ ¬α ∈ t iff α 6∈ t, for all ¬α ∈ clf (ϕ); and T2’ α ∧ β ∈ t iff α, β ∈ t, for all α ∧ β ∈ clf (ϕ).
Intuitively, a concept type describes one domain element at a single time point, while a formula type expresses constraints on all domain elements. If a ∈ t ∩ ind(ϕ), then t describes an named element, and we call it a named type.
To put an upper bound on the time window we have to consider, we consider the largest number occurring in ϕ and iRig, and denote it by `ϕ. Then, a (concept/formula) run segment for ϕ is a sequence σ = σ(0) . . . σ(`ϕ) composed exclusively of concept or formula types, respectively, such that R1 #α ∈ σ(0) iff α ∈ σ(1), for all #α ∈ cl∗(ϕ); R2 for all a ∈ ind(ϕ) an n ∈ (0, `ϕ], we have a ∈ σ(0) iff a ∈ σ(n); R3 for all α UI β ∈ cl∗(ϕ), we have α UI β ∈ σ(0) iff (a) there is j ∈ I ∩ [0, `ϕ] such that β ∈ σ(j) and α ∈ σ(i) for all i ∈ [0, j), or (b) I is of the form [c, ∞) and α, α U β ∈ σ(i) for all i ∈ [0, `ϕ], where cl∗ is either clc or clf (as appropriate), and R2 does not apply to formula run segments. A concept run segment captures the evolution of a domain element over a sequence of `ϕ + 1 time points, and a formula run segment describes general constraints on the interpretation over a sequence of `ϕ + 1 time points.
The evolution over the complete time line is captured by (concept/formula) runs for ϕ, which are infinite sequences r = r(0)r(1) . . . such that each subsequence of length `ϕ + 1 is a (concept/formula) run segment, and additionally R4 α U[c,∞)β ∈ r(n) implies that there is j ≥ n + c such that β ∈ r(j) and α ∈ r(i) for all i ∈ [n, j). A concept run (segment) is named if it contains only (equivalently, any) named types. We may write ra (σa) to denote a run (segment) that contains an individual name a. For a run (segment) σ, we write σ>i for the subsequence of σ starting at i + 1, σ<i for the one stopping at i − 1, and σ[i,j] for σ(i) . . . σ(j).
As we cannot explicitly represent infinite runs, we use run segments to construct them step-by-step. For this, it is important that a set of concept runs (segments) can be composed into a coherent model. In particular, we have to take care of (interval-rigid) role connections. A role constraint for ϕ is a tuple (σ, σ0, s, k), with concept run segments σ, σ0, s ∈ rol(ϕ), k ∈ [1, iRig(s)], such that C1 {¬C | ¬∃s.C ∈ σ(0)} ⊆ σ0(0); and C2 if σ0 is named, then σ is also named.
We write σ ks σ0 as a shorthand for the role constraint (σ, σ0, s, k). Intuitively, σ ks σ0 means that the domain elements described by σ(0), σ0(0) are connected by the role s at the current time point, and also at the k − 1 previous time points. In this case, we need to ensure that these elements stay connected for at least the following iRig(s) − k time points. Condition C1 ensures that, if σ(0) cannot have any s-successors that satisfy C, then σ0(0) does not satisfy C.
We can now describe the behaviour of a whole interpretation and its elements at a single time point, together with some bounded information about the future (up to `ϕ time points). A quasistate for ϕ is a pair Q = (RQ, CQ), where RQ is a set of run segments and CQ a set of role constraints over RQ such that Q1 RQ contains exactly one formula run segment σQ; Q2 RQ contains exactly one named run segment σa for each a ∈ ind(ϕ); Q3 for all C v D ∈ clf (ϕ), we have C v D ∈ σQ(0) iff C ∈ σ(0) implies D ∈ σ(0) for all concept run segments σ ∈ RQ; Q4 for all C(a) ∈ clf (ϕ), we have C(a) ∈ σQ(0) iff C ∈ σa(0); Q5 for all s(a, b) ∈ clf (ϕ), we have s(a, b) ∈ σQ(0) iff σa ks σb ∈ CQ for some k ∈ [1, iRig(s)]; and Q6 for all σ ∈ RQ and ∃s.D ∈ σ(0), there is σ ks σ0 ∈ CQ with D ∈ σ0(0) and k ∈ [1, iRig(s)].
We next capture when quasistates can be connected coherently to an infinite sequence. A pair (Q, Q0) of quasistates is compatible if there is a compatibility relation π ⊆ RQ × RQ0 such that C3 every run segment in RQ and RQ0 occurs at least once in the domain and range of π, respectively; C4 each pair (σ, σ0) ∈ π satisfies σ>0 = σ0<`ϕ ; C5 for all (σ1, σ10) ∈ π and σ1 ks σ2 ∈ Q with k < iRig(s), there is σ10 k +s1 σ20 ∈ Q0 with (σ2, σ20) ∈ π; and C6 for all (σ1, σ10) ∈ π and σ10 k +s1 σ20 ∈ Q0 with k > 1, there is σ1 ks σ2 ∈ Q with (σ2, σ20) ∈ π.
Such a relation makes sure that we can combine run segments of consecutive quasistates such that the interval-rigid roles are respected. Note that the unique
Q0 formula run segments must be matched to each other, and likewise for the named run segments. Moreover, the set of all compatibility relations for a pair of quasistates (Q, Q0) is closed under union, which means that compatible quasistates always have a unique maximal compatibility relation (w.r.t. set inclusion).
To illustrate this, consider Figure 2, showing a sequence of pairwise compatible quasistates, each containing two run segments. Here, `ϕ = iRig(s) = 3. The relations π0, π1, and π2 satisfy Conditions C3–C6, which, together with C1 and C2, ensure that a run going through the types t1, t2, t3, and t4 can be connected to another run via the role s for at least 3 consecutive time points.
Finally, a quasimodel for ϕ is a pair (S, R), where S is an infinite sequence of compatible quasistates S(0)S(1) . . . and R is a non-empty set of runs, such that M1 the runs in R are of the form σ0(0)σ1(0)σ2(0) . . . such that, for every i ∈ N, we have (σi, σi+1) ∈ πi, where πi is the maximal compatibility relation for the pair (S(i), S(i + 1)); M2 for every σ ∈ RS(i), there exists a run r ∈ R with r[i,i+`ϕ] = σ; M3 every role constraint in S(0) is of the form σ1 1s σ2; and M4 ϕ ∈ σS(0)(0).
By M1, the runs σ0(0)σ1(0)σ2(0) . . . always contain the whole run segments σ0, σ1, σ2, . . . , since we have σ1(0) = σ0(1), σ2(0) = σ0(2), and so on. Moreover, R always contains exactly one formula run and one named run for each a ∈ ind(ϕ).
We can show that every quasimodel describes a satisfying interpretation for ϕ and, conversely, that every such interpretation can be abstracted to a quasimodel. Moreover, one can always find a quasimodel of a regular shape.
Lemma 3. An LTLbin formula ϕ is satisfiable w.r.t. interval-rigid names iff ϕ
ALC has a quasimodel (S, R) in which S is of the form
S(0) . . . S(n)(S(n + 1) . . . S(n + m))ω, where n and m are bounded triple exponentially in the size of ϕ and iRig.
This allows us to devise a non-deterministic 2-ExpSpace algorithm that decides satisfiability of a given LTLbin formula. Namely, we first guess n and m,
ALC
and then the quasistates S(0), . . . , S(n + m) one after the other. To show that
this sequence corresponds to a quasimodel as in Lemma 3, note that only three
quasistates have to be kept in memory at any time, the sizes of which are double
exponentially bounded in the size of the input: the current quasistate, the next
quasistate, and the first repeating quasistate S(n + 1). 2-ExpSpace-hardness
holds already for the case without interval-rigid names or assertions [
ALC with respect to interval-rigid names is 2-ExpSpace-complete. 3.2
For LTLbin
ALC formulae with global GCIs, we show a tight (2-ExpTime) complexity bound only if we consider a modified temporal semantics that uses Z instead of N. Over Z, every satisfiable formula has a quasimodel in which the unnamed run segments and role constraints are the same for all quasisates. This is not the case for N, since then a quasistate at time point 1 can have role constraints σ ks σ0 with k > 1, whereas one at time point 0 cannot (see M3).
Hence, interpretations are now of the form I = (ΔI, (Ii)i∈Z), where ΔI is a constant domain and Ii are classical DL interpretations, as before. Recall that an LTLbAinLC formula with global GCIs is of the form 2T ∧φ, where T is a conjunction of GCIs and φ is an LTLbAinLC formula that does not contain GCIs. In order to enforce our GCIs on the whole time line (including the time points before 0), we replace 2T with 2+− in that definition, where 2+T expresses that in all models − I, I, i |= T for all i ∈ Z. We furthermore slightly adapt some of the notions introduced in Section 3.1. First, to ensure that GCIs hold on the whole time line, we require (in addition to T1’ and T2’) that all formula types contain all GCIs from T . Additionally, we adapt the notions of runs . . . r(−1)r(0)r(1) . . . and sequences . . . S(−1)S(0)S(1) . . . of quasistates to be infinite in both directions. Hence, we can now drop Condition M3, reflecting the fact that, over Z, role connections can exist before time point 0. All other definitions remain unchanged.
The proof follows a similar idea as in the last section. We first show that every formula is satisfiable iff it has a quasimodel of a regular shape, which now is also constant in its unnamed part, in the sense that, if unnamed run segments and role constraints occur in S(i), then they also occur in S(j), for all i, j ∈ Z. This allows us to devise an elimination procedure (in the spirit of [17, Theorem 3] and [14, Theorem 2]), with the difference that we eliminate run segments and role constraints instead of types, which gives us a 2-ExpTime upper bound. Theorem 5. Satisfiability in LTLbin
ALC w.r.t. interval-rigid names and global GCIs over Z is 2-ExpTime-complete. 4
Metric Extensions of ALC-LTL
We briefly summarize results that we have obtained for the sublogic ALC-LTLbin
of LTLbin , which does not allow temporal operators within concepts (cf. [
ALC
Due to lack of space, we refer the reader to [
ALC
and rigid roles do not lead to undecidability [
Known and new complexity results are compared in Tables 2 and 3 for ALCLTLbin with and without interval-rigid names, respectively. In the presence of interval-rigid names, we obtain several hardness results already for ALC-LTL, based on the insight that interval-rigid concepts can express the operator # on the concept level. In particular, the combination of rigid roles with interval-rigid concepts already leads to undecidability. If interval-rigid names are disallowed, the complexity of satisfiability in ALC-LTLbin corresponds to the maximum of the complexities of satisfiability in ALC-LTL and LTLbin. 5
We investigated a series of extensions of LTLALC and ALC-LTL with
intervalrigid names and metric temporal operators, with complexity results ranging
from ExpTime to 2-ExpSpace. Some cases were left open, such as the precise
complexity of LTLbAinLC with global GCIs, for which we have a partial result
for the temporal semantics based on Z. Nevertheless, this paper provides a
comprehensive guide to the complexities faced by applications that want to
combine ontological reasoning with quantitative temporal logics. For future work,
it would be interesting to extend temporal DLs based on light-weight logics such
as DL-Lite and EL [