Exchanging OWL 2 QL Knowledge Bases

1 Introduction

Complex forms of information, maintained in different formats and organized according to different structures, often need to be shared between agents. In recent years, both in the data management and in the knowledge representation communities, several settings have been investigated that address this problem from various perspectives: in information integration, uniform access is provided to a collection of data sources by means of an ontology (or global schema) to which the sources are mapped [Lenzerini, 2002]; in peer-topeer systems, a set of peers declaratively linked to each other collectively provide access to the information assets they maintain [Kementsietsidis et al., 2003; Adjiman et al., 2006; Fuxman et al., 2006]; in ontology matching, the aim is to understand and derive the correspondences between elements in two ontologies [Euzenat and Shvaiko, 2007; Shvaiko and Euzenat, 2013]; finally, in data exchange, the information stored according to a source schema needs to be restructured and translated so as to conform to a target schema [Fagin et al., 2005; Barcel´o, 2009].

The work we present in this paper is inspired by the latter setting, investigated in databases. We study it, how- Diego Calvanese TU Vienna, Austria Free U. of Bolzano, Italy & calvanese@inf.unibz.it Vladislav Ryzhikov Free U. of Bolzano Italy ryzhikov@inf.unibz.it ever, under the assumption of incomplete information typical of knowledge representation [Arenas et al., 2011]. Specifically, we investigate the problem of knowledge base exchange, where a source knowledge base (KB) is connected to a target KB by means of a declarative mapping specification, and the aim is to exchange knowledge from the source to the target by exploiting the mapping. We rely on a framework for KB exchange based on lightweight Description Logics (DLs) of the DL-Lite family [Calvanese et al., 2007], recently proposed in [Arenas et al., 2012a; 2012b]: both source and target are KBs constituted by a DL TBox, representing implicit information, and an ABox, representing explicit information, and mappings are sets of DL concept and role inclusions. Note that in data and knowledge base exchange, differently from ontology matching, mappings are first-class citizens. In fact, it has been recognized that building schema mappings is an important and complex activity, which requires the designer to have a thorough understanding of the source and how the information therein should be related to the target. Thus, several techniques and tools have been developed to support mapping design, e.g., exploiting lexical information [Fagin et al., 2009]. Here, similar to data exchange, we assume that for building mappings the target signature is given, but no further axioms constraining the target knowledge are available. In fact, such axioms are derived from the source KB and the mapping.

We consider two key problems: (i) computing universal solutions, which have been identified as one of the most desirable translations to be materialized; (ii) UCQ-representability of a source TBox by means of a target TBox that captures at best the intensional information that can be extracted from the source according to a mapping using union of conjunctive queries. Determining UCQ-representability is a crucial task, since it allows one to use the obtained target TBox to infer new knowledge in the target, thus reducing the amount of extensional information to be transferred from the source. Moreover, it has been noticed that in many data exchange applications users only extract information from the translated data by using specific queries (usually conjunctive queries), so query-based notions of translation specifically tailored to store enough information to answer such queries have been widely studied in the data exchange area [Madhavan and Halevy, 2003; Fagin et al., 2008; Arenas et al., 2009; Fagin and Kolaitis, 2012; Pichler et al., 2013]. For these two problems, we investigate both the task of checking membership, where a candidate universal solution (resp., UCQrepresentation) is given and one needs to check its correctness, and non-emptiness, where the aim is to determine the existence of a universal solution (resp., UCQ-representation).

We significantly extend previous results in several directions. First of all, we establish results for OWL2QL [Motik et al., 2012], one of the profiles of the standard Web Ontology Language OWL 2 [Bao et al., 2012], which is based on the DL DL-LiteR. To do so, we have to overcome the difficulty of dealing with null values in the ABox, since these become necessary in the target to represent universal solutions. Also, for the first time, we address disjointness assertions in the TBox, a construct that is part of OWL 2QL. The main contribution of our work is then a detailed analysis of the computational complexity of both membership and non-emptiness for universal solutions and UCQ-representability. For the nonemptiness problem of universal solutions, previous known results covered only the simple case of DL-LiteRDFS , the RDFS fragment of OWL2QL, in which no new facts can be inferred, and universal solutions always exist and can be computed in polynomial time via a chase procedure (see [Calvanese et al., 2007]). We show that in our case, instead, the problem is PSPACE-hard, hence significantly more complex, and provide an EXPTIME upper bound based on a novel approach exploiting two-way alternating automata. We provide also NP upper bounds for the simpler case of ABoxes without null values, and for the case of the membership problem. As for UCQ-representability, we adopt the notion of UCQrepresentability introduced in [Arenas et al., 2012a; 2012b] and extend it to take into account disjointness of OWL2QL. For that case we show NLOGSPACE-completeness of both non-emptiness and membership, improving on the previously known PTIME upper bounds.

