We show that deciding conjunctive query inseparability for OWL 2 QL ontologies is PSpace-hard and in ExpTime. We give polynomial-time (incomplete) algorithms and demonstrate by experiments that they can be used for practical module extraction.
Ontology-based data access (OBDA) has recently emerged as one of the most
interesting and challenging applications of description logic. The key idea is to
use ontologies for enriching data with background knowledge, and thereby
enable query answering over incomplete and semistructured data via a high-level
conceptual interface. The W3C recognised the importance of OBDA by
including in the OWL 2 Web Ontology Language the pro le OWL 2 QL, which was
designed for OBDA with relational database systems. OWL 2 QL is based on a
description logic that was originally introduced under the name DL-LiteR [
In the context of OBDA, the basic notion underlying many ontology engineering tasks is -query inseparability : for a signature (a set of concept and role names) , two ontologies are deemed to be inseparable if they give the same answers to any conjunctive query over any data formulated in . Thus, in applications using -queries and data, one can safely replace any ontology by a -query inseparable one. Note that the relativisation to is very important here. For example, one cannot expect modules of an ontology to be query inseparable from the whole ontology for arbitrary queries and data sets, whereas this should be the case if we restrict the query and data language to the module's signature or a speci ed subset thereof. Similarly, when comparing two versions of one ontology, the subtle and potentially problematic di erences are those that concern queries over their common symbols, rather than all symbols occurring in these versions. In applications where ontologies are built using imported parts, a stronger notion of inseparability is required: two ontologies are strongly -query inseparable if they give the same answers to -queries and data when imported to an arbitrary context ontology formulated in .
The aim of this paper is to (i) investigate the computational complexity of deciding (strong) -query inseparability for DL-LitecHore ontologies, (ii) develop e cient (though incomplete) algorithms for practical inseparability checking, and (iii) analyse the performance of the algorithms for the challenging task of minimal module extraction.
One of our surprising discoveries is that the analysis of -query
inseparability for DL-LitecHore ontologies requires drastically di erent logical tools
compared with the previously considered DLs. It turns out that the new syntactic
ingredient|the interaction of role inclusions and inverse roles|makes deciding
(strong) query inseparability PSpace-hard, as opposed to the known coNP and
2p-completeness results for DL-Lite dialects without role inclusions [
-Query Entailment and Inseparability We begin by formally de ning DL-LitecHore, underlying OWL 2 QL, and the notions of -query inseparability and entailment. The language of DL-LitecHore contains countably in nite sets of individual names ai, concept names Ai, and role names Pi. Roles R and concepts B of this language are de ned by: R ::=
Pi j
Pi ;
B ::= ? j > j
Ai j 9R: A DL-LitecHore TBox, T , is a nite set of inclusions
B1 v B2;
R1 v
R2;
B1 u B2 v ?;
R1 u R2 v ?;
where B1; B2 are concepts and R1; R2 roles. An ABox, A, is a nite set of
assertions of the form B(ai), R(ai; aj ) and ai 6= aj , where ai and aj are individual
names, B a concept and R a role. Ind(A) will stand for the set of individual names
occurring in A. Taken together, T and A constitute the DL-LitecHore knowledge
base (KB, for short) K = (T ; A). The sub-language of DL-LitecHore without role
inclusions R1 v R2 is denoted by DL-Litecore [
A conjunctive query (CQ) q(x1; : : : ; xn) is a rst-order formula
9y1 : : : 9ym '(x1; : : : ; xn; y1; : : : ; ym); where ' is constructed, using only ^, from atoms of the form B(t) and R(t1; t2), with B being a concept, R a role, and ti being an individual name or a variable from the list x1; : : : ; xn; y1; : : : ; ym. The variables in ~x = x1; : : : ; xn are called answer variables of q. We say that an n-tuple ~a Ind(A) is an answer to q in an interpretation I if I j= q[~a] (here we regard I to be a rst-order structure); ~a is a certain answer to q over a KB K = (T ; A) if I j= q[~a] for all models I of K; in this case we write K j= q[~a].
To de ne the main notions of this paper, consider two KBs K1 = (T1; A) and K2 = (T2; A). For example, the Ti are di erent versions of some ontology, or one of them is a re nement of the other by means of new axioms. The question we are interested in is whether they give the same answers to queries formulated in a certain signature, say, in the common vocabulary of the Ti or in a vocabulary relevant to an application. To be precise, by a signature, , we understand any nite set of concept and role names. A concept (inclusion, TBox, etc.) all concept and role names of which are in is called a -concept (inclusion, etc.). We say that K1 -query entails K2 if, for all -queries q(~x) and all ~a Ind(A), K2 j= q[~a] implies K1 j= q[~a]. In other words: any certain answer to a -query given by K2 is also given by K1. As the ABox is typically not xed or known at the ontology design stage, we may have to compare the TBoxes over arbitrary -ABoxes rather than a xed one, which gives our central de nition: De nition 1. Let T1 and T2 be TBoxes and a signature. T1 -query entails T2 if (T1; A) -query entails (T2; A) for any -ABox A. T1 and T2 are -query inseparable if they -query entail each other, in which case we write T1 T2. In many applications, -query inseparability is enough to ensure that T1 can be safely replaced by T2. However, if they are developed as part of a larger ontology or are meant to be imported in other ontologies, a stronger notion is required: De nition 2. T1 strongly -query entails T2 if T1 [ T -query entails T2 [ T , for all -TBoxes T . T1 and T2 are strongly -query inseparable if they strongly -query entail each other, in which case we write T1 s T2.
The following example illustrates the di erence between -query and strong
-query inseparability. For further discussion and examples, consult [
The canonical model, MK, of a consistent KB K = (T ; A) gives correct answers to all CQs. In general, MK is in nite; however, it can be folded up into a small generating model GK = (IK; K) consisting of a nite interpretation IK and a generating relation K that de nes the unfolding. Let vT be the re exive and transitive closure of the role inclusion relation given by T , and let [R] = fS j R vT S and S vT Rg. We write [R] T [S] if R vT S; thus, T is a partial order on the set f[R] j R a role in T g. For each [R], we introduce a witness w[R] and de ne a generating relation K on the set of these witnesses together with Ind(A) by taking: { a K w[R] if a 2 Ind(A) and [R] is
K 6j= R(a; b) for all b 2 Ind(A); { w[S] K w[R] if [R] is T -minimal with T j= 9S T -minimal such that K j= 9R(a) and v 9R and [S ] 6= [R].
A role R is generating in K if there are a 2 Ind(A) and R1; : : : ; Rn = R such that a K w[R1] K K w[Rn]. The interpretation IK is de ned as follows:
IK = Ind(A) [ fw[R] j R is generating in Kg; aIK = a; for all a 2 Ind(A); AIK = fa 2 Ind(A) j K j= A(a)g [ fw[R] j T j= 9R v Ag; P IK = f(a; b) 2 Ind(A)
Ind(A) j there is R(a; b) 2 A s.t. [R] f(x; w[R]) j x f(w[R]; x) j x
K w[R] and [R] K w[R] and [R] GK can be constructed in polynomial time in jKj, and it is not hard to see that IK j= K. To construct the canonical model MK giving the correct answers to all CQs, we unfold the generating model GK = (IK; K) along K. A path in GK is a nite sequence aw[R1] w[Rn], n 0, such that a 2 Ind(A), a K w[R1] and w[Ri] K w[Ri+1], for i < n. Denote by path(GK) the set of all paths in GK and by tail( ) the last element in 2 path(GK). MK is de ned by taking:
MK = path(GK); aMK = a; for all a 2 Ind(A);
AMK = f j tail( ) 2 AIK g; P MK = f(a; b) 2 Ind(A)
Ind(A) j (a; b) 2 P IK g [ f( ; f(
w[R]) j tail( ) w[R]; ) j tail( ) Theorem 5. For all consistent DL-LitecHore KBs K = (T ; A), CQs q(~x) and ~a Ind(A), we have K j= q[~a] i MK j= q[~a].
Thus, to decide -query entailment between KBs K1 and K2, it su ces to check whether MK2 j= q[~a] implies MK1 j= q[~a] for all -queries q(~x) and tuples ~a. This relationship between MK2 and MK1 can be characterised semantically in terms of nite -homomorphisms. For an interpretation I and a signature , the -types tI (x) and rI (x; y), for x; y 2 I , are given by: tI (x) = f -concept B j x 2 BI g; rI (x; y) = f -role R j (x; y) 2 RI g: A -homomorphism from an I to I0 is a function h : I ! I0 such that h(aI ) = aI0 , for all individual names a interpreted in I, tI (x) tI0 (h(x)) and rI (x; y) rI0 (h(x); h(y)), for all x; y 2 I .
It is well-known that answers to conjunctive -queries are preserved under -homomorphisms. Thus, if there is a -homomorphism from MK2 to MK1 , then K1 -query entails K2. However, the converse does not hold in general.
MK2 Example 6. Take T1 from Example 4, and let T2 result from replacing R in T1 with R . Let = fA; Rg and Ki = (Ti; fA(a)g). Then the -reduct of MK1 does not contain a -homomorphic image of the -reduct of MK2 , depicted below. On the other hand, it is easily seen that T1 and T2 are -query inseparable.
Aa R R . . .
Note that the -reduct of MK2 contains points that are not reachable from the ABox by -roles. In fact, using Konig's Lemma, one can show that if every point in MK2 is reachable from the ABox by a path of -roles, then K1 -query entails K2 i there exists a -homomorphism from MK2 to MK1 . We say that I is nitely -homomorphically embeddable into I0 if, for every nite sub-interpretation I1 of I, there exists a -homomorphism from I1 to I0. Theorem 7. Let K1 and K2 be consistent DL-LitecHore KBs. Then K1 entails K2 i MK2 is nitely -homomorphically embeddable into MK1 . -query Theorem 7 does not yet give a satisfactory semantic characterisation of query entailment between TBoxes, as one still has to consider in nitely many -ABoxes. However, using the fact that inclusions in DL-LitecHore, di erent from disjointness axioms, involve only one concept or role in the left-hand side and making sure that the TBoxes entail the same -inclusions, one can show that it is enough to consider singleton -ABoxes of the form fB(a)g. Denote the models G(T ;fB(a)g) and M(T ;fB(a)g) by GTB and MTB, respectively. We thus obtain the following characterisation of -entailment between DL-LitecHore TBoxes: Theorem 8. T1
-query entails T2 i (p) T2 j= (h) MTB2 is sistent implies T1 j= , for all -inclusions ;
nitely -homomorphically embeddable into MTB1 , for all T1-con-concepts B.
By applying condition (p) to B v ?, we obtain that every T1-consistent concept B is also T2-consistent. 4
We use Theorem 8 to show that deciding -query entailment for DL-LitecHore
TBoxes is PSpace-hard and in ExpTime. Recall that subsumption in DL-LitecHore
is NLogSpace-complete [
We begin by considering DL-Litecore, where the existence of
-homomorphisms between canonical models can be expressed in terms of the types of their
points; cf. [
ITB2 , there is x0 2 ITB1 with tITB2 (x) tITB1 (x0).
The criterion of Theorem 9 can be checked in polynomial time, in NLogSpace, to be more precise. Thus:
plete for NLogSpace.
-query entailment for TBoxes in DL-Litecore is comHowever, if role inclusions become available, the picture changes dramatically: not only do we have to compare the -types of points in the canonical models, but also the -paths to these points. To illustrate, consider the generating models G1, G2 in Fig. 1, where the arrows represent the generating relations, and the concept names A, Xi0, Xi1 and the role names R and Tj are all symbols in . The model G2 contains 4 R-paths from a to w, which are further extended by the in nite Tj -paths. The paths from a to w can be homomorphically mapped to distinct R-paths h( ) in G1 starting from a. But the extension of such a with the in nite Tj -chain can only be mapped rst to a su x of h( ) (backward, along Tj )|because we have to map paths in the unfolding M2 of G2 to paths in M1|and then to a Tj -loop in G1. But to check whether this can be done, we may have to `remember' the whole path .
A
G2 a A a
T1
R;Tj T1
T2 X21 R;Tj R;Tj
R R
T2 R;Tj
X31 X30
T1 X31 R;Tj R;Tj
R R
T1
R;Tj X10 R;Tj
X20 R;Tj
X30 R;Tj w T2 X41 R;Tj R;Tj X40
T2
To see that G1 and G2 can be given by DL-LitecHore TBoxes, x a QBF Q1X1 : : : QnXn Vm
j=1 Cj , where Qi 2 f8; 9g and C1; : : : ; Cm are clauses over the variables X1; : : : ; Xn. Let = fA; Xi0; Xi1; R; Tj j i n; j mg, T1 contain the inclusions
Xik v 9Rj if k = 0; :Xi 2 Cj or k = 1; Xi 2 Cj ; and let T2 contain the inclusions 9(Qik)
A v 9S0 ;
v Xik; 9Rj v 9Rj ;
A v 9S0 ; 9(Qik)
v Xik; 9Sn v 9Pj ; 9Si 1 v 9Qik;
Qk
i v Si; Rj v Tj ; 9Si 1 v
Qk
i v Si; 9Pj v 9Pj ; ( 9Qik; 9Si;
Si v R; Si v Tj ; if Qi = 8; if Qi = 9;
Si v R; Pj v Tj ; for all i n, j m, k = 1; 2. The generating models GTA1 and GTA2 , restricted to , look like G1 and G2 in Fig. 1, respectively. Moreover, one can show that MTA2 is ( nitely) -homomorphically embeddable into MTA1 i the QBF above is satis able. As satis ability of QBFs is PSpace-complete, we obtain:
-query entailment for DL-LitecHore TBoxes is PSpace-hard.
On the other hand, the problem whether MK2 is nitely -homomorphically
embeddable into MK1 can be reduced to the emptiness problem for alternating
two-way automata, which belongs to ExpTime [
-query entailment for DL-LitecHore TBoxes is in ExpTime.
The precise complexity of -query entailment for DL-LitecHore TBoxes is still
unknown. Recall that deciding -query entailment for DL-LitehNorn is
coNPcomplete [
Let us consider strong -query entailment. It is easy to construct an exponential-time algorithm checking strong -query entailment between DL-LitecHore TBoxes T1 and T2: enumerate all -TBoxes T and check whether T1 [T -query entails T2 [ T . As there are quadratically many -inclusions, this algorithm calls the -query entailment checker 2j j2 times. We now show that one can do much better than that. First, it turns out that instead of expensive -query entailment checks for the TBoxes Ti [ T , it is enough to check consistency (in polynomial time). More precisely, suppose T1 -query entails T2. One can show then that T1 does not strongly -query entail T2 i there exist a -TBox T and a -concept B such that (T1 [ T ; fB(a)g) is consistent but (T2 [ T ; fB(a)g) is not (cf. Example 3). Moreover, checking consistency for all -TBoxes T can further be reduced|using the primitive form of DL-LitecHore axioms|to checking consistency for all singleton -TBoxes T . Thus, we obtain the following: Theorem 13. Suppose that T1 -query entails T2. Then T1 does not strongly query entail T2 i there is a -concept B and a -TBox T with a single inclusion of the form B1 v B2 or R1 v R2 such that (T1 [ T ; fB(a)g) is consistent but (T2 [ T ; fB(a)g) is inconsistent.
So, if we already know that T1 -query entails T2, then checking whether this entailment is actually strong can be done in polynomial time (and NLogSpace).
The interplay between role inclusions and inverse roles, required in the proof of PSpace-hardness, appears to be too arti cial compared to how roles are used in `real-world' ontologies. Thus, in conceptual modelling, the number of roles is comparable with the number of concepts, but the number of role inclusions is much smaller. For this reason, instead of a complete (exponential) -query entailment checker, we have implemented a polynomial-time correct but incomplete algorithm, which is based on testing simulations between transition systems.
Let T1 and T2 be DL-LitecHore TBoxes, a signature, B a -concept. Denote Ki = (Ti; fB(a)g) and Ii = IKi , i = 1; 2. A relation I2 I1 is called a -simulation of GK2 in GK1 if the following conditions hold: (s1) the domain of is I2 and (aI2 ; aI1 ) 2 ; (s2) tI2 (x) tI1 (x0), for all (x; x0) 2 ; (s3) if x K2 w[R] and (x; x0) 2 , then there is y0 2 and S 2 rI1 (x0; y0) for every -role S with [R]
I1 such that (w[R]; y0) 2
We call a forward -simulation if it satis es (s1), (s2) and the condition
(s30), which strengthens (s3) with the extra requirement: y0 = w[T ], for some
role T , with x0 K1w[T ] and [T ] T1 [S] for every -role S with [R] T2 [S].
Example 14. In Example 6, there is a -simulation of GK2 in GK1 , but no forward
-simulation. The same applies to G2 and G1 in the proof of the PSpace bound.
In contrast to nite -homomorphic embeddability of MK2 in MK1 , the problem
of checking the existence of (forward) -simulations of GK2 in GK1 is tractable
and well understood from the literature on program veri cation [
every T1-consistent -concept B; (n) condition (p) does not hold or there is no any T1-consistent -concept B.
B in GTB1 , for -simulation of GT2
B in GTB1 , for -simulation of GT2 Theorem 15. Let T1; T2 be DL-LitecHore TBoxes and a signature. If (y) holds, then T1 -query entails T2. If (n) holds, then T1 does not -query entail T2.
Thus, an algorithm checking conditions (y) and (n) can be used as a correct but incomplete -query entailment checker. It cannot be complete since neither (y) nor (n) holds in Example 14. On the other hand, condition (n) proves to be a criterion of -query entailment in two important cases: Theorem 16. Let (a) T1, T2 be DL-Litecore TBoxes, or (b) T1 = ; and T2 a DL-LitecHore TBox. Then condition (n) holds i T1 does not -query entail T2. 6
Checking (strong) -query entailment has multiple applications in ontology versioning, re-use, and extraction. We have used the algorithms, suggested by Theorems 15 and 13, for minimal module extraction to see how e cient they are in practice and whether the incompleteness of the (y){(n) conditions is problematic. Extracting minimal modules from medium-sized real-world ontologies requires thousands of calls of the (strong) provides a tough test for our approach.
For a TBox T and a signature , a subset M
T is -query entailment checker, and thus { a -query module of T if M T ; { a strong -query module of T if M { a depleting -query module of T if ; signature of M.
s T ;
s [sig(M) T n M, where sig(M) is the
We are concerned with computing a minimal (w.r.t. ) -query (MQM), a
minimal strong -query (MSQM), and the (uniquely determined) minimal depleting
-query (MDQM) module of T . The general extraction algorithms, which call
-query entailment checkers, are taken from [
We extracted modules from OWL 2 QL approximations of 3 commercial
software applications called Core, Umbrella and Mimosa (the original ontologies use
a few axioms that are not expressible OWL 2 QL). Mimosa is a specialisation
of the MIMOSA OSA-EAI speci cation4 for container shipping. Core is based
on a supply-chain management system used by the bookstore chain Ottakar's
(now merged with Waterstone's), and Umbrella on a research data validation
and processing system used by the Intensive Care National Audit and Research
Centre.5 The original Core and Umbrella were used for the experiments in [
Core (1233) Mimosa (763) Umbrella (1519) IMDB (66) LUBM (145) 375375 391