Query Inseparability by Games E. Botoeva1 , R. Kontchakov2 , V. Ryzhikov1 , F. Wolter3 , and M. Zakharyaschev2 1 KRDB Research Centre, Free University of Bozen-Bolzano, Italy {botoeva,ryzhikov}@inf.unibz.it 2 Department of Computer Science and Inf. Systems, Birkbeck, University of London, U.K. {roman,michael}@dcs.bbk.ac.uk 3 Department of Computer Science, University of Liverpool, U.K. wolter@liverpool.ac.uk Abstract. We investigate conjunctive query inseparability of description logic knowledge bases (KBs) with respect to a given signature, a fundamental prob- lem for KB versioning, module extraction, forgetting and knowledge exchange. We develop a game-theoretic technique for checking query inseparability of KBs expressed in fragments of Horn-ALCHI, and show a number of complexity re- sults ranging from P to E XP T IME and 2E XP T IME. We also employ our results to resolve two major open problems for OWL 2 QL by showing that TBox query in- separability and the membership problem for universal UCQ-solutions in knowl- edge exchange are both E XP T IME-complete for combined complexity. Introduction A description logic (DL) knowledge base (KB) consists of a terminological box (TBox), storing conceptual knowledge, and an assertion box (ABox), storing data. Typical ap- plications of KBs involve answering queries over incomplete data sources (ABoxes) augmented by ontologies (TBoxes) that provide additional information about the do- main of interest as well as a convenient vocabulary for user queries. The standard query language in such applications, which balances expressiveness and computational com- plexity, is the language of conjunctive queries (CQs). With typically large data, often tangled ontologies, and the hard problem of answer- ing CQs over ontologies, various transformation and comparison tasks are becoming indispensable for KB engineering and maintenance. For example, to make answering certain CQs more efficient, one may want to extract from a given KB a smaller module returning the same answers to those CQs as the original KB; to provide the user with a more convenient query vocabulary, one may want to reformulate the KB in a new lan- guage. These tasks are known as module extraction [19] and knowledge exchange [2]; other relevant tasks include versioning, revision and forgetting [10, 20, 15]. In this paper, we investigate the following relationship between KBs that is funda- mental for all such tasks. Let Σ be a signature consisting of concept and role names. We call KBs K1 and K2 Σ-query inseparable and write K1 ≡Σ K2 if any CQ formulated in Σ has the same answers over K1 and K2 .The relativisation to (smaller) signatures is crucial to support the tasks mentioned above: (versioning) When comparing two versions K1 and K2 of a KB with respect to their answers to CQs in a relevant signature Σ, the task is to check whether K1 ≡Σ K2 . (modularisation) A Σ-module of a KB K is a KB K0 ⊆ K such that K0 ≡Σ K. If we are only interested in answering CQs in Σ over K, then we can achieve our aim by querying any Σ-module of K instead of K itself. (knowledge exchange) In knowledge exchange, we want to transform a KB K1 in a signature Σ1 to a new KB K2 in a disjoint signature Σ2 connected to Σ1 via a declarative mapping specification given by a TBox T12 . Thus, the target KB K2 should satisfy the condition K1 ∪ T12 ≡Σ2 K2 , in which case it is called a universal UCQ-solution (CQ and UCQ inseparabilities coincide for Horn DLs). (forgetting) A KB K0 is the result of forgetting a signature Σ in a KB K if K0 does not use Σ and gives the same answers to CQs without symbols in Σ as K: that is, sig(K0 ) ⊆ sig(K) \ Σ and K0 ≡sig(K)\Σ K. We study the data and combined complexity of deciding Σ-query inseparability for KBs expressed in various fragments of the DL Horn-ALCHI [14], which include DL-LiteH core [7] and EL [3] underlying the W3C profiles OWL 2 QL and OWL 2 EL. To establish upper complexity bounds, we develop a novel game-theoretic technique for checking finite Σ-homomorphic embeddability between (possibly infinite) materi- alisations of KBs. For all of the considered DLs, Σ-query inseparability turns out to be P-complete for data complexity, which matches the data complexity of CQ evalua- tion for all of our DLs lying outside the DL-Lite family. For combined complexity, the obtained tight complexity results are summarised in the diagram below. 2E XP T IME arbitrary strategy E XP T IME Thms. 23, 25 Thms. 23, 25 E XP T IME Horn-ALCHI Thms. 12, 25 DL-LiteH horn Horn-ALCH Horn-ALCI DL-LiteH core P ELH Horn-ALC DL-Litehorn Thms. 16, 24 P DL-Litecore Thms. 12, 24 EL forward strategy backward+forward strategy Most interesting are E XP T IME-completeness of DL-LiteH core and 2E XP T IME -complete- ness of Horn-ALCI, which contrast with NP-completeness and E XP T IME-complete- ness of CQ evaluation for those logics. For DL-Lite without role inclusions and ELH, Σ-query inseparability is P-complete, while CQ evaluation is NP-complete. In general, it is the combined presence of inverse roles and qualified existential restrictions (or role inclusions) that makes Σ-query inseparability hard. We apply our results to resolve two important open problems. First, we show that the membership problem for universal UCQ-solutions in knowledge exchange for KBs in DL-LiteH core is E XP T IME -complete for combined complexity, which settles an open question of Arenas et al. [1], where only PS PACE-hardness was established. We also show that Σ-query inseparability of DL-LiteH core TBoxes is E XP T IME -complete, which closes the PS PACE–E XP T IME gap that was left open by Konev et al. [12]. Recall that TBoxes T1 and T2 are Σ-query inseparable if, for all Σ-ABoxes A (which only use concept and role names from Σ), the KBs (T1 , A) and (T2 , A) are Σ- query inseparable. TBox and KB inseparabilities have different applications. The for- mer supports ontology engineering when data is not known or changes frequently: one can equivalently replace one TBox with another only if they return the same answers to queries for every Σ-ABox. In contrast, KB inseparability is useful in applications where data is stable—such as knowledge exchange or variants of module extraction and for- getting with fixed data—in order to use the KB in a new application or as a compilation step to make CQ answering more efficient. As we show below, TBox and KB Σ-query inseparabilities also have different computational properties. All the omitted proofs can be found in the full version of the paper [6]. Preliminaries All the DLs for which we investigate KB Σ-query inseparability are Horn fragments of ALCHI. To define these DLs, we fix sequences of individual names ai , concept names Ai , and role names Pi , where i < ω. A role is either a role name Pi or an inverse role Pi− ; we assume that (Pi− )− = Pi . Concepts in the DLs ALCI, ALC, and EL are defined as usual. DL-Litehorn -concepts are constructed from concept names using the constructors >, ⊥, u, and ∃R.> and DL-Litecore -concepts are DL-Litehorn -concepts without u; in other words, they are basic concepts of the form ⊥, >, Ai or ∃R.>. For a DL L, an L-concept inclusion (CI) takes the form C v D, where C and D are L-concepts. An L-TBox, T , is a finite set of L-CIs. An ALCHI, DL-LiteH horn and DL-LiteH core TBox can also contain a finite number of role inclusions (RIs) R1 v R2 , where the Ri are roles. In ELH TBoxes, RIs have no inverse roles. DL-Lite TBoxes may also contain disjointness constraints B1 u B2 v ⊥ and R1 u R2 v ⊥, for basic concepts Bi and roles Ri . To introduce the Horn fragments of these DLs, we require the standard recursive definition [9, 11] of positive occurrences of a concept. A TBox T is Horn if no concept of the form C t D occurs positively in T , and no concept of the form ¬C or ∀R.C occurs negatively in T . In the DL Horn-L only Horn-L-TBoxes are allowed. An ABox, A, is a finite set of assertions of the form Ak (ai ) or Pk (ai , aj ). An L-TBox T and an ABox A together form an L knowledge base (KB) K = (T , A). The set of individual names in K is denoted by ind(K). The semantics for the DLs is defined in the usual way based on interpretations I = (∆I , ·I ) that comply with the unique name assumption: aIi 6= aIj for i 6= j [4]. We write I |= α in case an inclusion or assertion α is true in I. If I |= α, for all α ∈ T ∪ A, then I is a model of a KB K = (T , A); in symbols: I |= K. K is consistent if it has a model. K |= α means that I |= α for all I |= K. A conjunctive query (CQ) q(x) is a formula ∃y ϕ(x, y), where ϕ is a conjunction of atoms of the form Ak (z1 ) or Pk (z1 , z2 ) with zi ∈ x ∪ y. A tuple a in ind(K) (of the same length as x) is a certain answer to q(x) over K if I |= q(a) for all I |= K; in this case we write K |= q(a). A signature, Σ, is a set of concept and role names. By a Σ-concept, Σ-role, Σ-CQ, etc. we understand any concept, role, CQ, etc. constructed using the names from Σ. Definition 1. Let K1 and K2 be KBs and Σ a signature. Then K1 Σ-query entails K2 if K2 |= q(a) implies K1 |= q(a) for all Σ-CQs q(x) and all tuples a in ind(K2 ). And K1 and K2 are Σ-query inseparable if they Σ-query entail each other; in which case we write K1 ≡Σ K2 . Since Σ-query inseparability can be reduced to two Σ-query entailment checks, we can prove complexity upper bounds for entailment. Conversely, for most languages we have a semantically transparent reduction of Σ-query entailment to Σ-query inseparability: Theorem 2. For any of our DLs L containing EL or having role inclusions, Σ-query entailment for L-KBs is L OG S PACE-reducible to Σ-query inseparability for L-KBs. We now consider the relationship between inseparability and universal UCQ-solu- tions in knowledge exchange. Suppose K1 and K2 are KBs in disjoint signatures Σ1 and Σ2 . Let T12 be a mapping consisting of inclusions of the form S1 v S2 , where the Si are concept (or role) names in Σi . Then K2 is a universal UCQ-solution for (K1 , T12 , Σ2 ) if K1 ∪ T12 ≡Σ2 K2 . Deciding the latter is called the membership problem for universal UCQ-solutions. For DLs L with role inclusions, the problem whether K1 ∪T12 ≡Σ2 K2 is a Σ2 -query inseparability problem in L. Conversely, we have: Theorem 3. Σ-query entailment for any of our DLs L is L OG S PACE-reducible to the membership problem for universal UCQ-solutions in L. Semantic Characterisation In this section, we give a semantic characterisation of Σ-query entailment based on an abstract notion of materialisation and finite homomorphisms between such structures. Let K be a KB. An interpretation I is called a materialisation of K if K |= q(a) just in case I |= q(a), for all CQs q(x) and tuples a in ind(K). We say that K is materialisable if it has a materialisation. Materialisations can be used to characterise KB Σ-query entailment by means of Σ-homomorphisms. For an interpretation I and a signature Σ, the Σ-types tIΣ (x) and r IΣ (x, y) of x, y ∈ ∆I are defined by taking tIΣ (x) = { Σ-concept name A | x ∈ AI }, r IΣ (x, y) = { Σ-role R | (x, y) ∈ RI }. Suppose Ii is a materialisation of Ki , i = 1, 2. A function h : ∆I2 → ∆I1 is a Σ- homomorphism from I2 to I1 if, for any a ∈ ind(K2 ) and any x, y ∈ ∆I2 , – h(aI2 ) = aI1 whenever tIΣ2 (a) 6= ∅ or r IΣ2 (a, y) 6= ∅ for some y ∈ ∆I2 , and – tIΣ2 (x) ⊆ tIΣ1 (h(x)), r IΣ2 (x, y) ⊆ r IΣ1 (h(x), h(y)). As answers to Σ-CQs are preserved under Σ-homomorphisms, K1 Σ-query entails K2 if there is a Σ-homomorphism from I2 to I1 . However, the converse does not hold. Example 4. Suppose I2 and I2 Q Q Q I1 on the right are material- a u Q isations of KBs K2 and K1 , P R S T S T where a is the only ABox indi- x R R R vidual. Let Σ = {Q, R, S, T }. I1 Then there is no Σ-homo- T, Q S, Q T, Q S, Q a morphism from I2 to I1 (as r IΣ2 (a, u) = ∅, we can map u to, say, x but then only the shaded part of I2 can be mapped Σ-homomorphically to I1 ). However, for any Σ-query q(x), I2 |= q(c) implies I1 |= q(c) as any finite subinterpretation of I2 can be Σ-homomorphically mapped to I1 . We say that I2 is finitely Σ-homomorphically embeddable into I1 if, for every finite subinterpretation I20 of I2 , there exists a Σ-homomorphism from I20 to I1 . To prove the following theorem, one can regard any finite subinterpretation of I2 as a CQ whose variables are elements of ∆I2 , with the answer variables being in ind(K2 ). Theorem 5. Suppose Ki is a consistent KB with a materialisation Ii , i = 1, 2. Then K1 Σ-query entails K2 iff I2 is finitely Σ-homomorphically embeddable into I1 . One problem with applying Theorem 5 is that materialisations are in general infinite for any of the DLs considered in this paper. We address this problem by introducing finite representations of materialisations. Let K be a KB and let G = (∆G , ·G , ) be a finite structure such that ∆G = ind(K) ∪ Ω, for ind(K) ∩ Ω = ∅, ·G is an interpretation function on ∆G with AGi ⊆ ∆G , PiG ⊆ ind(K) × ind(K), and (∆G , ) is a directed graph (containing loops) with nodes ∆G and edges ⊆ ∆G × Ω, in which every edge u v is labelled with a set (u, v)G 6= ∅ of roles satisfying the condition: if u1 v and u2 v, then (u1 , v)G = (u2 , v)G. We call G a generating structure for K if the interpretation M defined below is a materialisation of K. A path in G is a sequence σ = u0 . . . un with u0 ∈ ind(K) and ui ui+1 for i < n. Let tail(σ) = un and let path(G) be the set of paths in G. The materialisation M is given by: ∆M = path(G), aM = a, for a ∈ ind(K), AM = {σ | tail(σ) ∈ AG }, P M = P G ∪ {(σ, σu) | tail(σ) u, P ∈ (tail(σ), u)G } ∪ {(σu, σ) | tail(σ) u, P − ∈ (tail(σ), u)G }. DL L has finitely generated materialisations if every L-KB has a generating structure. Theorem 6. Horn-ALCHI and all of its fragments defined above have finitely gener- ated materialisations. Moreover, – for any L ∈ {ALCHI, ALCI, ALCH, ALC} and any Horn-L KB (T , A), a gen- erating structure can be constructed in time |A| · 2p(|T |) , p a polynomial; – for any L in the EL and DL-Lite families introduced above and any L-KB (T , A), a generating structure can be constructed in time |A| · p(|T |), p a polynomial. Finite generating structures have been defined for EL [16], DL-Lite [13] and more expressive Horn DLs [8]. With the exception of DL-Lite, however, the relation guiding the construction of materialisations was implicit. We show how the existing constructions can be converted to generating structures in the full paper. Example 7. The materialisation Q− − I2 from Example 4 can be gen- Q T− P R− erated by the structure G2 shown G2 a S− on the right. S− For a generating structure G for K and a signature Σ, the Σ-types tGΣ (u) and r Σ (u, v) of u, v ∈ ∆G are defined by taking tGΣ (u) = { Σ-concept name A | u ∈ AG }, G r GΣ (u, v) as { Σ-role R | (u, v) ∈ RG } if u, v ∈ ind(K), as { Σ-role R | R ∈ (u, v)G } if u v, and ∅ otherwise, where (P − )G is the converse of P G . We also define r̄ GΣ (u, v) to contain the inverses of the roles in r GΣ (u, v); note that r̄ GΣ (u, v) is not the same as r GΣ (v, u). We write u Σ v if u v and r GΣ (u, v) 6= ∅. In the next section, we show that, for a DL L having finitely generated material- isations, Σ-query entailment for L-KBs can be reduced to the problem of finding a winning strategy in a game played on the generating structures for these KBs. Σ-Query Entailment by Games Suppose a DL L has finitely generated materialisations, Ki is a consistent L-KB, for i = 1, 2, and Σ a signature. Let Gi = (∆Gi , ·Gi , i ) be a generating structure for Ki and Mi be its materialisation; GiΣ and MΣ i denote the restrictions of Gi and Mi to Σ. We begin with a very simple game on the finite generating structure G2Σ and the possibly infinite materialisation MΣ1 . Infinite game GΣ (G2 , M1 ). This game is played by two players: player 2 and player 1. The states of the game are of the form si = (ui 7→ σi ), for i ≥ 0, where ui ∈ ∆G2 and σi ∈ ∆M1 satisfy the following condition: (s1 ) tGΣ2 (ui ) ⊆ tM Σ (σi ). 1 The game starts in a state s0 = (u0 7→ σ0 ) with σ0 = u0 in case u0 ∈ ind(K2 ). In each round i > 0, player 2 challenges player 1 with some ui ∈ ∆G2 such that ui−1 Σ 2 ui . Player 1 has to respond with a σi ∈ ∆M1 satisfying (s1 ) and (s2 ) r GΣ2 (ui−1 , ui ) ⊆ r M Σ (σi−1 , σi ). 1 This gives the next state si = (ui 7→ σi ). Note that of all the ui only u0 may be an ABox individual; however, there is no such a restriction on the σi . A play of length n ≥ 0 starting from s0 is any sequence s0 , . . . , sn of states obtained as described above. For an ordinal λ ≤ ω, we say that player 1 has a λ-winning strategy in the game GΣ (G2 , M1 ) starting from a state s0 if, for any play of length i < λ, which starts from s0 and conforms with this strategy, and any challenge of player 2 in round i+1, player 1 has a response. The following theorem gives a game-theoretic flavour to the criterion of Theorem 5 (see the full paper for a proof). Theorem 8. M2 is finitely Σ-homomorphically embeddable into M1 iff (abox) r M M1 Σ (a, b) ⊆ r Σ (a, b), for any a, b ∈ ind(K2 ), and, 2 (win) for any u0 ∈ ∆G2 and n < ω, there exists σ0 ∈ ∆M1 such that player 1 has an n-winning strategy in the game GΣ (G2 , M1 ) starting from (u0 7→ σ0 ). Example 9. Let Σ = Q− 4 {Q, R, S, T }. Consider G Σ − 3 2 T− G2Σ and MΣ 1 shown in u Q the picture on the right. a R− S− 0 1 2 S− 3 For any n < ω and σ 2 R R R u ∈ ∆G2 , player 1 has MΣ 4 1 an n-winning strategy in T, Q S, Q T, Q S, Q a GΣ (G2 , M1 ). A 4-winning strategy starting from (u 7→ σ) is shown by dotted lines (in round 2, player 2 has two possible challenges). For a larger n, a suitable σ can be chosen further away from the root a of M1 . The criterion of Theorem 8 does not seem to be a big improvement on Theorem 5 as we still have to deal with an infinite materialisation. Our aim now is to show that condition (win) in the infinite game GΣ (G2 , M1 ) can be checked by analysing a more complex game on the finite generating structures G2 and G1 . We consider four types of strategies in GΣ (G2 , M1 ). For each strategy type, τ , we define a game GτΣ (G2 , G1 ) such that, for any u0 ∈ ∆G2 , the following conditions are equivalent: (< ω) for every n < ω, player 1 has an n-winning τ -strategy in GΣ (G2 , M1 ) starting from some (u0 7→ σ0n ); (ω) player 1 has an ω-winning strategy in GτΣ (G2 , G1 ) starting from some state de- pending on u0 and τ . We begin with ‘forward’ winning strategies sufficient for DLs without inverse roles. Forward strategy and game GfΣ (G2 , G1 ). We say that a λ-strategy (λ ≤ ω) for player 1 in the game GΣ (G2 , M1 ) is forward if, for any play of length i−1 < λ, which conforms Σ with this strategy, and any challenge ui−1 2 ui by player 2, the response σi of player 1 is such that either σi−1 , σi ∈ ind(K1 ) or σi = σi−1 v, for some v ∈ ∆G1 . For example, if the Gi , i = 1, 2, satisfy the condition (f) the Σ-labels on i -edges contain no inverse roles, then every strategy in GΣ (G2 , M1 ) is forward. This is clearly the case for Horn-ALCH, Horn-ALC, ELH and EL, which by definition do not have inverse roles. The existence of a forward λ-winning strategy for player 1 in GΣ (G2 , M1 ) is equiv- alent to the existence of an ω-winning strategy in the game GfΣ (G2 , G1 ), which is de- fined similarly to GΣ (G2 , M1 ) but with two modifications: (1) it is played on G2 and G1 ; and (2) the response xi ∈ ∆G1 of player 1 to a challenge ui−1 Σ 2 ui must be such that either xi−1 , xi ∈ ind(K1 ) or xi−1 1 xi , and (s1 )–(s2 ) hold (with G1 and xi in place of M1 and σi ). Example 10. Let G2 and G1 be as R R Q shown on the right. Then, for any G2Σ a R u ∈ ∆G2 , there is x ∈ ∆G1 such R 0 1 that player 1 has an ω-winning 1 2 strategy in GfΣ (G2 , G1 ) starting G1Σ R Q a R from (u 7→ x). The next theorem follows from König’s Lemma: Lemma 11. For any u0 ∈ ∆G2 , condition (< ω) holds for forward strategies in GΣ (G2 , M1 ) iff (ω) holds in GfΣ (G2 , G1 ) for some state (u0 7→ x0 ). GfΣ (G2 , G1 ) is a standard simulation or reachability game on finite graphs, where the existence of ω-winning strategies for player 1 follows from the existence of n-winning strategies for n = O(|G2 | × |G1 |), which can be checked in polynomial time [18, 5]. By Theorem 6 and (f), we obtain: Theorem 12. For combined complexity, checking Σ-query entailment is in P for EL and ELH KBs, and in E XP T IME for Horn-ALC and Horn-ALCH KBs. For data com- plexity, it is in P for all these DLs. In comparison to forward strategies, the winning strategies used in Example 9 can be described as ‘backward.’ Backward strategy and game GbΣ (G2 , G1 ). A λ-strategy for player 1 in GΣ (G2 , M1 ) is backward if, for any play of length i − 1 < λ, which conforms with this strategy, and any challenge ui−1 Σ 2 ui by player 2, the response σi of player 1 is the immediate predecessor of σi−1 in M1 in the sense that σi−1 = σi v, for some v ∈ ∆G1 (player 1 loses in case σi−1 ∈ ind(K1 )). Note that, since M1 is tree-shaped, the response of 0 player 1 to any different challenge ui−1 Σ 2 ui must be the same σi ; cf. Example 9. b That is why the states of the game GΣ (G2 , G1 ) are of the form (Ξi 7→ xi ), where Ξi ⊆ ∆G2 , Ξi 6= ∅, and xi ∈ ∆G1 satisfy the following condition: (s01 ) tGΣ2 (u) ⊆ tGΣ1 (xi ), for all u ∈ Ξi . The game starts in a state (Ξ0 7→ x0 ) such that (s00 ) if u ∈ Ξ0 ∩ ind(K2 ), then x0 = u ∈ ind(K1 ). For each i > 0, player 2 always challenges player 1 with the set Ξi = Ξi−1 , where Ξ = {v ∈ ∆G2 | u Σ 2 v, for some u ∈ Ξ}, provided that it is not empty (otherwise, player 2 loses). Player 1 responds with xi ∈ ∆G1 such that xi 1 xi−1 and (s01 ) and the following condition hold: (s02 ) r GΣ2 (u, v) ⊆ r̄ GΣ1 (xi−1 , xi ), for all u ∈ Ξi−1 , v ∈ Ξi . Lemma 13. For any u0 ∈ ∆G2 , condition (< ω) holds for backward strategies in GΣ (G2 , M1 ) iff (ω) holds in GbΣ (G2 , G1 ) for some state ({u0 } 7→ x0 ). Although Lemmas 11 and 13 look similar, the game GbΣ (G2 , G1 ) turns out to be more complex than GfΣ (G2 , G1 ). v1 Example 14. To illustrate, con- a u v3 sider G2Σ shown on the right G2Σ v2 (with concepts and roles omitted) w2 w1 and an arbitrary G1 . A play in GbΣ (G2 , G1 ) may proceed as: ({u} 7→ x0 ), ({v1 , w1 } 7→ x1 ), ({v2 , w2 } 7→ x2 ), ({v3 , w1 } 7→ x3 ), etc. This gives at least 6 different sets Ξi . But if G2 contained k cy- cles of lengths p1 , . . . , pk , where pi is the ith prime number, then the number of states in GbΣ (G2 , G1 ) could be exponential (p1 × · · · × pk ). In fact, we have the following: Lemma 15. Checking (ω) in Lemma 13 is CO NP-hard. Observe that in the case of DL-Litecore and DL-Litehorn , (which have inverse roles but no RIs), generating structures G = (∆G , ·G , ) can be defined so that, for any u ∈ ∆G and R, there is at most one v with u v and R ∈ r G (u, v) [13]. As a result, any n-winning strategy starting from (u0 7→ σ0 ) in GΣ (G2 , M1 ) consists of a (possibly empty) backward part followed by a (possibly empty) forward part. Moreover, in the backward games for these DLs, the sets Ξi are always singletons. Thus, the number of states in the combined backward/forward games on the Gi is polynomial, and the existence of winning strategies can be checked in polynomial time. Theorem 16. Checking Σ-query entailment for DL-Litecore and DL-Litehorn KBs is in P for both combined and data complexity. An arbitrary strategy for player 1 in GΣ (G2 , M1 ) is a combination of a backward strategy and a number of start-bounded strategies to be defined next. Start-bounded strategy and game GsΣ (G2 , G1 ). A strategy for player 1 in the game GΣ (G2 , M1 ) starting from a state (u0 7→ σ0 ) is start-bounded if it never leads to (ui 7→ σi ) such that σ0 = σi v, for some v and i > 0. In other words, player 1 cannot use those elements of M1 that are located closer to the ABox than σ0 ; the ABox individuals in M1 can only be used if σ0 ∈ ind(K1 ). Example 17. The strategy G2Σ u20 T 1 W 2 W1− T1− starting from (u2 7→ σ1 ) and shown on the right is σ1 T, T1 W, W1 start-bounded. MΣ 1 4 3 In the game GsΣ (G2 , G1 ), player 1 will have to guess all the points of G2 that are mapped to the same point of M1 . The states of GsΣ (G2 , G1 ) are of the form (Γi , Ξi 7→ xi ), i ≥ 0, where Γi , Ξi ⊆ ∆ , Ξi 6= ∅, xi ∈ ∆G1 and (s01 ) holds. The initial state is of the form (∅, Ξ0 7→ x0 ) G2 such that (s00 ) holds. In each round i > 0, player 2 challenges player 1 with some u Σ 2 v such that u ∈ Ξi−1 and (nbk) if v ∈ Γi−1 then r GΣ2 (u, v) 6⊆ r̄ GΣ1 (xi−2 , xi−1 ). Player 1 responds with either a state (Ξi−1 , Ξi 7→ xi ) such that xi−1 1 xi (and so / ind(K1 )) and (s002 ) holds, or a state (∅, Ξi 7→ xi ) such that xi−1 , xi ∈ ind(K1 ) and xi ∈ (s002 ) r GΣ2 (u, v) ⊆ r GΣ1 (xi−1 , xi ). We make challenges u Σ 2 v, for which u ∈ Ξi−1 and (nbk) does not hold, ‘illegiti- mate’ because xi−2 can always be used as a response. Because of this, player 1 always moves ‘forward’ in G1 , but has to guess appropriate sets Ξi in advance. Note that Γi is always uniquely determined by xi−1 , xi and Ξi−1 (and it is either Ξi−1 or empty). Example 18. Let G2Σ and Σ u2 T u6 W u7 W1− u8 T1− u9 Σ G1 be as shown on the G2 1 0 right (cf. Example 17). a 0 1 2 We show that player 1 has x1 T, T1 x3 W, W1 x4 G1Σ an ω-winning strategy in GsΣ (G2 , G1 ) starting from (∅, {u2 , u9 } 7→ x1 ). Player 2 challenges with u2 Σ 2 u6 , and player 1 responds with ({u2 , u9 }, {u6 , u8 } 7→ x3 ). Then player 2 picks u6 Σ 2 u7 and player 1 responds with ({u6 , u8 }, {u7 } 7→ x4 ), where the game ends. Note the crucial guesses {u2 , u9 } 7→ x1 and {u6 , u8 } 7→ x3 made by player 1. If player 1 failed to guess that u8 must also be mapped to x3 and responded with ({u2 , u9 }, {u6 } 7→ x3 ), then after the challenge u6 Σ 2 u7 and response ({u6 }, {u7 } 7→ x4 )), player 2 would pick u7 Σ 2 u8 , to which player 1 could not respond. Lemma 19. For any u0 ∈ ∆G2 , condition (< ω) holds for start-bounded strategies in GΣ (G2 , M1 ) iff (ω) holds in GsΣ (G2 , G1 ) for some state (∅, Ξ0 7→ x0 ) with u0 ∈ Ξ0 . Arbitrary strategies and game GaΣ (G2 , G1 ). An arbitrary winning strategy in the game GΣ (G2 , M1 ) can be composed of one backward and a number of start-bounded strategies. u3 u4 − u5 Example 20. u1 u2 S U U− Σ Σ Consider G2 and G2 R− T u6 u7 u8 u9 u10 MΣ 1 shown on 0 the right. Starting W W1− T1− S1− MΣ σ2 R 1 1 2 2 from (u1 7→ σ2 ), 1 player 1 can respond σ4 σ3 σ S, S1 a U T1 1 b T, to the challenges W, W1 Σ Σ u1 2 u2 2 u3 according to the backward strategy; the challenges u2 Σ 2 u6 Σ 2 u7 Σ 2 u8 Σ 2 Σ u9 according to the start-bounded strategy as in Example 17; the challenges u3 2 u4 Σ 2 u5 also according to the obvious start-bounded strategy; finally, the challenge u9 Σ 2 u10 needs a response according to the backward strategy. We will combine the two backward strategies into a single one, but keep the start-bounded ones separate. The game GaΣ (G2 , G1 ) begins as the game GbΣ (G2 , G1 ), but with states of the form (Ξi 7→ xi , Ψi ), i ≥ 0, where Ξi ⊆ ∆G2 and xi ∈ ∆G1 satisfy (s01 ) and Ψi is a (possibly empty) subset of Ξi , which indicates initial challenges in start-bounded games. The initial state satisfies (s00 ). In each round i > 0, if xi−1 ∈ ind(K1 ) then player 2 launches the start-bounded game GsΣ (G2 , G1 ) with the initial state (∅, Ξi−1 7→ xi−1 ). Otherwise, if xi−1 ∈ / ind(K1 ), player 2 has two options. First, he can challenge player 1 with the set Ψi−1 (that is, similar to the backward game but with a possibly smaller Ψi−1 in place of Ξi−1 ); player 1 responds to this challenge with a state (Ξi 7→ xi , Ψi ) such that Ψi−1 ⊆ Ξi , xi 1 xi−1 and (s02 ) holds. Second, player 2 can launch the start-bounded game GsΣ (G2 , G1 ) with the initial state (∅, Ξi−1 7→ xi−1 ), where the first challenge of player 2 must be picked from Φi−1 = Ξi−1 \ Ψi−1 . Example 21. We illustrate the ω-winning strategy for player 1 in GaΣ (G2 , G1 ) starting from ({u1 } 7→ x2 , {u2 }), where G2Σ is from Example 20 and G1Σ looks like MΣ 1 from Example 20 (but with xi in place of σi ): {u ,u }, {u } 7→ x 6 8 7 4 {u1 } 7→ x2 , {u2 } u6 u7 ∅, {u5 } 7→ a {u2 ,u9 }, {u6 , u8 } 7→ x3 u4 u5 {u2 , u9 } 7→ x1 , {u3 ,u10 } u2 u6 ∅, {u4 } 7→ b ∅, {u2 , u9 } 7→ x1 u3 u4 {u3 , u10 } 7→ a, ∅ ∅, {u3 , u10 } 7→ a Lemma 22. For any u0 ∈ ∆G2 , condition (< ω) holds for arbitrary strategies in the game GΣ (G2 , M1 ) iff (ω) holds in GaΣ (G2 , G1 ) for some (Ξ0 7→ x0 , Ψ0 ) with u0 ∈ Ξ0 . G2 Condition (ω) in Lemma 22 is checked in time O(|ind(K2 )|×2|∆ \ind(K2 )|×|∆G1 |), which can be readily seen by analysing the full game graph for GaΣ (G2 , G1 ) (similar to that in Example 21). By Theorem 6, we then obtain: Theorem 23. For combined complexity, the Σ-query entailment problem is in 2E XP T IME for Horn-ALCHI and Horn-ALCI KBs and in E XP T IME for DL-LiteH horn and DL-LiteH core KBs. For data complexity, these problems are all in P. Discussion We have shown that, for all of our DLs, Σ-query entailment and inseparability are in P for data complexity. The next theorem establishes a matching lower bound: Theorem 24. For data complexity, Σ-query entailment and inseparability are P-hard for DL-Litecore and EL KBs. For combined complexity, E XP T IME-hardness of Σ-query inseparability for Horn-ALC can be proved by reduction of the subsumption problem: we have T |= A v B iff (T , {A(a)}) and (T ∪ {A v B}, {A(a)}) are {B}-query inseparable. We now estab- lish matching lower bounds in the technically challenging cases. Theorem 25. For combined complexity, Σ-query entailment and inseparability are (i) 2E XP T IME-hard for Horn-ALCI KBs and (ii) E XP T IME-hard for DL-LiteH core KBs. The obtained tight complexity bounds apply to the membership problem for uni- versal UCQ-solutions and to Σ-query inseparability of TBoxes. As a consequence of Theorems 3, 23 and 25 we obtain: Theorem 26. For combined complexity, the membership problem for universal UCQ- solutions is 2E XP T IME-complete for Horn-ALCHI and Horn-ALCI; E XP T IME-com- plete for Horn-ALCH, Horn-ALC, DL-LiteH H horn and DL-Litecore ; and P-complete for EL and ELH. For data complexity, all these problems are P-complete. Σ-query inseparability of DL-LiteH core TBoxes was known to sit between PS PACE and E XP T IME [12]. Using the fact that witness ABoxes for DL-LiteH core TBox separabil- ity can always be chosen among the singleton ABoxes [12, Theorem 8], we can modify the proof of Theorem 25 to improve the PS PACE lower bound: Theorem 27. Σ-query inseparability of DL-LiteH core TBoxes is E XP T IME -complete. For more expressive DLs, TBox Σ-query inseparability is often harder than KB inseparability: for DL-Litehorn , the space of relevant witness ABoxes for TBox sepa- rability is of exponential size and, in fact, TBox inseparability is NP-hard, while KB inseparability is in P. Similarly, Σ-query inseparability of EL KBs is tractable, while Σ-query inseparability of TBoxes is E XP T IME-complete [17]. The complexity of TBox inseparability for Horn-DLs extending Horn-ALC is not known. As for future work, from a theoretical point of view, it would be of interest to inves- tigate the complexity of Σ-query inseparability for KBs in more expressive Horn DLs (e.g., Horn-SHIQ) and non-Horn DLs extending ALC. We conjecture that the game technique developed in this paper can be extended to those DLs as well. Our games can also be used to define efficient approximations of Σ-query entailment and insepa- rability for KBs. The existence of a forward strategy, for example, provides a sufficient condition for Σ-query entailment for all of our DLs. Thus, one can extract a Σ-query module of a given KB K by exhaustively removing from K those inclusions and asser- tions α such that player 1 has a winning strategy in the game GfΣ (G2 , G1 ), where G1 and G2 are generating structures for K \ {α} and K, respectively. The resulting modules are minimal for our DLs without inverse roles, and we conjecture that in practice they are often minimal for DLs with inverse roles as well; see [12] for experiments testing similar ideas for module extraction from TBoxes. References 1. Arenas, M., Botoeva, E., Calvanese, D., Ryzhikov, V.: Exchanging OWL 2 QL knowledge bases. In: Proc. of the 23rd Int. Joint Conf. on Artificial Intelligence (IJCAI 2013) (2013) 2. Arenas, M., Botoeva, E., Calvanese, D., Ryzhikov, V., Sherkhonov, E.: Exchanging descrip- tion logic knowledge bases. In: Proc. of the 13th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2012). AAAI Press (2012) 3. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI-05). pp. 364–369 (2005) 4. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The De- scription Logic Handbook: Theory, Implementation and Applications. Cambridge University Press (2003), (2nd edition, 2007) 5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2007) 6. Botoeva, E., Kontchakov, R., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Query insepara- bility for description logic knowledge bases. In: Proc. of the 14th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2014). AAAI Press (2014), full version is available at www.dcs.bbk.ac.uk/˜roman/KR2014.pdf. 7. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Journal of Auto- mated Reasoning 39(3), 385–429 (2007) 8. Eiter, T., Gottlob, G., Ortiz, M., Simkus, M.: Query answering in the description logic Horn- SHIQ. In: Proc. of the 11th European Conf. on Logics in Artificial Intelligence (JELIA 2008). Lecture Notes in Computer Science, vol. 5293, pp. 166–179. Springer (2008) 9. Hustadt, U., Motik, B., Sattler, U.: Data complexity of reasoning in very expressive descrip- tion logics. In: Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI-05). pp. 466–471 (2005) 10. Jiménez-Ruiz, E., Cuenca Grau, B., Horrocks, I., Berlanga Llavori, R.: Supporting concur- rent ontology development: Framework, algorithms and tool. Data & Knowledge Engineer- ing 70(1), 146–164 (2011) 11. Kazakov, Y.: Consequence-driven reasoning for Horn-SHIQ ontologies. In: Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJCAI 2009). pp. 2040–2045 (2009) 12. Konev, B., Kontchakov, R., Ludwig, M., Schneider, T., Wolter, F., Zakharyaschev, M.: Con- junctive query inseparability of OWL 2 QL TBoxes. In: Proc. of the 25th AAAI Conf. on Artificial Intelligence (AAAI 2011). AAAI Press (2011) 13. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The combined approach to query answering in DL-Lite. In: Proc. of the 12th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2010). AAAI Press (2010) 14. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexities of Horn description logics. ACM Trans- actions on Computational Logic 14(1), 2 (2013) 15. Lin, F., Reiter, R.: Forget it! In: In Proc. of the AAAI Fall Symposium on Relevance. pp. 154–159 (1994) 16. Lutz, C., Toman, D., Wolter, F.: Conjunctive query answering in the description logic EL us- ing a relational database system. In: Proc. of the 21st Int. Joint Conf. on Artificial Intelligence (IJCAI-09). pp. 2070–2075 (2009) 17. Lutz, C., Wolter, F.: Deciding inseparability and conservative extensions in the description logic EL. Journal of Symbolic Computation 45(2), 194–228 (2010) 18. Mazala, R.: Infinite games. In: Automata, Logics, and Infinite Games. pp. 23–42 (2001) 19. Stuckenschmidt, H., Parent, C., Spaccapietra, S. (eds.): Modular Ontologies: Concepts, The- ories and Techniques for Knowledge Modularization, Lecture Notes in Computer Science, vol. 5445. Springer (2009) 20. Wang, Z., Wang, K., Topor, R.W.: Revising general knowledge bases in description logics. In: Proc. of the 12th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2010). AAAI Press (2010)