The paper is organized as follows. In Section 2, we give preliminary notions on DLs and queries. In Section 3, we define our framework of KB exchange and discuss the problem of computing solutions. In Section 4, we overview our contributions, and then we provide our results on computing universal solutions in Section 5, and on UCQ-representability in Section 6. Finally, in Section 7, we draw some conclusions and outline issues for future work.

The proofs are available in an extended technical report accessible at http://arxiv.org/abs/1304.5810.

2 Preliminaries

The DLs of the DL-Lite family [Calvanese et al., 2007] of light-weight DLs are characterized by the fact that standard reasoning can be done in polynomial time. We adapt here DL-LiteR, the DL underlying OWL2QL, and present now its syntax and semantics. Let NC, NR, Na, Nℓ be pairwise disjoint sets of concept names, role names, constants, and labeled nulls, respectively. Assume in the following that A ∈ NC and P ∈ NR; in DL-LiteR, B and C are used to denote basic and arbitrary (or complex) concepts, respectively, and R and Q are used to denote basic and arbitrary (or complex) roles, respectively, defined as follows:

From now on, for a basic role R, we use R- to denote P - when R = P , and P when R = P -.

A TBox is a finite set of concept inclusions B ⊑ C and role inclusions R ⊑ Q. We call an inclusion of the form B1 ⊑ ¬B2 or R1 ⊑ ¬R2 a disjointness assertion. An ABox is a finite set of membership assertions B(a), R(a, b), where a, b ∈ Na. In this paper, we also consider extended ABoxes, which are obtained by allowing labeled nulls in membership assertions. Formally, an extended ABox is a finite set of membership assertions B(u) and R(u, v), where u, v ∈ (Na∪Nℓ). Moreover, a(n extended) KB K is a pair 〈T , A〉, where T is a TBox and A is an (extended) ABox.

A signature Σ is a finite set of concept and role names. A KB K is said to be defined over (or simply, over) Σ if all the concept and role names occurring in K belong to Σ (and likewise for TBoxes, ABoxes, concept inclusions, role inclusions and membership assertions). Moreover, an interpretation I of Σ is a pair 〈∆I , ·I 〉, where ∆I is a non-empty domain and ·I is an interpretation function such that: (1) AI ⊆ ∆I , for every concept name A ∈ Σ; (2) P I ⊆ ∆I × ∆I , for every role name P ∈ Σ; and (3) aI ∈ ∆I , for every constant a ∈ Na. Function ·I is extended to also interpret concept and role constructs:

Note that, consistently with the semantics of OWL2QL, we do not make the unique name assumption (UNA), i.e., we allow distinct constants a, b ∈ Na to be interpreted as the same object, i.e., aI = bI . Note also that labeled nulls are not interpreted by I.

Let I = 〈∆I , ·I 〉 be an interpretation over a signature Σ. Then I is said to satisfy a concept inclusion B ⊑ C over Σ, denoted by I |= B ⊑ C, if BI ⊆ C I ; I is said to satisfy a role inclusion R ⊑ Q over Σ, denoted by I |= R ⊑ Q, if RI ⊆ QI ; and I is said to satisfy a TBox T over Σ, denoted by I |= T , if I |= α for every α ∈ T . Moreover, satisfaction of membership assertions over Σ is defined as follows. A substitution over I is a function h : (Na ∪Nℓ) → ∆I such that h(a) = aI for every a ∈ Na. Then I is said to satisfy an (extended) ABox A, denoted by I |= A, if there exists a substitution h over I such that:

• for every B(u) ∈ A, it holds that h(u) ∈ BI ; and
• for every R(u, v) ∈ A, it holds that (h(u), h(v)) ∈ RI . Finally, I is said to satisfy a(n extended) KB K = 〈T ,A〉, denoted by I |= K, if I |= T and I |= A. Such I is called a model of K, and we use MOD(K) to denote the set of all models of K. We say that K is consistent if MOD(K) ̸= ∅.

As is customary, given an (extended) KB K over a signature Σ and a membership assertion or an inclusion α over Σ, we use notation K |= α to indicate that for every interpretation I of Σ, if I |= K, then I |= α.

2.1 Queries and certain answers

A k-ary query q over a signature Σ, with k ≥ 0, is a function that maps every interpretation 〈∆I , ·I 〉 of Σ into a k-ary relation qI ⊆ (∆I )k . In particular, if k = 0, then q is said to be a Boolean query, and qI is either a relation containing the empty tuple () (representing the value true) or the empty relation (representing the value false). Given a KB K over Σ, the set of certain answers to q over K, denoted by cert (q, K), is defined as:

Notice that the certain answer to a query does not contain labeled nulls. Besides, notice that if q is a Boolean query, then cert(q,K) evaluates to true if qI evaluates to true for every I ∈ MOD(K), and it evaluates to false otherwise.

