Query Inseparability by Games

Abstract

We investigate conjunctive query inseparability of description logic knowledge bases (KBs) with respect to a given signature, a fundamental problem 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 results ranging from P to EXPTIME and 2EXPTIME. We also employ our results to resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal UCQ-solutions in knowledge exchange are both EXPTIME-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 applications of KBs involve answering queries over incomplete data sources (ABoxes) augmented by ontologies (TBoxes) that provide additional information about the domain of interest as well as a convenient vocabulary for user queries. The standard query language in such applications, which balances expressiveness and computational complexity, is the language of conjunctive queries (CQs).

With typically large data, often tangled ontologies, and the hard problem of answering 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 language. 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 fundamental 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) n and K0 sig(K)n 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-LitecHore [ 7 ] and E L [ 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) materialisations 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 evaluation 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.

arbitrary strategy

Horn-ALCH

Horn-ALCI

2EXPTIME Thms. 23, 25

Horn-ALCHI

Horn-ALC

EXPTIME Thms. 23, 25

DL-LitehHorn

DL-LitecHore

DL-Litehorn

P

DL-LitecoTrhems. 16, 24 backward+forward strategy EXPTIME Thms. 12, 25 E LH

P Thms. 12, 24

forward strategy

E L Most interesting are EXPTIME-completeness of DL-LitecHore and 2EXPTIME-completeness of Horn-ALCI, which contrast with NP-completeness and EXPTIME-completeness of CQ evaluation for those logics. For DL-Lite without role inclusions and E LH, -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-LitecHore is EXPTIME-complete for combined complexity, which settles an open question of Arenas et al. [ 1 ], where only PSPACE-hardness was established. We also show that -query inseparability of DL-LitecHore TBoxes is EXPTIME-complete, which closes the PSPACE–EXPTIME 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 former 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 forgetting 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 E L are defined as usual. DL-Litehorn-concepts are constructed from concept names using the constructors >, ?, u, and 9R:> and DL-Litecore-concepts are DL-Litehorn-concepts without u; in other words, they are basic concepts of the form ?, >, Ai or 9R:>.

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-LitehHorn and DL-LitecHore TBox can also contain a finite number of role inclusions (RIs) R1 v R2, where the Ri are roles. In E LH 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 8R: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= ajI for i 6= j [ 4 ]. We write I j= in case an inclusion or assertion is true in I. If I j= , for all 2 T [ A, then I is a model of a KB K = (T ; A); in symbols: I j= K. K is consistent if it has a model. K j= means that I j= for all I j= K.

A conjunctive query (CQ) q(x) is a formula 9y '(x; y), where ' is a conjunction of atoms of the form Ak(z1) or Pk(z1; z2) with zi 2 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 j= q(a) for all I j= K; in this case we write K j= 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 j= q(a) implies K1 j= 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 E L or having role inclusions, -query entailment for L-KBs is LOGSPACE-reducible to -query inseparability for L-KBs.

We now consider the relationship between inseparability and universal UCQ-solutions 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 LOGSPACE-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 j= q(a) just in case I j= 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 rI (x; y) of x; y 2 I are defined by taking tI (x) = f -concept name A j x 2 AI g; rI (x; y) = f -role R j (x; y) 2 RI g: Suppose Ii is a materialisation of Ki, i = 1; 2. A function h : I2 ! homomorphism from I2 to I1 if, for any a 2 ind(K2) and any x; y 2 I2 , I1 is a – h(aI2 ) = aI1 whenever tI2 (a) 6= ; or rI2 (a; y) 6= ; for some y 2 – tI2 (x) tI1 (h(x)), rI2 (x; y) rI1 (h(x); h(y)).

I2 , and 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 = fQ; R; S; T g. I1 Then there is no -homo- T; Q S; Q T; Q S; Q a morphism from I2 to I1 (as rI2 (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 j= q(c) implies I1 j= 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 AiG 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 2 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 2 ind(K);

AM = f j tail( ) 2 AG g; P M = P G [ f( ; u) j tail( )

u; P 2 (tail( ); u)G g [ f( u; ) j tail( ) u; P 2 (tail( ); u)G 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 generated materialisations. Moreover, – for any L 2 fALCHI; ALCI; ALCH; ALCg and any Horn-L KB (T ; A), a generating structure can be constructed in time jAj 2p(jT j), p a polynomial; – for any L in the E L and DL-Lite families introduced above and any L-KB (T ; A), a generating structure can be constructed in time jAj p(jT j), p a polynomial.

Finite generating structures have been defined for E L [ 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 I2 from Example 4 can be generated by the structure G2 shown on the right.

G2 a

P

R

Q

S

Q

T

S

For a generating structure G for K and a signature , the -types tG (u) and rG (u; v) of u; v 2 G are defined by taking tG (u) = f -concept name A j u 2 AG g, rG (u; v) as f -role R j (u; v) 2 RG g if u; v 2 ind(K), as f -role R j R 2 (u; v)G g if u v, and ; otherwise, where (P )G is the converse of P G . We also define rG (u; v) to contain the inverses of the roles in rG (u; v); note that rG (u; v) is not the same as rG (v; u). We write u v if u v and rG (u; v) 6= ;.

In the next section, we show that, for a DL L having finitely generated materialisations, -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 Mi 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 M1 .

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 2 G2 and

M1 satisfy the following condition: (s1) tG2 (ui)

tM1 ( i).

The game starts in a state s0 = (u0 7! 0) with 0 = u0 in case u0 2 ind(K2). In each round i > 0, player 2 challenges player 1 with some ui 2 G2 such that ui 1 2 ui. Player 1 has to respond with a i 2 M1 satisfying (s1) and (s2) rG2 (ui 1; ui)

rM1 ( i 1; i).

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) rM2 (a; b) rM1 (a; b), for any a; b 2 ind(K2), and, (win) for any u0 2 G2 and n < !, there exists 0 2 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 fGQ2; Ran;dS;MT g1. sChoonwsnidienr G2 u Q T 3 tFhoer paicntyuren on<the!rigahntd. a 0 R 1 S 2 2 S 3 u 2 G2 , player 1 has M1 R R R 4 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 2 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 depending 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 2 ind(K1) or i = i 1v, for some v 2 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, E LH and E L, which by definition do not have inverse roles.

The existence of a forward -winning strategy for player 1 in G (G2; M1) is equivalent to the existence of an !-winning strategy in the game Gf (G2; G1), which is defined similarly to G (G2; M1) but with two modifications: (1) it is played on G2 and G1; and (2) the response xi 2 G1 of player 1 to a challenge ui 1 2 ui must be such that either xi 1; xi 2 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 shown on the right. Then, for any u 2 G2 , there is x 2 G1 such that player 1 has an !-winning strategy in Gf (G2; G1) starting from (u 7! x).

G2 G1 R 0 a a 1

R R R 1 2

R

R Q

Q

The next theorem follows from Ko¨nig’s Lemma: Lemma 11. For any u0 2 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(jG2j jG1j), 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 E L and E LH KBs, and in EXPTIME for Horn-ALC and Horn-ALCH KBs. For data complexity, 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 = iv, for some v 2 G1 (player 1 loses in case i 1 2 ind(K1)). Note that, since M1 is tree-shaped, the response of player 1 to any different challenge ui 1 2 u0i must be the same i; cf. Example 9.

That is why the states of the game Gb (G2; G1) are of the form ( i 7! xi), where i G2 , i 6= ;, and xi 2 G1 satisfy the following condition: (s01) tG2 (u) tG1 (xi), for all u 2

The game starts in a state ( 0 7! x0) such that (s00) if u 2

0 \ ind(K2), then x0 = u 2 ind(K1).

For each i > 0, player 2 always challenges player 1 with the set i = i 1, where = fv 2

G2 j u 2 v; for some u 2 g; provided that it is not empty (otherwise, player 2 loses). Player 1 responds with xi 2 such that xi 1 xi 1 and (s01) and the following condition hold: G1 (s02) rG2 (u; v) rG1 (xi 1; xi), for all u 2 i 1, v 2

Lemma 13. For any u0 2 G2 , condition (< !) holds for backward strategies in G (G2; M1) iff (!) holds in Gb (G2; G1) for some state (fu0g 7! x0).

Although Lemmas 11 and 13 look similar, the game Gb (G2; G1) turns out to be more complex than Gf (G2; G1). sEixdaemrpGle2 14s.hoTwonillounstrathtee, rciognh-t G2 a u v2 v3 (with concepts and roles omitted) w2 and an arbitrary G1. A play in w1 Gb (G2; G1) may proceed as: (fug 7! x0), (fv1; w1g 7! x1), (fv2; w2g 7! x2), (fv3; w1g 7! x3), etc. This gives at least 6 different sets i. But if G2 contained k cycles 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: v1 Lemma 15. Checking (!) in Lemma 13 is CONP-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 2 G and R, there is at most one v with u v and R 2 rG (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 = iv, 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 2 ind(K1). sEtxaartminpglefr1o7m. T(uhe2 s7 !trateg1y) G2 u20 T 1 W 2 W1 T1 satnadrt-sbhoouwnndeodn. the right is M1 1 4 T; T1 3 W; W1 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 G2 , i 6= ;, xi 2 G1 and (s01) holds. The initial state is of the form (;; 0 7! x0) such that (s00) holds. In each round i > 0, player 2 challenges player 1 with some u 2 v such that u 2 i 1 and (nbk) if v 2 i 1 then rG2 (u; v) 6 rG1 (xi 2; xi 1).

Player 1 responds with either a state ( i 1; i 7! xi) such that xi 1 1 xi (and so xi 2= ind(K1)) and (s020) holds, or a state (;; i 7! xi) such that xi 1; xi 2 ind(K1) and (s020) rG2 (u; v)

rG1 (xi 1; xi).

We make challenges u 2 v, for which u 2 i 1 and (nbk) does not hold, ‘illegitimate’ 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 rGi1ghtbe(caf.s Eshxoawmnploen 1t7h)e. aG2 0 1 2 1 0 aWne!s-hwoiwnnthinagt pslatryaetreg1yhains x1 T; T1 x3 W; W1 x4 G1 Gs (G2; G1) starting from (;; fu2; u9g 7! x1). Player 2 challenges with u2 2 u6, and player 1 responds with (fu2; u9g; fu6; u8g 7! x3). Then player 2 picks u6 2 u7 and player 1 responds with (fu6; u8g; fu7g 7! x4), where the game ends. Note the crucial guesses fu2; u9g 7! x1 and fu6; u8g 7! x3 made by player 1. If player 1 failed to guess that u8 must also be mapped to x3 and responded with (fu2; u9g; fu6g 7! x3), then after the challenge u6 2 u7 and response (fu6g; fu7g 7! x4)), player 2 would pick u7 2 u8, to which player 1 could not respond.

Lemma 19. For any u0 2 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 2 0. u8 u9

u10 S1 G2 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.

Example 20.

Consider

G2 and M1 shown on the right. Starting from (u1 7! 2), player 1 can respond to the challenges u3 u6 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 2 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 2 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 2= 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 =

Example 21. We illustrate the !-winning strategy for player 1 in Ga (G2; G1) starting from (fu1g 7! x2; fu2g), where G2 is from Example 20 and G1 looks like M1 from Example 20 (but with xi in place of i):

fu1g 7! x2; fu2g fu2; u9g 7! x1; fu3;u10g

fu3; u10g 7! a; ; Lemma 22. For any u0 2 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 2 0.

Condition (!) in Lemma 22 is checked in time O(jind(K2)j 2j G2 nind(K2)j j G1 j), 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 2EXPTIME for Horn-ALCHI and Horn-ALCI KBs and in EXPTIME for DL-LitehHorn and DL-LitecHore KBs. For data complexity, these problems are all in P. fu6;u8g; fu7g 7! x4 u6 u7 fu2;u9g; fu6; u8g 7! x3 u2 u6 ;; fu2; u9g 7! x1 ;; fu5g 7! a u4

u5 ;; fu4g 7! b

u3 u4 ;; fu3; u10g 7! a 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 E L KBs.

For combined complexity, EXPTIME-hardness of -query inseparability for Horn-ALC can be proved by reduction of the subsumption problem: we have T j= A v B iff (T ; fA(a)g) and (T [ fA v Bg; fA(a)g) are fBg-query inseparable. We now establish matching lower bounds in the technically challenging cases.

Theorem 25. For combined complexity, -query entailment and inseparability are (i) 2EXPTIME-hard for Horn-ALCI KBs and (ii) EXPTIME-hard for DL-LitecHore KBs.

The obtained tight complexity bounds apply to the membership problem for universal 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 UCQsolutions is 2EXPTIME-complete for Horn-ALCHI and Horn-ALCI; EXPTIME-complete for Horn-ALCH, Horn-ALC, DL-LitehHorn and DL-LitecHore; and P-complete for E L and E LH. For data complexity, all these problems are P-complete.

-query inseparability of DL-LitecHore TBoxes was known to sit between PSPACE and EXPTIME [ 12 ]. Using the fact that witness ABoxes for DL-LitecHore TBox separability can always be chosen among the singleton ABoxes [12, Theorem 8], we can modify the proof of Theorem 25 to improve the PSPACE lower bound: Theorem 27.

-query inseparability of DL-LitecHore TBoxes is EXPTIME-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 separability is of exponential size and, in fact, TBox inseparability is NP-hard, while KB inseparability is in P. Similarly, -query inseparability of E L KBs is tractable, while -query inseparability of TBoxes is EXPTIME-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 investigate 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 inseparability 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 assertions such that player 1 has a winning strategy in the game Gf (G2; G1), where G1 and G2 are generating structures for K n f g 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. 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)

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 description 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 Description 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 inseparability 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 Automated Reasoning 39 ( 3 ), 385 - 429 ( 2007 )

8. Eiter , T. , Gottlob , G. , Ortiz , M. , Simkus , M. : Query answering in the description logic HornSHIQ . 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 description logics . In: Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI-05) . pp. 466 - 471 ( 2005 )

10. Jime ´nez- Ruiz , E. , Cuenca Grau , B. , Horrocks , I. , Berlanga Llavori , R.: Supporting concurrent ontology development: Framework, algorithms and tool . Data & Knowledge Engineering 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. : Conjunctive 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. Kro¨ tzsch, M. , Rudolph , S. , Hitzler , P. : Complexities of Horn description logics . ACM Transactions 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 using 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 , Theories and Techniques for Knowledge Modularization, Lecture Notes in Computer Science , vol. 5445 . Springer ( 2009 )