In this paper we use automata-theoretic techniques to tightly characterize the worst-case complexity of the knowledge base satisfiability problem for the very expressive Description Logics (DLs) ALCQIbr+eg and S RIQ. The logic ALCQIbr+eg extends ALC with qualified number restrictions, inverse roles, safe Boolean role expressions, regular expressions over roles, and concepts of the form ∃P.Self in the style of S RIQ, a well known DL closely related to the new Semantic Web Standard OWL 2. By reducing its knowledge base satisfiability problem to the emptiness test of an automaton on infinite trees, we show that all these additions do not increase the worst case complexity of ALC and provide a decision procedure for one of the most expressive DLs that have been shown to be decidable in exponential time. We also close the open question of the precise complexity of reasoning in S RIQ, exploiting a reduction from the S RIQ knowledge base satisfiability problem into the ALCQIbr+eg one.
Introduction
non-deterministic double exponential time even in the restricted case of SHIQ KBs. For
SROIQ, an optimal 2NEXPTIME upper bound could be established by reducing it (with an
exponential blow-up) to the two variable fragment of First Order Logic with counting, but the
tight complexity of SRIQ remained open [
In this paper, we introduce an extension of the logic ALCQIbreg previously considered
in [
As we show in this paper, the ALCQIbr+eg knowledge base satisfiability problem allows
for an elegant reduction to the emptiness test of an automaton on infinite trees. The reduction
builds on [
The paper is organized as follows. In Section 2, after introducing the syntax and semantics
of ALCQIbr+eg knowledge bases, we define their syntactic closure, introduce a normal form
for them and a canonical form for their models. These allow us to extend the automata
algorithm of [
The DL ALCQIb+
reg
We introduce the syntax and semantics of the DL ALCQIbr+eg , a natural extension of
ALCQIbreg [
According to the following syntax, we define (ALCQIbr+eg ) concepts C, C′, atomic roles Q, simple roles S, S′, and roles R, R′, where A ∈ C, P ∈ R and P 6= T.
C, C′ −→ A | ¬C | C ⊓ C′ | C ⊔ C′ | ∀R.C | ∃R.C |> n S.C |6 n S.C | ∃S.Self
Q −→ P | P − S, S′ −→ Q | S ∩ S′ | S ∪ S′ | S ∩ ¬S′
R, R′ −→ T | S | R ∪ R′ | R ◦ R′ | R∗ | id (C) We use S \ S′ as a shortcut for S ∩ ¬S′. An ALCQIbr+eg expression is a concept or a role. Subconcepts, subroles and subexpressions are defined in the natural way.
Definition 2 (Knowledge Bases). An (ALCQIbr+eg ) assertion is of the form C(a), S(a, b), or a 6= b, where C is a concept, S a simple role and a, b ∈ I. An (ALCQIbr+eg ) ABox is a set of assertions. An (ALCQIbr+eg ) concept inclusion axiom (CIA) is an expression C ⊑ C′ for arbitrary concepts C and C′. An Boolean role inclusion axiom (BRIA) is an expression S ⊑ S′ for simple roles S and S′. An ALCQIbr+eg TBox is a set of CIAs and BRIAs.
An (ALCQIbr+eg ) knowledge base (KB) is a pair K = hA, T i where T is an ALCQIbr+eg TBox and A is a non-empty ALCQIbr+eg ABox.We denote by CK the set of atomic concepts occurring in K, by RK the set of roles names occurring in K, by RK the set RK ∪ {P − | P ∈ RK}, and by IK the individuals in K.
Definition 3 (Semantics). An interpretation I = (ΔI , ·I ) consists of a non-empty domain ΔI and a valuation function ·I that maps each individual a ∈ I to an element aI ∈ ΔI , each concept name A ∈ C to a set AI ⊆ ΔI , and each role name P ∈ R to a set of pairs RI ⊆ ΔI × ΔI , in such a way that ⊤I = ΔI , ⊥I = ∅, TI = ΔI × ΔI and BI = ∅. The function ·I is inductively extended to all concepts and roles as follows:
(¬C)I=ΔI \CI (P −)I = {(y, x) | (x, y) ∈ P I} (C ⊓ C′)I=CI ∩ C′I (R ∩ R′)I = RI ∩ R′I (C ⊔ C′)I=CI ∪ C′I (R ∪ R′)I = RI ∪ R′I (∀R.C)I={x | ∀y.(x, y) ∈ RI → y ∈ CI } (¬R)I = (ΔI × ΔI) \ RI (∃R.C)I={x | ∃y.(x, y) ∈ RI ∧ y ∈ CI} (R ◦ R′)I = RI ◦ R′I (> n S.C)I={x | |{y | (x, y) ∈ SI ∧ y ∈ CI }| ≥ n} (R∗)I = (RI)∗ (6 n S.C)I={x | |{y | (x, y) ∈ SI ∧ y ∈ CI }| ≤ n} (id(C))I = {(x, x) | x ∈ CI } (∃S.Self)I={x | (x, x) ∈ SI} where ∩, ∪ and \ are overridden to denote the standard set-theoretic operations, ◦ to denote composition and ·∗ to denote the reflexive transitive closure of a binary relation.
I satisfies an assertion α, denoted I |= α, if aI ∈ AI when α = A(a); haI , bI i ∈ P I when α = P (a, b); and aI 6= bI when α = a 6≈ b. I is a model of an ABox A, denoted I |= A if it satisfies every assertion in A.I satisfies a CIA or BRIA E ⊑ E′ if EI ⊆ E′I . I is a model of a TBox T , denoted I |= T if it satisfies every CIA and BRIA in T . Finally, I is a model of K = hT , Ai, denoted I |= K, if I |= T and I |= A. Given a KB K, Knowledge base satisfiability is the problem of deciding whether there exists an I such that I |= K. 2.1 Syntactic Closure We define the (syntactic) closure of a concept, which contains all the concepts and simple roles that are relevant for deciding its satisfiability. It is analogous to the well-known FischerLadner closure of PDL, and it is exploited by the automata construction in Section 3.
In this section, we consider concepts and roles in a DL that we call ALCQIBr+eg ; it is very similar to ALCQIbr+eg but supports arbitrary role negation ¬S instead of role difference S ∩¬S′. If an ALCQIBr+eg expression is equivalent to an ALCQIbr+eg one, we call it safe. Intuitively, since ALCQIBr+eg does not impose safety, it allows for a more flexible manipulation of Boolean role expressions and a simpler notion of syntactic closure.
In what follows, we use ≷ to denote either > or 6. For a role name P ∈ C, we call P − the inverse of P and P the inverse of P −; the inverse of an atomic role Q is denoted Inv(Q). For a simple role S, Inv(S) denotes the role obtained by replacing each atomic role Q occurring in S by its inverse Inv(Q). For brevity, we assume in this subsection that ⊔ and ∀ are expressed by means ⊓, ∃ and using ¬, and that \ and ∪ are expressed using ∩ and ¬. As usual, C and C′, S and S′ and R and R′ respectively stand for concepts, simple roles and arbitrary roles. Definition 4. The closure Cl (D) of an ALCQIBr+eg concept D is defined as the smallest set of ALCQIBr+eg expressions such that D ∈ Cl (D) and: if C ∈ Cl (D) then ¬C ∈ Cl (D) (if C is not of the form ¬C′) if ¬C ∈ Cl (D) then C ∈ Cl (D) if C ⊓ C′ ∈ Cl (D) then C, C′ ∈ Cl (D) if ∃R.C ∈ Cl (D) then C ∈ Cl (D) if ∃(R ∪ R′).C ∈ Cl (D) then ∃R.C, ∃R′.C ∈ Cl (D) if ∃(R ◦ R′).C ∈ Cl (D) then ∃R.∃R′.C ∈ Cl (D) if ∃R∗.C ∈ Cl (D) then ∃R.∃R∗.C ∈ Cl (D) if ∃id (C).C′ ∈ Cl (D) then C, C′ ∈ Cl (D) if ∃S.C ∈ Cl (D) then S ∈ Cl (D) if ≷ n S.C ∈ Cl (D) then S, C ∈ Cl (D) if ∃S.Self ∈ Cl (D) then S ∈ Cl (D) if S ∩ S′ ∈ Cl (D) then S, S′ ∈ Cl (D) if ¬S ∈ Cl (D) then S ∈ Cl (D) if S ∈ Cl (D) then ¬S ∈ Cl (D) (if S is not of the form ¬S′) if S ∈ Cl (D) then Inv(S) ∈ Cl (D)
Note that |Cl (D)| is linear in the length of D and that Cl (D) may contain non safe ALCQIBr+eg expressions even when D is an ALCQIbr+eg concept. 2.2 Normalizing Knowledge Bases We present now some simple reductions that allow us to transform a KB into an equivalent one with a more restricted syntactic structure. We consider ALCQIbr+eg KBs as well as ALCQIBr+eg ones, which are defined in the natural way.
First of all, we consider the special expressions ⊤, ⊥, B and T, and show that they can be expressed without the need of special symbols. Then we show how every KB can be transformed into an extensionally reduced one, where all terminological information is expressed by CIAs. Finally, we consider the well known negation normal form of KBs. Universal role and special expressions. The special concepts ⊤ and ⊥ can be simulated via any concept names C⊤ and C⊥ not occurring in K by adding, e.g., CIAs C ⊔ ¬C ⊑ C⊤, ¬C⊤ ⊑ C⊥ and ¬C⊥ ⊑ C⊤ for any concept C. Further, using ⊤ and ⊥, the empty role B can also be easily simulated by a fresh role name PB by adding an axiom ⊤ ⊑ ∀PB.⊥. Note that the above holds for every DL containing ALC.
The universal role can be expressed in ALCQIBr+eg as ¬B, but this is not a safe role and is hence disallowed in ALCQIbr+eg KBs. In fact, in the absence of the T symbol, there is no ALCQIbr+eg role expression that is always equivalent to T. However, for each input KB K, there exists a role expression U such that the resulting KB has a model I with U I = ΔI × ΔI whenever K is satisfiable. This is similar to what occurs in other expressive DLs (e.g., SHIQ) and sufficient for the problems we consider.
Indeed, since every satisfiable ALCQIbr+eg concept C has a connected model, we can transform C into an equisatisfiable concept replacing each occurrence of T by U = (SQ∈RC Q)∗, where RC denotes the set of all atomic roles occurring in C. In the presence of ABoxes, we additionally need to ensure that all pairs of ABox individuals are in the extension of the role expression simulating T. Hence, given a KB K = hA, T i, we can eliminate the universal role T as follows: - For a fresh role name AU , an assertion AU (a, b) is added to A for every pair a, b ∈ IK. - Each occurrence of T in T is replaced by the role U = (AU ∪ SQ∈RK Q)∗. Extensionally reduced KBs. Let KB K = hA, T i be an ALCQIBr+eg KB. Of the transformations below, the one w.r.t. to the ABox is well known. Here we use a similar technique to rewrite by means of CIAs all terminological information in the ∃R.Self concepts and BRIAs. Please note that all the transformations below involve only simple roles, hence the resulting KB complies to the allowed syntax. Also, since they do not introduce any non-safe role expressions, if K is an ALCQIbr+eg KB, it will remain in ALCQIbr+eg after the reduction. – ABox reduction. K is extensionally reduced w.r.t. the ABox if only assertions of the forms A(a), P (a, b) and a 6= b with A ∈ C and P ∈ R occur in A.
The ABox reduction of K is the KB ΩABox(K) obtained as follows: 1. Each assertion of the form C(a) in A with C 6∈ C is replaced with an assertion
AC (a) for a fresh AC ∈ C and an axiom AC ⊑ C is added to T . 2. Each assertion S(a, b) in A with S 6∈ R is replaced with an assertion PS (a, b) for a fresh PS ∈ R and an axiom PS ⊑ S is added to T . – Self concepts reduction. K is extensionally reduced w.r.t. Self concepts if P ∈ R for every concept of the form ∃P.Self occurring in it.
The Self concept reduction of K is the KB ΩSelf(K) obtained by replacing each concept of the form ∃S.Self with S 6∈ R occurring in T with a concept ∃PS .Self for a fresh PS ∈ R and an adding an axiom PS ⊑ S to T . – BRIA reduction. K is extensionally reduced w.r.t. BRIAs if all axioms in T are CIAs.
The BRIA reduction of K is the KB ΩBRIA(K) obtained by replacing in T each BRIA of the form S ⊑ S′ by a CIA ∃(S \ S′).⊤ ⊑ ⊥. – KB reduction. K is extensionally reduced if it is extensionally reduced w.r.t. the ABox, Self concepts and BRIAs.
The reduction of K is the KB Ω(K) = ΩBRIA(ΩSelf(ΩABox(K))).
The above reductions preserve the semantics of the knowledge base K, and Ω(K) additionally constrains the interpretation of some concept names not occurring in K. If we consider the standard first order translation of K and Ω(K), then the latter is a conservative extension of the former. With this observation, the proof of the following proposition is straightforward: Proposition 1. For a given ALCQIBr+eg KB K, Ω(K) can be obtained in linear time. For every interpretation I, I |= Ω(K)′ implies I |= K and I |= K implies I′ |= Ω(K), where I′ denotes the interpretation s.t. E′ I = EI for every E ∈ CK ∪ RK, (AC )I′ = CI for every AC ∈ CΩ(K) \ CK, and (PS )I = SI for every PS ∈ RΩ(K) \ RK.
Thus deciding the satisfiability of K can be reduced (in linear time) to used deciding the
satisfiability of Ω(K), and we can restrict or attention to extensionally reduced knowledge
bases. Note that we can also consider Ω(K) to decide the entailment of any sentence over the
language of K; this is useful, e.g., for query answering [
Negation Normal Form. Finally, we transform KBs to negation normal form (NNF).
An ALCQIBr+eg role R is in NNF form if Q is atomic for every subrole ¬Q of R. Similarly, a concept C is in negation normal form (NNF) if A is atomic for every subconcept ¬A of C, and all roles occurring in C are in NNF. A knowledge base is in NNF if only expressions in NNF occur in it. For an expression E, nnf (E) denotes the equivalent expression in NNF obtained from E using the standard transformations. For a concept D, we let Cl nnf (D) = {nnf (E) | E ∈ Cl (D)}. For a KB K, nnf (K) denotes the KB obtained from K by replacing each expression E in K by nnf (E).
Proposition 2. For every ALCQIBr+eg expression E, nnf (E) can be obtained in linear time, and if E is an ALCQIbr+eg expression, then so is nnf (E). Further, for every KB K and every interpretation I, I |= K iff I |= nnf (K) .
An ALCQIbr+eg KB K = hA, T i is normal if it is extensionally reduced and in NNF, it does not contain ⊤, ⊥, T and B, and each concept occurring in A also occurs in T .1 1 This is w.l.o.g. as we can add to T , e.g., A ⊑ ⊤ for each A ∈ C that occurs in A but not in T . 2.3
Canonical Models and Trees We have seen that, to decide KB satisfiability, we only need to consider KBs with a restricted syntax. Now we consider some semantic properties by which the shape of the considered interpretations can also be conveniently restricted.
In what follows, we consider only ALCQIbr+eg KBs; the results of this section do not hold for ALCQIBr+eg in general.2 Like many DLs, ALCQIbr+eg has some form of the tree model property: every satisfiable TBox T (or similarly, every satisfiable concept C) has a model that can be seen as a tree with possible additional loops at some nodes, say a ‘quasi-tree’. A satisfiable ALCQIbr+eg KB K = hA, T i has a ‘quasi-forest’ shaped canonical model, in which each ABox individual is the root of a quasi-tree shaped model of T .
Definition 5. Let K = hT , Ai be an ALCQIbr+eg KB, and let 1 ≤ n ≤ |IK|, k ≥ 0. An interpretation I = (ΔI , ·I ) for K is called a canonical interpretation (with n roots and branching degree k) if: (1) each i·x ∈ ΔI has i ∈ {1, . . . , n} and x ∈ {1, . . . , k}∗; if x = ε then i is called a root. (2) {ε} ∪ ΔI is prefix closed, i.e., if x·c ∈ ΔI , then x ∈ {ε} ∪ ΔI . (3) For each a ∈ IK there is exactly one root j such that aI = j. (4) For each root j there is some a ∈ IK with aI = j. (5) If (i·w, j·w′) ∈ P I for some atomic role P and two roots i, j, then either w = w′ = ε, or i = j and one of the following holds: (i) w = w′, (ii) w′ = w·l or (iii) w = w′·l, for some 1 ≤ l ≤ k.
In ALCQIbr+eg , any TBox T can be ‘internalized’ into an equivalent concept CT , so that
the satisfiability of T can be established by obtaining a model of CT [
Proposition 3. Consider an ALCQIbreg knowledge base K
CT = ∀(SR∈RK R)∗. FC1⊑C2∈T (¬C1 ⊔ C2) For every interpretation I = (ΔI , ·I ), I |= T iff (CT )I = ΔI . Furthermore, if I is a canonical interpretation, then I |= T iff i ∈ (CT )I for each root i of I. = hA, T i, and let
Now we can establish the canonical model property of ALCQIbr+eg ; it can be shown by
adapting corresponding proofs for related logics [
Theorem 1. Every satisfiable ALCQIbr+eg KB K = hT , Ai has a canonical model I such that I is a canonical interpretation for K with branching kCT , I |= A and i ∈ (CT )I for each root i of I.
By Theorem 1, which does not hold for ALCQIBr+eg in general, deciding the satisfiability
of an ALCQIbr+eg KB boils down to deciding whether it has a canonical model. To decide
the latter, we rely on a representation of canonical interpretations as infinite labeled trees and
define an automaton that decides the existence of such trees.
2 Theorem 1 fails already in the extension of ALC with non-safe Boolean role expressions, see [
In the following, we assume a (fixed) given normal ALCQIbr+eg KB K = hA, T i. We denote IK by J and assume an arbitrary, fixed, enumeration a1, . . . , am of the elements of J . We define PI = {P ij | ai, aj ∈ J and P ∈ RK} and PS = {PSelf | P ∈ RK}. We will define the tree representation of a canonical interpretation I for K as a labeled tree TI over the alphabet ΣK = 2CK∪RK∪J ∪{r}∪{d}∪PI∪PS.
To define TI , we first note that the domain of a canonical interpretation is almost a tree; we only need to add a root ε to it. The extensions of the interpretations of individuals, concepts and roles can be represented as labels over the alphabet ΣK in a straightforward way. Roughly, each element of x ∈ ΔI , which is a node of the tree, is labeled with a set V (x) that contains: (i) the atomic concepts A such that x ∈ AI ; (ii) the atomic roles that connect the predecessor of x to x, and (iii) a special symbol PSelf for each P such that x ∈ (∃P.Self)I . The root ε and the roots of I (which are at the first level of the tree TI ) are treated differently. The label of each root i of I, apart from the atomic concepts to which i belongs, also contains the name of the individuals in J which it interprets, and it contains no basic roles. The relations between level one nodes are stored in the label of the root ε. The root ε does not represent any object in ΔI and is marked with a special identifier r and symbols of the form P ij indicating that the pair of individuals (ai, aj ) belongs to the extension of the basic role P . For simplicity, if I has n roots and |J | > n, |J | − n dummy children labeled {d} are added to the root ε, ensuring that it has exactly |J | children.
Definition 7. Let I be a canonical interpretation for K with n roots. The tree representation of I is the labeled tree TI = (T , V ) over the alphabet ΣK = 2CK∪RK∪J ∪{r}∪{d}∪PI∪PS defined as follows: • T = {ε} ∪ ΔI ∪ {n + 1, . . . , m}. • V (ε) = {r} ∪ {P ij | ai, aj ∈ J , P ∈ CK and haiI , ajI i ∈ P I }, • for each 1 ≤ i ≤ n, V (i) = {aj ∈ J | ajI = i} ∪ {A ∈ CK | ajI ∈ AI and ajI = i}, • for each n + 1 ≤ i ≤ m, V (i) = {d}, • for all other nodes i·x of T , V (i·x) = {A ∈ CK | i·x ∈ AI } ∪ {Q ∈ RK | (i·w, i·x) ∈
P I where x = w·j for some j, 1 ≤ j ≤ kCT } ∪ {PSelf | P ∈ RK and i·x ∈ (∃P.Self)I }
Note that the branching degree of TI is bounded by |J | at the root and by kCT at all other
levels, so the tree has branching degree max(kCT , |J |).
3
Automata on infinite trees allow for an elegant reduction of decision problems for temporal
and program logics [
The transition function δ maps a state q ∈ Q and an input letter σ ∈ Σ to a positive Boolean formula ϕ over atoms [k] × Q. Intuitively, if δ(q, σ) = ϕ, then each atom (c, q′) in ϕ corresponds to a new copy of the automaton going in the direction given by c and starting in state q′. E.g., a transition of the form δ(q1, σ) = (1, q2) ∧ (1, q3) ∨ (−1, q1) ∧ (0, q3) indicates that if A is in the state q1 and reads the node x labeled with σ, it proceeds by sending off either two copies, in the states q2 and q3 respectively, to the first successor of x, or one copy in the state q1 to the predecessor of x and one copy in the state q3 to x itself.
Informally, a run of a 2ATA A over a labeled tree (T , V ) is a labeled tree (Tr, r) in which each node y ∈ Tr is labeled by an element r(y) = (x, q) ∈ T × Q and describes a copy of A that is in the state q and reads the node x of T ; the labels of adjacent nodes must satisfy the transition function of A. The run is accepting if in every infinite path at least one state from F occurs infinitely often in the node labels.
Formally, given a 2ATA A = hΣ, Q, δ, q0, F i and a Σ-labeled tree (T , V ), a run of A over (T , V ) is a T ×Q-labeled tree (Tr, r) satisfying: • ε ∈ Tr and r(ε) = (ε, q0). • For each y ∈ Tr with r(y) = (x, q) there is a (possibly empty) set S = {(c1, q1) , . . . , (cn, qn)} ⊆ [k] × Q such that S satisfies δ(q, V (x)) and for all 1 ≤ i ≤ n, we have that y·i ∈ Tr, x·ci is defined and r(y·i) = (x·ci, qi).
A run (Tr, r) over (T , V ) is accepting, if for each infinite path π of Tr there is some state qf ∈ F such that the set {y ∈ π | r(y) = (x, qf ) for some x ∈ T } is infinite. A labeled tree (T , V ) is accepted by A if there is an accepting run of A over (T , V ), and L(A) denotes the set of Σ-labeled trees accepted by A.
The non-emptiness problem for 2ATAs is to decide whether, given a 2ATA A, the set L(A)
is nonempty. It was shown in [
The alphabet is ΣK = 2CK∪RK∪J ∪{r}∪{d}∪PI∪PS as given in Definition 7; note that the
only difference w.r.t. [
Like in [
More precisely, let S = J ∪ PS ∪ {c, d}. There is a state for each element of the the
set Cl ext = Cl nnf (CT ) ∪ {s, ¬s | s ∈ S} which we call the S-extended closure of CT . The
extended closure allows us to treat the individual names and special symbols in the node labels
as well as the atomic expressions in a uniform way. Note that, in contrast to [
As in [
The transition function δ : SK × ΣK → B([k] × SK), where k = max(kCT , |J |), is
defined as follows. First, for each σ in σ ∈ ΣK with r ∈ σ we define a transition δ(s0, σ)
=F1 ∧ · · · ∧ F8 from the initial state s0, which verifies (i) that the root is the only node
containing r and that the ABox individuals are properly represented by the level one nodes
(F1–F4); (ii) that all ABox assertions are satisfied (F5–F7); and (iii) that every non-dummy
node at level one is the root of a tree representing a model of CT (F8). F4 requires a transition
δ(s1, σ) from the other special state s1 for each σ ∈ ΣK, which is necessary for F4 to correctly
ensure that the symbol r only occurs at the root and the symbols in J only occur at the first
level of the tree. These transitions are as in [
The transitions that inductively decompose complex concepts while navigating the tree
are as in [
Further transitions in [
Since the potential neighbors of a node x are different depending on whether (i) x is a level one node, or (ii) x is a node at any other level, the transitions must differ accordingly. Hence, for each concept of the form ∃S.C or ∀S.C in Cl nnf (CT ) with S simple and each σ ∈ ΣK, if σ ∩ (J ∪ {d}) = ∅ we define: δ(∃S.C, σ) = ((0, SSelf) ∧ (0, C)) ∨ ((0, Inv(S)) ∧ (−1, C)) ∨
W1≤i≤kCT ((i, S) ∧ (i, C)) δ(∀S.C, σ) = ((0, nnf (¬SSelf)) ∨ (0, C)) ∧ ((0, nnf (¬Inv(S))) ∨ (−1, C)) ∧
V1≤i≤kCT ((i, nnf (¬S)) ∨ (i, C)) Otherwise, if σ ∩ (J ∪ {d}) 6= ∅, we have: δ(∃S.C, σ) = ((0, SSelf) ∧ (0, C)) ∨ Waj∈σ(−1, hj, ∃S.Ci)∨
W1≤i≤kCT((i, S) ∧ (i, C)) δ(∀S.C, σ) = ((0, nnf (¬SSelf)) ∨ (0, C)) ∧ Vaj∈σ(−1, hj, ∀S.Ci) ∧
V1≤i≤kCT ((i, nnf (¬S)) ∨ (i, C))
The first disjunct/conjunct in these transitions, which verifies whether the current node
reaches itself via S and is labelled C, is not present in the corresponding transitions from [
In the last set of transitions (case (i) above, σ ∩ (J ∪ {d}) 6= ∅), the second
disjunct/conjunct is responsible for sending a copy of the automaton to the root of the tree and
moving to the special states in SA quant , in order to traverse all the ABox individuals which are
potential neighbors of the current node. The latter is achieved as in [
^ ( δ(hj, ∀S.Ci, σ) =
^ ((0, nnf (¬Sjk)) ∨ (i, ¬ak) ∨ (i, C))) 1≤i≤|J | 1≤k≤|J |
The above transitions decompose all concepts and roles until they reach states corresponding to atomic expressions or (possibly negated) special symbols in PI ∪ PS; it is then checked whether the expression is contained in the node label σ. The transitions form the states s0 and s1 may also move to states corresponding to possibly negated symbols in J ∪{r, d}, which are similarly checked at the node labels. Thus, for each σ ∈ ΣK, each s ∈ CK ∪ RK ∪ J ∪ {r, d} and each t ∈ PI ∪ PS, there are transitions:
(true, if s ∈ σ (true, if s 6∈ σ δ(s, σ) = δ(t, σ) =
false, if s 6∈ σ
(true, if t ∈ σ or Inv(t) ∈ σ
false, otherwise
δ(¬s, σ) =
δ(¬t, σ) =
false, if s ∈ σ
false, otherwise
(true, if t 6∈ σ and Inv(t) 6∈ σ
where Inv(t) = Inv(P )ji if t = P ij and Inv(t) = Inv(P )Self if t = PSelf for each P ∈ RK.
These transitions extend similar ones in [
By a simple adaptation of the proofs in [
This shows that the automaton AK can be used to decide the satisfiability of K. Theorem 2. K is satisfiable iff the set of trees accepted by AK is nonempty.
Under unary encoding of numbers in restrictions, the number of states of AK is polynomial
in the size of K. Since ΣK is single exponential in the size of K, we can exploit the results of
[
Corollary 1. Satisfiability of ALCQIbr+eg knowledge bases is EXPTIME-complete. 4
Reasoning in SRI Q
The description logic SRIQ was introduced in [
A set Rh of SRIAs is regular if there exists a partial order ≺ on R such that Inv(R) ≺ R′ iff R ≺ R′ for every R, R′ ∈ R, and such that every SRIA in Rh is of one of the following forms: (i) R ◦ R ⊑ R, or (ii) Inv(R) ⊑ R, or (iii) R1 ◦ . . . ◦ Rn ⊑ R and Ri ≺ R for each 1 ≤ i ≤ n, or (iv) R ◦ R1 ◦ . . . ◦ Rn ⊑ R and Ri ≺ R for each 1 ≤ i ≤ n, or (v) R1 ◦ . . . ◦ Rn ◦ R ⊑ R and Ri ≺ R for each 1 ≤ i ≤ n.
Given a set Rh of SRIAs, let RRh denote the set of roles occurring in Rh. The set of simple roles in Rh is the minimal set SR(Rh) ⊆ RRh containing each role R such that (i) there are no SRIAs of the form R1 ◦ . . . ◦ Rn ⊑ R in Rh, and (ii) if n = 1 and R1 ∈ SR(Rh) for every SRIA of the form R1 ◦ . . . ◦ Rn ⊑ R in Rh, then R ∈ SR(Rh).
A role assertion is an expression of the form Sym(R), Ref(R), Irr(R), or Dis(R, R′), where R, R′ ∈ R.3 An RBox R is a finite set of SRIAs and role assertions such that R ∈ SR(Rh) for each R occurring in a role assertion of the form Ref(R), Irr(R) or Dis(R, R′) in R, where Rh denotes the set of SRIAs in R. We say that R is regular if Rh is regular, and define SR(R) = SR(Rh).
Similarly as in ALCQIbr+eg , (SRIQ) concepts C, C′ obey the following syntax C, C′ −→ A | ¬C | C ⊓ C′ | C ⊔ C′ | ∀R.C | ∃R.C |> n S.C |6 n S.C | ∃S.Self, where A ∈ C and R, S ∈ R. A (SRIQ) concept inclusion axiom (SCIA) is an expression C ⊑ C′ for arbitrary SRIQ concepts C and C′. A (SRIQ) TBox is a set of SCIAs. For an RBox R, a concept C is R-simple if S ∈ SR(Rh) for each S occurring in a subconcept of C of the form > n S.C′, 6 n S.C′ or ∃S.Self; a TBox T is R-simple if all concepts occurring in the SCIAs of T are R-simple.
An (SRIQ) assertion is an expression C(a), R(a, b), ¬S(a, b) or a 6= b, where C is a SRIQ concept, S, R are SRIQ roles and a, b ∈ I. An (SRIQ) ABox is a set of SRIQ assertions. An ABox A is R-simple for an RBox R if S ∈ SR(Rh) for each S occurring in an assertion of the form ¬S(a, b).
An (SRIQ) knowledge base is a tuple K = hA, T , Ri where R is a regular SRIQ RBox, A a non-empty R-simple SRIQ ABox and T an R-simple SRIQ TBox.
The semantics of SRIQ TBoxes and ABoxes is defined as for ALCQIbr+eg . An interpretation I satisfies a role assertion Sym(R), Ref(R) or Irr(R) if RI is a symmetric, reflexive or irreflexive relation, respectively; I satisfies Dis(R, R′) if the relations are disjoint, i.e., RI ∩ R′I = ∅; I satisfies a SRIA R1 ◦ . . . ◦ Rn ⊑ R if R1I ◦ . . . ◦ RnI ⊆ RI , where again we override the symbol ◦ and use it to denote binary role composition. An interpretation I is a model of an RBox, in symbols I |= R, if it satisfies all SRIAs and role assertions in R. Modelhood of a KB is restricted in the natural way to the models of the RBox, i.e., I |= hA, T , Ri iff I |= A, I |= T and I |= R. 4.1 Reducing SRI Q to ALCQI br+eg The restriction to regular RBoxes, which is crucial for the decidability of SRIQ, ensures that all implications between roles can be captured by a set of regular expressions. This will allow us to reduce reasoning in SRIQ to reasoning in ALCQI br+eg , and to show that the algorithm we have presented is also an optimal decision procedure for SRIQ KB satisfiability.
If R is a regular RBox, then for every role R ∈ R there is a regular expression ρR such
that a word w = R1 ◦ . . . ◦ Rn over R is in the language of ρR iff wI ⊆ RI in every model
I of R. This was shown in [
Reducing TBoxes. Each regular expression ρR is an ALCQIbr+eg role. Further, if a role S
is simple in R, then ρS is the regular expression S(S′⊑S)∈R S′, which is in fact a simple
ALCQIbr+eg role. As a consequence, if we replace R by ρR is any SRIQ concept, the
resulting expression is an ALCQIbr+eg concept. This allows for a natural translation of SRIQ
concepts and TBoxes into ALCQI br+eg .
3 In [
Definition 10. Given an SRIQ ABox A, let Aneg contain all negative role assertions ¬S(a, b), and let Apos be obtained by replacing each assertion ¬S(a, b) in Aneg by P¬S (a, b), where P¬S is a fresh role name. Further, let RA be the set of ALCQIbr+eg BRIAs containing P¬S ∩ S ⊑ B for each ¬S(a, b) in A.
If an ABox contains an assertion in which a non-simple role R occurs, ρR is not a simple ALCQIbr+eg role and hence we can not replace R with it. Instead, we explicitly add as assertions all relations between individuals that are implied by the RBox.
Definition 11. Let A and R be a SRIQ ABox and a SRIQ RBox respectively. The Rextension of A, denoted AR, is the minimal set of assertions containing A such that, if there are individuals a1, . . . , an+1 ∈ IK and a SRIA R1◦. . .◦Rn ⊑ R in R such that Ri(ai, ai+1) ∈ AR for each 1 ≤ i ≤ n, then R(a1, an+1) ∈ AR.
Reducing RBoxes. As for the RBox, the satisfaction of the SRIAs is ensured by the regular expressions added to the TBox and the assertions added to the ABox. We only have to ensure the satisfaction of the role assertions, which is easy in ALCQIbr+eg .
Definition 12. Let R be a regular SRIQ RBox and let R′ denote the set of role assertions in R. We denote by RB the set of BRIAs and CIAs that contains: • R ⊑ R′ for every SRIA R ⊑ R′ in R such that R′ ∈ SR(R), • R ⊑ Inv(R) and Inv(R) ⊑ R for every assertion Sym(R) in R′, • ⊤ ⊑ ∃R.Self for every assertion Ref(R) in R′, • ∃R.Self ⊑ ⊥ for every assertion Irr(R) in R′, and • R ∩ R′ ⊑ B for every assertion Dis(R, R′) in R′.
Reducing KBs. Now we can reduce any given SRIQ KB K = hA, T , Ri into an equivalent ALCQIbr+eg KB K = hA, T i as follows.
Definition 13. Let K = hA, T , Ri be a SRIQ knowledge base. We denote by K′ = hA′, T ′i the following ALCQIbr+eg KB: • The ABox A′ is AR, where A = (A \ Aneg) ∪ Apos. • The TBox T ′ is T R ∪ RA ∪ RB .
For any interpretation I, I |= K implies I |= K′. The converse holds in a slightly weaker form. While a model of K′ need not be closed under the RBox and it may not be a model of K, the models of K′ and K may only differ in the interpretation of some ‘implied’ roles. Adding them to a model of K′, we obtain a model of K.
For a model I of K′, the extension of I to R is the interpretation IR such that ΔI = ΔI ; (A)IR = (A)I for every atomic concept A; and for every atomic role P occurring in R, if R (x, y) ∈ (ρP )I or (y, x) ∈ (ρP − )I , then (x, y) ∈ (P )I . It can be easily verified that if I |= K′, then IR |= K. Hence, we can reduce the satisfiability problem for any SRIQ knowledge bases to satisfiability of an ALCQIbr+eg one. Proposition 6. Let K = hA, T , Ri be a SRIQ knowledge base. Then K is satisfiable iff K′ is satisfiable.
As a consequence, the automata algorithm in Section 3 can be used to decide the satisfiability of SRIQ knowledge bases.
Furthermore, it is worst case optimal. All steps are clearly polynomial in the size of A, T
and exp(R). However, the size of exp(R) can be exponential in the size of R [
It was recently shown that SRIQ is 2EXPTIME hard [
Note that the blow-up in complexity w.r.t. ALCQIbr+eg is due to the size of exp(R), and
that the algorithm is single exponential whenever exp(R) is polynomial in R; this includes,
for example, the so-called simple role hierarchies defined in [
Conclusions
We have shown that the DL ALCQIbr+eg fully captures the DL SRIQ. Although the latter
is exponentially more succinct, reasoning is also (provably) exponentially harder in the worst
case. The syntax of ALCQIbr+eg allows for additional constructions not supported by SRIQ,
like Boolean role expressions and inclusions between them. Since these additional features
can be useful for modeling KBs and for ontology engineering [
In order for ALCQIbr+eg to become a suitable alternative to SRIQ in practice, the main challenge that remains ahead is to explore alternatives for practicable algorithms for this kind of logics, and to implement them in actual reasoners. Unfortunately, DLs that support transitive closure, or more generally, regular expressions over roles in the style of PDL, have largely been displaced by the better known alternative of role hierarchies on which implemented reasoners have focused. While it is often claimed that the development systems that support such logics is problematic, to our knowledge there have been no major attempts to do it. Regular expressions are nevertheless worth exploring, as they are well understood and widely used in computer science, and are likely to be useful for ontology engineering.
Another natural alternative is to extend SRIQ with more constructors from ALCQIbr+eg .
In particular, one can consider SRIQb, the extension of SRIQ with safe Boolean role
expressions; similar extensions of closely related DLs like SHIQ and SROIQ were
already considered in [
Finally, we point out that with the techniques given here, the query answering problem
for SRIQ can be reduced to ALCQIbr+eg , showing that answering two-way positive regular
path queries as defined in [