A conjunctive query (CQ) over a signature Σ is a formula of the form q(⃗x) = ∃⃗y. ϕ(⃗x, ⃗y), where ⃗x, ⃗y are tuples of variables and ϕ(⃗x, ⃗y) is a conjunction of atoms of the form A(t), with A a concept name in Σ, and P (t, t′ ), with P a role name in Σ, where each of t, t′ is either a constant from Na or a variable from ⃗x or ⃗y. Given an interpretation I = 〈∆I , ·I 〉 of Σ, the answer of q over I, denoted by qI , is the set of tuples ⃗a of elements from ∆I for which there exist a tuple ⃗b of elements from ∆I such that I satisfies every conjunct in ϕ(⃗a,⃗b). A union of conjunctive queries (UCQ) over a signature Σ is a formula of the form q(⃗x) = ∨ni=1 qi(⃗x), where each qi (1 ≤ i ≤ n) is a CQ over Σ, whose semantics is defined as qI = ⋃ni=1 qI i .

3 Exchanging OWL2QLKnowledge Bases

We generalize now, in Section 3.1, the setting proposed in [Arenas et al., 2011] to OWL2QL, and we formalize in Section 3.2 the main problems studied in the rest of the paper.

3.1 A knowledge base exchange framework for OWL 2 QL

Assume that Σ1, Σ2 are signatures with no concepts or roles in common. An inclusion E1 ⊑ E2 is said to be from Σ1 to Σ2, if E1 is a concept or a role over Σ1 and E2 is a concept or a role over Σ2. A mapping is a tuple M = (Σ1, Σ2, T12), where T12 is a TBox consisting of inclusions from Σ1 to Σ2 [Arenas et al., 2012a]. Recall that in this paper, we deal with DL-LiteR TBoxes only, so T12 is assumed to be a set of DL-LiteR concept and role inclusions. The semantics of such a mapping is defined in [Arenas et al., 2012a] in terms of a notion of satisfaction for interpretations, which has to be extended in our case to deal with interpretations not satisfying the UNA (and, more generally, the standard name assumption). More specifically, given interpretations I, J of Σ1 and Σ2, respectively, pair (I,J) satisfies TBox T12, denoted by (I, J ) |= T12, if (i) for every a ∈ Na, it holds that aI = aJ , (ii) for every concept inclusion B ⊑ C ∈ T12, it holds that BI ⊆ C J , and (iii) for every role inclusion R ⊑ Q ∈ T12, it holds that RI ⊆ QJ . Notice that the connection between the information in I and J is established through the constants that move from source to target according to the mapping. For this reason, we require constants to be interpreted in the same way in I and J , i.e., they preserve their meaning when they are transferred. Besides, notice that this is the only restriction imposed on the domains of I and J (in particular, we require neither that ∆I = ∆J nor that ∆I ⊆ ∆J ). Finally, SATM(I) is defined as the set of interpretations J of Σ2 such that (I, J ) |= T12, and given a set X of interpretations of Σ1, SATM(X) is defined as ⋃I∈X SATM(I).

The main problem studied in the knowledge exchange area is the problem of translating a KB according to a mapping, which is formalized through several different notions of translation (for a thorough comparison of different notions of solutions see [Arenas et al., 2012a]). The first such notion is the concept of solution, which is formalized as follows. Given a mapping M = (Σ1, Σ2, T12) and KBs K1, K2 over Σ1 and Σ2, respectively, K2 is a solution for K1 under M if MOD(K2) ⊆ SATM(MOD(K1)). Thus, K2 is a solution for K1 under M if every interpretation of K2 is a valid translation of an interpretation of K1 according to M. Although natural, this is a mild restriction, which gives rise to the stronger notion of universal solution. Given M, K1 and K2 as before, K2 is a universal solution for K1 under M if MOD(K2) = SATM(MOD(K1)). Thus, K2 is designed to exactly represent the space of interpretations obtained by translating the interpretations of K1 under M [Arenas et al., 2012a]. Below is a simple example demonstrating the notion of universal solutions. This example also illustrates some issues regarding the absence of the UNA, which has to be given up to comply with the OWL 2 QL standard, and regarding the use of disjointness assertions.

Example 3.1 Assume M = ({F(·),G(·)}, {F ′ (·),G′ (·)}, T12), where T12 = {F ⊑ F ′ ,G ⊑ G′ }, and let K1 = 〈T1,A1〉, where T1 = {} and A1 = {F(a),G(b)}. Then the ABox A2 = {F ′ (a), G′ (b)} is a universal solution for K1 under M.

Now, if we add a seemingly harmless disjointness assertion {F ⊑ ¬G} to T1, we obtain that A2 is no longer a universal solution (not even a solution) for K1 under M. The reason for that is the lack of the UNA on the one hand, and the presence of the disjointness assertion in T1 on the other hand. In fact, the latter forces a and b to be interpreted differently in the source. Thus, for a model J of A2 such that aJ = bJ and F ′J = G′J = {aJ }, there exists no model I of K1 such that (I,J) |= T12 (which would require aI = aJ and bI = bJ ). In general, there exists no universal solution for K1 under M, even though K1 and T12 are consistent with each other.

A second class of translations is obtained in [Arenas et al., 2012a] by observing that solutions and universal solutions are too restrictive for some applications, in particular when one only needs a translation storing enough information to properly answer some queries. For the particular case of UCQ, this gives rise to the notions of UCQ-solution and universal UCQ-solution. Given a mapping M = (Σ1, Σ2, T12), a KB K1 = 〈T1, A1〉 over Σ1 and a KB K2 over Σ2, K2 is a UCQsolution for K1 under M if for every query q ∈ UCQ over Σ2: cert(q, 〈T1 ∪ T12,A1〉) ⊆ cert(q,K2), while K2 is a universal UCQ-solution for K1 under M if for every query q ∈ UCQ over Σ2: cert (q, 〈T1 ∪ T12, A1〉) = cert (q, K2).

Finally, a last class of solutions is obtained in [Arenas et al., 2012a] by considering that users want to translate as much of the knowledge in a TBox as possible, as a lot of effort is put in practice when constructing a TBox. This observation gives rise to the notion of UCQ-representation [Arenas et al., 2012a], which formalizes the idea of translating a source TBox according to a mapping. Next, we present an alternative formalization of this notion, which is appropriate for our setting where disjointness assertions are considered. 1 Assume that M = (Σ1, Σ2, T12) and T1, T2 are TBoxes over Σ1 and Σ2, respectively. Then T2 is a UCQ-representation of T1 under M if for every query q ∈ UCQ over Σ2 and every ABox A1 over Σ1 that is consistent with T1:

Notice that in the previous definition, A2 is said to be a UCQsolution for A1 under M if the KB 〈∅, A2〉 is a UCQ-solution for the KB 〈∅,A1〉 under M. Let us explain the intuition behind the definition of the notion of UCQ-representation. Assume that T1, T2, M satisfy (†). First, T2 captures the information in T1 that is translated by M and that can be extracted by using a UCQ, as for every ABox A1 over Σ1 that is consistent with T1 and every UCQ q over Σ2, if we choose an arbitrary UCQ-solution A2 for A1 under M, then it holds that cert (q, 〈T1 ∪T12, A1〉) ⊆ cert (q, 〈T2, A2〉). Notice that A1 is required to be consistent with T1 in the previous condition, as we are interested in translating data that make sense according to T1. Second, T2 does not include any piece of information that can be extracted by using a UCQ and it is not the result of translating the information in T1 according to M. In fact, if A1 is an ABox over Σ1 that is consistent with T1 and q is a UCQ over Σ2, then it could be the case that cert(q, 〈T1 ∪ T12,A1〉) ⊊ cert(q, 〈T2,A⋆2 〉) for some UCQ-solution A⋆2 for A1 under M. However, the extra tuples extracted by query q are obtained from the extra information in A⋆2 , as if we consider a tuple ⃗a that belong to cert(q, 〈T2,A2〉) for every UCQ-solution A2 for A1 under M, then it holds that ⃗a ∈ cert(q, 〈T1 ∪ T12, A1〉).

Example 3.2 Assume that M = ({F(·),G(·),H(·),D(·)}, {F ′ (·),G′ (·),H′ (·)}, T12), where T12 = {F ⊑ F ′ ,G ⊑ G′ ,H ⊑ H′}, and let T1 = {F ⊑ G}. As expected, TBox T2 = {F ′ ⊑ G′} is a UCQ-representation of T1 under M. Moreover, we can add the inclusion D ⊑ ¬H′ to T12, and T2 will still remain a UCQ-representation of T1 under M. Notice that in this latter setting, our definition has to deal with some ABoxes A1 that are consistent with T1 but not with T1 ∪ T12, for instance A1 = {H(a),D(a)} for some constant a. In those cases, Equation (†) is trivially satisfied, since MOD(〈T1 ∪ T12,A1〉) = ∅ and the set of UCQ-solutions for A1 under M is empty.

3.2 On the problem of computing solutions

Arguably, the most important problem in knowledge exchange [Arenas et al., 2011; 2012a], as well as in data exchange [Fagin et al., 2005; Kolaitis, 2005], is the task of computing a translation of a KB according to a mapping. To study the computational complexity of this task for the different notions of solutions presented in the previous section, we introduce the following decision problems. The membership problem for universal solutions (resp. universal UCQsolutions) has as input a mapping M = (Σ1,Σ2, T12) and KBs K1, K2 over Σ1 and Σ2, respectively. Then the question to answer is whether K2 is a universal solution (resp. universal UCQ-solution) for K1 under M. Moreover, the membership problem for UCQ-representations has as input a mapping M = (Σ1, Σ2, T12) and TBoxes T1, T2 over Σ1 and Σ2, respectively, and the question to answer is whether T2 is a UCQ-representation of T1 under M.

1 If disjointness assertions are not allowed, then this new notion can be shown to be equivalent to the original formalization of UCQrepresentation proposed in [Arenas et al., 2012a].

In our study, we cannot leave aside the existential versions of the previous problems, which are directly related with the problem of computing translations of a KB according to a mapping. Formally, the non-emptiness problem for universal solutions (resp. universal UCQ-solutions) has as input a mapping M = (Σ1, Σ2, T12) and a KB K1 over Σ1. Then the question to answer is whether there exists a universal solution (resp. universal UCQ-solution) for K1 under M. Moreover, the non-emptiness problem for UCQ-representations has as input a mapping M = (Σ1, Σ2, T12) and a TBox T1 over Σ1, and the question to answer is whether there exists a UCQrepresentation of T1 under M.

4 Our contributions

In Section 3.2, we have introduced the problems that are studied in this paper. It is important to notice that these problems are defined by considering only KBs (as opposed to extended KBs), as they are the formal counterpart of OWL2QL. Nevertheless, as shown in Section 5, there are natural examples of OWL 2 QL specifications and mappings where null values are needed when constructing solutions. Thus, we also study the problems defined in Section 3.2 in the case where translations can be extended KBs. It should be noticed that the notions of solution, universal solution, UCQ-solution, universal UCQ-solution, and UCQ-representation have to be enlarged to consider extended KBs, which is straightforward to do. In particular, given a mapping M = (Σ1, Σ2, T12) and TBoxes T1, T2 over Σ1 and Σ2, respectively, T2 is said to be a UCQrepresentation of T1 under M in this extended setting if in Equation (†), A2 is an extended ABox over Σ2 that is a UCQsolution for A1 under M.

The main contribution of this paper is to provide a detailed analysis of the complexity of the membership and non-emptiness problems for the notions of universal solution and UCQ-representation. In Figure 1, we provide a summary of the main results in the paper, which are explained in more detail in Sections 5 and 6. It is important to notice that these results considerably extend the previous known results about these problems [Arenas et al., 2012a; 2012b]. In the first place, the problem of computing universal solutions was studied in [Arenas et al., 2012a] for the case of DL-LiteRDFS , a fragment of DL-LiteR that allows neither for inclusions of the form B ⊑ ∃R nor for disjointness assertions. In that case, it is straightforward to show that every source KB has a universal solution that can be computed by using the chase procedure [Calvanese et al., 2007]. Unfortunately, this result does not provide any information about how to solve the much larger case considered in this paper, where, in particular, the non-emptiness problem is not trivial. In fact, for the case of the notion of universal solution, all the lower and upper bounds provided in Figure 1 are new results, which are not consequences of the results obtained in [Arenas et al., 2012a]. In the second place, a notion of UCQ-representation that is appropriate for the fragment of DL-LiteR not including disjointness assertions was studied in [Arenas et al., 2012a; 2012b]. In particular, it was shown that the membership and non-emptiness problems for this notion are solvable in polynomial time. In this paper, we considerably strengthen these results: (i) by generalizing the definition of the notion of UCQ-representation to be able to deal with OWL2QL, that is, with the entire language DL-LiteR (which includes disjointness assertions); and (ii) by showing that the membership and non-emptiness problems are both NLOGSPACE-complete in this larger scenario.

It turns out that reasoning about universal UCQ-solutions is much more intricate. In fact, as a second contribution of our paper, we provide a PSPACE lower bound for the complexity of the membership problem for the notion of universal UCQ-solution, which is in sharp contrast with the NP and NLOGSPACE upper bounds for this problem for the case of universal solutions and UCQ-representations, respectively (see Figure 1). Although many questions about universal UCQ-solutions remain open, we think that this is an interesting first result, as universal UCQ-solutions have only been investigated before for the very restricted fragment DL-LiteRDFS of DL-LiteR [Arenas et al., 2012a], which is described in the previous paragraph.

5 Computing universal solutions

In this section, we study the membership and non-emptiness problems for universal solutions, in the cases where nulls are not allowed (Section 5.1) and are allowed (Section 5.2) in such solutions. But before going into this, we give an example that shows the shape of universal solutions in DL-LiteR.

Example 5.1 Assume that M = ({F(·), S(·, ·)}, {G′ (·)}, {∃S- ⊑ G′}), and let K1 = 〈T1,A1〉, where T1 = {F ⊑ ∃S} and A1 = {F(a)}. Then a natural way to construct a universal solution for K1 underMis to 'populate' the target with all implied facts (as it is usually done in data exchange). Thus, the ABox A2 = {G′ (n)}, where n is a labeled null, is a universal solution for K1 under M if nulls are allowed. Notice that here, a universal solution with non-extended ABoxes does not exist: substituting n by any constant is too restrictive, ruining universality.

T1 = {F ⊑ ∃S, ∃S- ⊑ ∃S} and A1 = {F(a), T(a, a)}. In this case, we cannot use the same approach as in Example 5.1 to construct a universal solution, as now we would need of an infinite number of labeled nulls to construct such a solution. However, as S and T are transferred to the same role S′ , it is possible to use constant a to represent all implied facts. In particular, in this case A2 = {S′ (a, a)} is a universal solution for K1 underM.

5.1 Universal solutions without null values

We explain here how the NP upper bound for the nonemptiness problem for universal solutions is obtained, when ABoxes are not allowed to contain null values.

Assume given a mapping M = (Σ1, Σ2, T12) and a KB K1 = 〈T1,A1〉 over Σ1. To check whether K1 has a universal solution under M, we use the following non-deterministic polynomial-time algorithm. First, we construct an ABox A2 over Σ2 containing every membership assertion α such that 〈T1 ∪ T12,A1〉 |= α, where α is of the form either B(a) or R(a, b), and a, b are constants mentioned in A1. Second, we guess an interpretation I of Σ1 such that I |= K1 and (I, UA2 ) |= T12, where UA2 is the interpretation of Σ2 naturally corresponding 2 to A2. The correctness of the algorithm is a consequence of the facts that:

1. there exists a universal solution for A1 under M if and only if A2 is a solution for A1 under M; and
2. A2 is a solution for A1 under M if and only if there exists a model I of K1 such that (I, UA2 ) |= T12.

Moreover, the algorithm can be implemented in a nondeterministic polynomial-time Turing machine given that: (i) A2 can be constructed in polynomial time; (ii) if there exists a model I of K1 such that (I, UA2 ) |= T12, then there exists a model of K1 of polynomial-size satisfying this condition; and (iii) it can be checked in polynomial time whether I |= K1 and (I, UA2 ) |= T12.

In addition, in this case, the membership problem can be reduced to the non-emptiness problem, thus, we have that:

Theorem 5.3 The non-emptiness and membership problems for universal solutions are in NP.

The exact complexity of these problems remains open. In fact, we conjecture that these problems are in PTIME.

We conclude by showing that reasoning about universal UCQ-solutions is harder than reasoning about universal solutions, which can be explained by the fact that TBoxes have bigger impact on the structure of universal UCQ-solutions rather than of universal solutions. In fact, by using a reduction from the validity problem for quantified Boolean formulas, similar to a reduction in [Konev et al., 2011], we are able to prove the following:

2 Interpretation UA2 can be defined as the Herbrand model of A2 extended with fresh domain elements to satisfy assertions of the form ∃R(a) in A2.

Theorem 5.4 The membership problem for universal UCQsolutions is PSPACE-hard.

5.2 Universal solutions with null values

We start by considering the non-emptiness problem for universal solutions with null values, that is, when extended ABoxes are allowed in universal solutions. As our first result, similar to the reduction above, we show that this problem is PSPACE-hard, and identify the inclusion of inverse roles as one of the main sources of complexity.

To obtain an upper bound for this problem, we use twoway alternating automata on infinite trees (2ATA), which are a generalization of nondeterministic automata on infinite trees [Vardi, 1998] well suited for handling inverse roles in DL-LiteR. More precisely, given a KB K, we first show that it is possible to construct the following automata:

• Acan K is a 2ATA that accepts trees corresponding to the canonical model of K 3 with nodes arbitrary labeled with a special symbol G;
• Amod K is a 2ATA that accepts a tree if its subtree labeled with G corresponds to a tree model I of K (that is, a model forming a tree on the labeled nulls); and
• Afin is a (one-way) non-deterministic automaton that accepts a tree if it has a finite prefix where each node is marked with G, and no other node in the tree is marked with G.

Then to verify whether a KB K1 = 〈T1,A1〉 has a universal solution under a mapping M = (Σ1, Σ2, T12), we solve the non-emptiness problem for an automaton B defined as the product automaton of πΓK (Acan K ), πΓK (Amod K ) and Afin, where K = 〈T1 ∪ T12,A1〉, πΓK (Acan K ) is the projection of Acan K on a vocabulary ΓK not mentioning symbols from Σ1, and likewise for πΓK (Amod K ). If the language accepted by B is empty, then there is no universal solution for K1 under M, otherwise a universal solution (possibly of exponential size) exists, and we can compute it by extracting the ABox encoded in some tree accepted by B . Summing up, we get:

Theorem 5.5 If extended ABoxes are allowed in universal solutions, then the non-emptiness problem for universal solutions is PSPACE-hard and in EXPTIME.

Interestingly, the membership problem can be solved more efficiently in this scenario, as now the candidate universal solutions are part of the input. In the following theorem, we pinpoint the exact complexity of this problem.

Theorem 5.6 If extended ABoxes are allowed in universal solutions, then the membership problem for universal solutions is NP-complete.

3 If K = 〈T ,A〉, then this model essentially corresponds to the chase of Awith T (see [Konev et al., 2011] for a formal definition).

6 Computing UCQ-representations

In Section 5, we show that the complexity of the membership and non-emptiness problems for universal solutions differ depending on whether ABoxes or extended ABoxes are considered. On the other hand, we show in the following proposition that the use of null values in ABoxes does not make any difference in the case of UCQ-representations. In this proposition, given a mapping M and TBoxes T1, T2, we say that T2 is a UCQ-representation of T1 under M considering extended ABoxes if T1, T2, M satisfy Equation (†) in Section 3.1, but assuming that A2 is an extended ABox over Σ2 that is a UCQ-solution for A1 underM.

Proposition 6.1 A TBox T2 is a UCQ-representation of a TBox T1 under a mapping M if and only if T2 is a UCQrepresentation of T1 under M considering extended ABoxes.

Thus, from now on we study the membership and nonemptiness problems for UCQ-representations assuming that ABoxes can contain null values.

We start by considering the membership problem for UCQrepresentations. In this case, one can immediately notice some similarities between this task and the membership problem for universal UCQ-solutions, which was shown to be PSPACE-hard in Theorem 5.4. However, the universal quantification over ABoxes in the definition of the notion of UCQrepresentation makes the latter problem computationally simpler, which is illustrated by the following example.

Example 6.2 Assume that M = (Σ1,Σ2, T12), where Σ1 = {F(·), S1(·, ·), S2(·, ·), T1(·, ·), T2(·, ·)}, Σ2 = {F ′ (·), S′ (·, ·), T ′ (·, ·),G′ (·)} and T12 = {F ⊑ F ′ , S1 ⊑ S′ , S2 ⊑ S′ , T1 ⊑ T ′ , T2 ⊑ T ′ , ∃T - 1 ⊑ G′}. Moreover, assume that T1 = {F ⊑ ∃S1, F ⊑ ∃S2, ∃S1 ⊑ ∃T1, ∃S2 ⊑ ∃T2} and T2 = {F ′ ⊑ ∃S′ , ∃S′- ⊑ ∃T ′ , ∃T ′- ⊑ G′}. If we were to verify whether 〈T2, {F ′ (a)}〉 is a universal UCQ-solution for 〈T1, {F(a)}〉 under M (which it is in this case), then we would first need to construct the path π = 〈F ′ (a), S′ (a, n), T ′ (n,m),G′ (m)〉 formed by the inclusions in T2, where n,m are fresh null values, and then we would need to explore the translations according toMof all paths formed by the inclusions in T1 to find one that matches π.

On the other hand, to verify whether T2 is a UCQrepresentation of T1 under M, one does not need to execute any "backtracking", as it is sufficient to consider independently a polynomial number of pieces C taken from the paths formed by the inclusions in T1, each of them of polynomial size, and then checking whether the translation C ′ of C according toMmatches with the paths formed from C ′ by the inclusions in T2. If any of these pieces does not satisfy this condition, then it can be transformed into a witness that Equation (†) is not satisfied, showing that T2 is not a UCQrepresentation of T1 under M (as we have a universal quantification over the ABoxes over Σ1 in the definition of UCQrepresentations). In fact, one of the pieces considered in this case is C = 〈T2(n,m)〉, where n, m are null values, which does not satisfy the previous condition as the translation C ′ of C according toM is 〈T ′ (n,m)〉, and this does not match with the path 〈T ′ (n, m), G′ (m)〉 formed from C ′ by the inclusions in T2. This particular case is transformed into an ABox A1 = {T2(b, c)} and a query q = T ′ (b, c) ∧ G′ (c), where b, c are fresh constants, for which we have that Equation (†) is not satisfied.

Notice that disjointness assertions in the mapping may cause 〈T1 ∪ T12, A1〉 to become inconsistent for some source ABoxes A1 (which will make all possible tuples to be in the answer to every query), therefore additional conditions have to be imposed on T2. To give more intuition about how the membership problem for UCQ-representations is solved, we give an example showing how one can deal with some of these inconsistency issues.

Example 6.3 Assume that M = (Σ1, Σ2, T12), where Σ1 = {F(·),G(·),H(·)}, Σ2 = {F ′ (·),G′ (·),H′ (·)} and T12 = {F ⊑ F ′ ,G ⊑ G′ ,H ⊑ H′}. Moreover, assume that T1 = {F ⊑ G} and T2 = {F ′ ⊑ G′}. In this case, it is clear that T2 is a UCQ-representation of T1 under M. However, if we add inclusion H ⊑ ¬G′ to T12, then T2 is no longer a UCQrepresentation of T1 under M. To see why this is the case, consider an ABox A1 = {F(a),H(a)}, which is consistent with T1, and a query q = F ′ (b), where b is a fresh constant. Then we have that cert(q, 〈T1 ∪ T12,A1〉) = {()} as KB 〈T1 ∪ T12,A1〉 is inconsistent, while cert(q, 〈T2,A2〉) = ∅ for UCQ-solution A2 = {F ′ (a),H′ (a)} for A1 under M. Thus, we conclude that Equation (†) is violated in this case.

One can deal with the issue raised in the previous example by checking that on every pair (B,B′ ) of T1-consistent basic concepts over Σ1, 4 it holds that: (B,B′ ) is (T1 ∪ T12)- consistent if and only if (B,B′ ) is (T12 ∪T2)-consistent, and likewise for every pair of basic roles over Σ1. This condition guarantees that for every ABox A1 over Σ1 that is consistent with T1, it holds that: 〈T1 ∪T12,A1〉 is consistent if and only if there exists an extended ABox A2 over Σ2 such that A2 is a UCQ-solution for A1 under M and 〈T2,A2〉 is consistent. Thus, the previous condition ensures that the sets on the leftand right-hand side of Equation (†) coincide whenever the intersection on either of these sides is taken over an empty set.

The following theorem, which requires of a lengthy and non-trivial proof, shows that there exists an efficient algorithm for the membership problem for UCQ-representations that can deal with all the aforementioned issues.

Theorem 6.4 The membership problem for UCQrepresentations is NLOGSPACE-complete.

We conclude by pointing out that the non-emptiness problem for UCQ-representations can also be solved efficiently. We give an intuition of how this can be done in the following example, where we say that T1 is UCQ-representable under M if there exists a UCQ-representation T2 of T1 under M.

Example 6.5 Assume that M = (Σ1, Σ2, T12), where Σ1 = {F(·),G(·),H(·)}, Σ2 = {F ′ (·),G′ (·)} and T12 = {F ⊑ F ′ ,G ⊑ G′ ,H ⊑ F ′}. Moreover, assume that T1 = {F ⊑ G}. Then it follows that T1 ∪ T12 |= F ⊑ G′ , and in order for T1 to be UCQ-representable under M, the following condition must be satisfied:

4 A pair (B,B)′ is T -consistent for a TBox T , if the KB 〈T , {B(a), B′ (a)}〉 is consistent, where a is an arbitrary constant.

• (⋆) there exists a concept B′ over Σ2 s.t. T12 |= F ⊑ B′ , and for each concept B over Σ1 with T1∪T12 |= B ⊑ B′ it follows that T1 ∪ T12 |= B ⊑ G′ .

The idea is then to add the inclusion B′ ⊑ G′ to a UCQrepresentation T2 so that T12 ∪ T2 |= F ⊑ G′ as well. In our case, concept F ′ satisfies the condition T12 |= F ⊑ F ′ , but it does not satisfy the second requirement as T1 ∪ T12 |= H ⊑ F ′ and T1 ∪ T12 ̸|= H ⊑ G′ . In fact, F ′ ⊑ G′ cannot be added to T2 as it would result in T12 ∪ T2 |= H ⊑ G′ , hence in Equation (†), the inclusion from right to left would be violated. There is no way to reflect the inclusion F ⊑ G′ in the target, so in this case T1 is not UCQ-representable under M.

The proof of the following result requires of some involved extensions of the techniques used to prove Theorem 6.4.

Theorem 6.6 The non-emptiness problem for UCQrepresentations is NLOGSPACE-complete.

The techniques used to prove Theorem 6.6, which is sketched in the example below.

Example 6.7 ConsiderMand T1 from Example 6.5, but assuming that T12 does not contain the inclusion H ⊑ F ′ . Again, T1 ∪ T12 |= F ⊑ G′ , but now condition (⋆) is satisfied. Then, an algorithm for computing a representation essentially needs to take any B′ given by condition (⋆) and add the inclusion B′ ⊑ F ′ to T2. In this case, T2 = {F ′ ⊑ G′} is a UCQ-representation of T1 under M.

7 Conclusions

In this paper, we have studied the problem of KB exchange for OWL2QL, improving on previously known results with respect to both the expressiveness of the ontology language and the understanding of the computational properties of the problem. Our investigation leaves open several issues, which we intend to address in the future. First, it would be good to have characterizations of classes of source KBs and mappings for which universal (UCQ-)solutions are guaranteed to exist. As for the computation of universal solutions, while we have pinned-down the complexity of membership for extended ABoxes as NP-complete, an exact bound for the other case is still missing. Moreover, it is easy to see that allowing for inequalities between terms (e.g., a ̸= b in Example 3.1) and for negated atoms in the (target) ABox would allow one to obtain more universal solutions, but a full understanding of this case is still missing. Finally, we intend to investigate the challenging problem of computing universal UCQ-solutions, adopting also here an automata-based approach.

8 Acknowledgements

This research has been partially supported by the EU IP project Optique (grant FP7-318338), by EU Marie Curie action FP7-PEOPLE-2009-IRSES (grant 24761), by ERC grant agreement DIADEM, no. 246858, and by Fondecyt grant 1131049. Diego Calvanese has been partially supported by the Wolfgang Pauli Institute Vienna. The authors are also grateful to Evgeny Sherkhonov and Roman Kontchakov for helpful comments and discussions.