Containment of Regular Path Queries under Description Logic Constraints

1 Introduction

Query containment [Abiteboul et al., 1995], called subsumption in AI [Baader et al., 2007], is a fundamental task in contexts like query optimization, information integration, knowledge base verification, and management of semistructured and XML data, cf. [Levy and Rousset, 1998; ten Cate and Lutz, 2009].

The complexity of query containment has been studied extensively, starting from the classical NP-completeness result for plain conjunctive queries (CQs) [Chandra and Merlin, 1977]. For recursive Datalog queries the problem is undecidable [Shmueli, 1993] but it remains decidable when one of the two queries is non-recursive [Sagiv, 1988; Chaudhuri and Vardi, 1997]. Containment has also been addressed for various forms of recursive queries over graph databases, i.e.,

∗This work was partially supported by the Austrian Science Fund (FWF) grant P20840, the Vienna Science and Technology Fund (WWTF) project ICT08-032, and by the EU under the ICT Collaborative Project ACSI (Artifact-Centric Service Interoperation), grant agreement n. FP7-257593.

Magdalena Ortiz and Mantas ˇSimkus

Institute of Information Systems Vienna University of Technology Favoritenstraße 9-11, Vienna, Austria

ortiz@kr.tuwien.ac.at, simkus@dbai.tuwien.ac.at

databases consisting of binary relations only. In this setting, which is receiving increased attention [Barcel`o et al., 2010], the basic querying mechanism is (two-way) regular path queries (2RPQs) [Calvanese et al., 2003]. These queries ask for all pairs of objects connected by a path conforming to a regular language over the binary relations, and thus support a restricted form of recursion. 2RPQs have been included in the new version of the SPARQL language for querying ontologies, which is currently under standarisation at W3C. 1

By employing techniques based on two-way automata over finite words, containment has been shown PSPACE-complete for 2RPQs [Calvanese et al., 2003], and EXPSPACE-complete for conjunctive 2RPQs (C2RPQs), the expressive variant of queries considered here that extends plain CQs by allowing each atom to be a 2RPQ [Calvanese et al., 2000].

We address here the problem of query containment under constraints, which amounts to checking whether containment between the answers to two queries holds for all structures (i.e., databases) satisfying a given set of constraints. This problem has been considered, e.g., under various forms of database constraints [Johnson and Klug, 1984], and for XML queries under constraints expressed as DTDs [ten Cate and Lutz, 2009]. We consider constraints expressed in terms of expressive Description Logics (DLs) [Baader et al., 2007], which allow one to capture by means of a TBox complex conditions that hold in a domain of interest.

For plain CQs over TBoxes, containment Q1 ⊆ Q2 of two queries is equivalent to checking entailment of Q2 in a knowledge base (KB) whose extensional component (ABox) is directly obtained from Q1. In general, entailment/containment of CQs in expressive DLs is exponentially harder than inference over plain KBs, e.g., 2EXPTIME-hard for extensions of ALC with inverse roles [Lutz, 2008], or with role hierarchies and transitivity [Eiter et al., 2009]. Tight upper bounds for entailment/containment of CQs under expressive DL constraints have been obtained using a variety of techniques [Glimm et al., 2008; Lutz, 2008; Eiter et al., 2009], and extended to entailment of C2RPQs [Calvanese et al., 2009]. However, these upper bounds do not easily extend to containment in the presence of regular path constructs, as a 2RPQ or C2RPQ on the left of Q1 ⊆ Q2, unlike a CQ, cannot be written as an ABox. Using nominals to incorporate Q1 into the TBox, tight upper bounds for containment of (an extension of) C2RPQs were obtained in [Calvanese et al., 2009], but only for DLs that cannot express functionality constraints, or for the case where inverses are disallowed from both the constraints and the query. The case when both inverses and functionality are allowed remained open until now, since there are no algorithms for reasoning in logics that support both, together with regular expressions and nominals. A technique for containment of C2RPQs under this kind of expressive DL constraints had been proposed in [Calvanese et al., 1998], but it turned out to be incomplete.

1 http://www.w3.org/TR/sparql11-query/

We show that, surprisingly, the presence of functionality constraints alone makes containment of 2RPQs EXPTIME-hard (it is PSPACE-complete in the absence of constraints [Calvanese et al., 2003]). This result is based on the ability, under functionality, to generate/traverse a tree using a regular language. We also provide the first algorithm for containment of 2RPQs under functionality contraints, and obtain a tight EXPTIME upper bound that extends to very expressive DL constraints. This is achieved extending ideas used for 2RPQs without constraints [Calvanese et al., 2000; 2003] to the setting of expressive DLs, in order to characterize a non-trivial class of structures over which containment can be decided using automata on infinite trees [Calvanese et al., 2009]. For containment of a 2RPQ in a C2RPQs under functionality constraints alone, we prove a further jump in complexity to 2EXPTIME, and provide again a matching upper bound for containment between C2RPQs under expressive DL constraints. Our techniques provide also a solution to the problem of query entailment over DL KBs in which individuals in the ABox may be related through regular rolepaths, since such ABoxes can be encoded as C2RPQs.

2 Preliminaries

We introduce now our notation for standard notions, the specific description logic (DL) that we use as a constraint language, and the class of queries that we consider.

We make use of regular languages, represented by nondeterministic finite state automata (NFAs) or regular expressions. Recall that an NFA over an alphabet Σ is a tuple α = 〈S, Σ, δ, s, f〉, where S is a finite set of states, δ ⊆ S ×Σ×S the transition relation, s ∈ S the initial state, and f ∈ S the final state 2 . We use Sα, Σα, δα, Ini(α), and Fin(α) to denote the five components of such an α. We assume that there are no incoming transitions into the initial state, and no outgoing transitions from the final state (i.e., s2 ̸= Ini(α) and s1 ̸= Fin(α) for all (s1, c, s2) ∈ δ). This is w.l.o.g., since every NFA can be translated in polynomial time into an NFA with the above properties while preserving the accepted language.

2.1 The Description Logic ALCIFbreg

We define now the DL ALCIFbreg . The vocabulary comprises countably infinite sets NR of role names and NC of concept names. If P ∈ NR, then P - is the inverse of P, and NR = NR ∪ {P - | P ∈ NR} is the set of atomic roles.

2 We can assume w.l.o.g. that an NFA has a unique final state.

Each R ∈ NR is a simple role, and if R,R′ are simple roles, so are R∩R′ , R∪R′ , and R\R′ . Every NFA whose alphabet is a set of simple roles is a role. Every A∈NC is a concept, and if R is a simple role, α is a role, and C, C ′ are concepts, then C ⊓ C′ , C ⊔ C ′ , ∃α.C, ∀α.C, ⩽ 1 R.C and ⩾2 R.C are concepts. An ALCIFbreg constraint is an expression C⊑C ′ where C,C ′ are concepts. If C is of the form ⊤⊑⩽1R.⊤ we call it a functionality constraint (where ⊤ is a shortcut for C⊔¬C). A set T of ALCIFbreg constraints is called a TBox. The syntactic closure of T , cl(T ), is defined in the usual way and is assumed to contain concepts in negation normal form (NNF) only. Recall that cl(T ) contains every concept in T and is closed under subconcepts and negation (in NNF).

A structure is a pair I = 〈ΔI , ·I 〉 where ΔI ̸= ∅, AI ⊆ ΔI for each A∈NC, and P I ⊆ ΔI × ΔI for each P ∈NR. The function ·I is extended to concepts and roles in the usual way [Baader et al., 2007], we only recall that αI = {〈d1, d2〉 | d2 is an α-successor of d1 in I}, where d2 is an α-successor of d1 in I if there is a word R1 · · ·Rn accepted by α and a sequence e0, . . . , en of elements in ΔI such that e0 = d1, en = d2, and 〈ei-1, ei〉 ∈ RI i for 1 ≤ i ≤ n. A structure I is a model of T , in symbols I |= T , if CI ⊆ C ′I for every C ⊑C ′ ∈ T .

2.2 (Conjunctive) 2-way Regular Path Queries

Let V be a countably infinite set of variables. An atom is an expression α(x, y), where x, y ∈ V and α is an NFA with alphabet Σα = NR. A conjunctive 2-way regular path query (C2RPQ) Q is an expression

where {x1, . . . , xn} ⊆ {u1, v1, . . . , um, vm} and each αi(ui, vi), 1 ≤ i ≤ m, is an atom. We let At(Q) = ⋃1≤i≤m{αi(ui, vi)} and V(Q) = ⋃1≤i≤m{ui, vi}. A match for Q in a structure I is a mapping π : V(Q) → ΔI such that π(y) is an α-successor of π(x) for each α(x, y) ∈ At(Q).

The tuple 〈x1, . . . , xn〉 of answer variables of Q is denoted by AVars(Q). The answer to Q over I, denoted Ans(Q, I), is the set of all n-tuples 〈d1, . . . , dn〉 such that 〈d1, . . . , dn〉 = 〈π(x1), . . . , π(xn)〉 for some match π for Q in I.

A query is Boolean if it has no answer variables. A 2way regular path query (2RPQ) is a C2RPQ of the form Q(x, y) ← α(x, y). A conjunctive query (CQ) is a C2RPQ where the regular language of each atom consists of one role. 3

The Query Containment Problem. Assume a pair Q1, Q2 of C2RPQs and a TBox T . We say that Q1 is contained in Q2 w.r.t. T , denoted Q1 ⊆T Q2, if Ans(Q1, I) ⊆ Ans(Q2, I) for each model I of T . The query containment problem is to decide given Q1, Q2, and T , whether Q1 ⊆T Q2.

3 Counter-models

In this section and the next one, we prove our upper bounds for query containment. Assume henceforth C2RPQs Q1, Q2 and a TBox T . We refer to any structure I containing a tuple

3 Unary atoms A(x), usually allowed in such queries, can be encoded by PA(x, x′ ), where PA is a fresh role associated to the unary predicate A and x′ is a fresh variable occurring nowhere else.

⃗ d such that ⃗ d∈Ans(Q1, I) and ⃗ d /∈ Ans(Q2, I) as a counterexample (for "Q1 ⊆ Q2"). Note that Q1 ⊆T Q2 does not hold (in symbols, Q1 ⊈T Q2) iff there is a counter-example I such that I |= T . We refer to such a structure as a countermodel (for "Q1 ⊆T Q2"). Our first goal is to show that if Q1 ⊈T Q2, then there is always a counter-model I with a "tree-like" structure that can be recognized using a treeautomaton.

Definition 1 (Tree-shaped structures). A tree is any prefixclosed set T of words over the set N+ of positive integers. A structure I is a tree-structure if ΔI is a tree and for each d1, d2 ∈ΔI and atomic role R, 〈d1, d2〉∈RI implies d2 = d1 · c or d1 = d2 · c for some c∈N+. A structure I is treeshaped if it is isomorphic to some tree-structure.

We show that Q1 ⊈T Q2 implies that there exists a witnessing counter-model I that can be decomposed into a small number of tree-shaped structures because it has a small number of split points. Intuitively, split points are elements d in I that have at least 3 neighbors d1, d2, d3 such that the 3 arcs d→d1, d→d2, and d→d3 lie on cycles in I. It is not difficult to see that a structure with n split points can be represented as n + 1 tree-shaped structures. To understand split points, we note that in the absence of DL constrains, the counter-example I can be assumed to resemble the structure of Q1 and to have at most one split point for each variable of Q1. In the presence of DL constraints more split points may be needed to account for elements that need to be collapsed due to functionality constraints. See Figure 1 for an illustration.

Given a structure I and a set S ⊆ ΔI , we use I|S to denote the restriction of I to the elements in S. A path in a structure I is a possibly infinite sequence P = d0, d1, d2, . . . of elements in ΔI such that for each di in P, where i > 0, there is an atomic role R such that 〈di-1, di〉 ∈ RI . We say P is simple if each element in P occurs exactly once.

Definition 2. Assume a structure I and d0 ∈ΔI . We let dnI(d0) = {d1 | ∃R ∈ NR : 〈d0, d1〉 ∈ RI } be the set of (direct) neighbors of d0 in I. A node d1 ∈dnI(d0) is a tree-neighbor of d0 in I if the structure I|{d0,d1}∪S is treeshaped, where S is the set of all nodes dn ∈ΔI such that I has a simple path d0, d1, d2, . . . , dn for some d2, . . . , dn-1.

Let tnI(d0) denote the set of all tree-neighbors of d in I, and let cnI(d0) = dnI(d0) \ tnI(d0) (the latter are cycle neighbors of d0). We let Sp(I) = {d∈ΔI | |cnI(d)| ≥ 3} be the set of split points in I, and let OD(I) be the out-degree of I, that is the maximum |dnI(d)| over all d∈ΔI .

Our goal now is to prove the following claim, to which we dedicate the rest of this section.

Proposition 3. Let T be a TBox, Q1 and Q2 C2RPQs, m the number of atoms of Q1, and k the total number of states over all atoms of Q1. If Q1 ⊈T Q2, then there is a countermodel J such that: (a) |Sp(J)| ≤ |V(Q1)| + 2m, and (b) OD(J )| ≤ |cl(T )| + 2k.

Proof. For a function f : B1→B2 and a tuple ⃗t = 〈b1, . . . , bk〉∈(B1)k , we let f(⃗t) = 〈f(b1), . . . , f(bk)〉. Assume for the remainder of the proof that ⃗z = 〈z1, . . . , zl〉 = AVars(Q1) and ⃗z′ = 〈z′1 , . . . , z′ l 〉 = AVars(Q2).

Assume an arbitrary counter-model I for Q1 ⊈T Q2. The strategy is to show that I can be reshaped into a countermodel with the desired properties. Since I is a countermodel, there is a tuple ⃗v = 〈v1, . . . , vl〉 ∈ (ΔI )m and a match π for Q1 such that ⃗v = π(⃗z) and ⃗v /∈Ans(Q2, I). We assume that all NFAs of Q1 have mutually disjoint state sets.

Take an arbitrary atom at = α(x, y) of Q1. Since π is a match for Q1 in I, we have that π(y) is an α-successor of π(x) in I. This means there is a sequence Γat = 〈d0, s0〉, . . . , 〈dn, sn〉 such that

• (b) for each 0 < i ≤ n, there is an atomic role R∈NR such that (si-1, R, si) ∈ δα and 〈di-1, di〉 ∈RI .

We assume that in each Γat there is no i ̸= j with 〈di, si〉 = 〈dj, sj〉. Note that a Γat with a repetition of a pair can be shortened to a sequence with no repetition while preserving the satisfaction of (a) and (b) above. Let Elem(Γat) be the set of all elements in Γat . We let Elem(Q1) = ⋃at ∈At(Q1) Elem(Γat), and note that |Elem(Q1)| = Σat ∈ At(Q1)|Elem(Γat )|.

Definition 4 (Induced interpretations). Assume a set D ⊆ 2ΔI ×B , where B is a set. We say D is good if for all e∈D we have that (i) e ̸= ∅, and (ii) 〈d1, s1〉∈e and 〈d2, s2〉∈e implies d1 = d2. If D is good and e∈D, then let ˆ e be the unique de in {d | 〈d, s〉∈e}. The interpretation induced by a good D, is JD where (i) ΔJD = D; (ii) for each atomic concept A, AJD = {e∈D | ˆ e∈AI }; (iii) for each atomic role R, RJD = {〈e1, e2〉∈D2 | 〈ˆ e1, ˆ e2〉∈RI }. For a good D, let ξD : D→ΔI be the function ξD(e) = ˆ e.

As easily seen, if D ⊆ 2ΔI ×B is good, then ξD is a homomorphism from JD to I. We can now proceed with the construction of a counter-model with the desired properties.

Stage 1 (Stretching). We construct a basic structure JD0 such that Ans(Q1, JD0 ) ⊈ Ans(Q2, JD0 ). Intuitively, in JD0 we 'stretch' the paths along which the atoms of Q1 are matched, possibly duplicating objects so that each (non initial or final) state of each atom 'visits' a different domain object. We ensure that Q2 still has no match in the stretched structure. JD0 need not be a model of T , but we shall fix this later.

For a variable x∈V(Q1), let St(x) be the set of all states s such that there is α(x1, x2)∈At(Q1) such that (a) x1 = x and s = Ini(α), or (b) x2 = x and s = Fin(α). For each x∈V(Q1), let κ(x) = {〈d, s〉∈Elem(Q1) | s∈St(x)}. Let

Our goal is to show that κ(⃗z)∈Ans(Q1, JD0 ) and κ(⃗z) /∈Ans(Q2, JD0 ) (recall κ(⃗z) = 〈κ(z1), . . . , κ(zl)〉). Note first of all that D0 is a good set by construction.

To see that κ(⃗z)∈Ans(Q1, JD0 ), we simply show that κ is actually a match for Q1 in JD0 . For this, let us assume an arbitrary atom at = α(x, y) of Q1. We must show that κ(y) is an α-successor of κ(x). To this end, from Γat = 〈d0, s0〉, . . . , 〈dn, sn〉 define a new sequence Γ′ = 〈e0, s0〉, . . . , 〈en, sn〉, where each ei is the unique element in D0 with 〈di, si〉∈ei. It remains to see:

• (a) That e0 = κ(x) and en = κ(y). Clearly, s0 ∈St(x) and sn ∈St(y). Then by the definition of D0 we have 〈d0, s0〉 ∈ κ(x) and 〈dn, sn〉 ∈ κ(y). Due to the construction of Γ′ , we have e0 = κ(x) and en = κ(y).
• (b) That s0 = Ini(α) and sn = Fin(α). This holds by assumption of Γat .
• (c) That for each 0 < i ≤ n, there is a symbol R∈NR such that (si-1,R, si)∈δα and 〈ei-1, ei〉∈RJD0 . Assume any such i. By assumption (i.e., due to Γat ), there is a symbol R∈NR such that (si-1, R, si) ∈ δα and 〈di-1, di〉∈RI . We know D0 is a good set. Furthermore, 〈di-1, si-1〉∈ei-1 and 〈di, si〉∈ei by construction of Γ′ . Then by the construction of JD0 fromD0 and I, we have 〈ei-1, ei〉 ∈RJD0 .

For κ(⃗z) /∈Ans(Q2, JD0 ), assume towards a contradiction that κ(⃗z)∈Ans(Q2, JD0 ). Consider the function ξD0 . As we know, ξD0 is a homomorphism from JD0 to I. Then clearly ξD0 (κ(⃗z))∈Ans(Q2, I). Then the contradiction follows from the assumption that ⃗v /∈Ans(Q2, I) and the fact that ξD0 (κ(⃗z)) = ⃗v. Indeed, for any zi in ⃗z, we have ξD0 (κ(zi)) = π(zi) and π(zi) = vi.

Stage 2 (Collapsing). This stage transforms JD0 into a structure that does not violate any functionality constraints. Consider the following rewrite rule RW which rewrites a good set D ⊆ 2ΔI ×B : If there are e, e1, e2 ∈D and ⩽1R.C ∈ cl(T ) such that ˆ e∈(⩽1R.C)I , {〈e, e1〉, 〈e, e2〉} ⊆ RJD , {e1, e2} ⊆ C JD , and e1 ̸= e2, then replace e1 and e2 by e3 = e1 ∪e2. If D′ is a result of applying RWon D, then we write D→D′ . If D→D′ , from ˆ e∈(⩽1R.C)I it follows that ˆ e1 = ˆ e2, and hence D′ is good.

We let πD0 (x) = κ(x). For each D′ that results from rewriting, let πD′(x) be the unique e∈D′ with κ(x) ⊆ e. It is not difficult to see that the counter-example is preserved while rewriting D0 with RW. This follows directly from the fact that JD0 is a counter-example and the following lemma.

Lemma 5. If (a) D→D′ , (b) πD is a match for Q1 in JD s.t. πD(⃗z)∈Ans(Q1, JD), and (c) πD(⃗z) /∈Ans(Q2, JD), then πD′ (⃗z) ∈ Ans(Q1, JD′ ) and πD′ (⃗z) /∈ Ans(Q2, JD′ ).

Note that by the construction of D0, |Sp(JD0 )| ≤ |V(Q1)|. RWmay add at most 2m new split point, i.e., |Sp(JD1 )| ≤ |V(Q1)|+2m. To see this, for a structure J , we let SD(J ) = Σd ∈ Sp(J )(|cnJ (d)| - 3). Then the bound is immediate from the easy fact that SD(JD0 ) ≤ 2m and the following:

Lemma 6. If D→D′ , then either (a) |Sp(JD′)|≤|Sp(JD)|, or (b) |Sp(JD′ )| = |Sp(JD)| + 1 and SD(JD′ ) < SD(JD).

Proof. Let e, e1, e2, and e3 witness D→D′ as above. Assume the case (⋆) such that Sp(JD′) = Sp(JD) ∪ {e3}. Since {e1, e2} ∩ D′ = ∅, the assumption (⋆) implies e1 /∈ Sp(JD) and e2 /∈ Sp(JD). Since e3 ∈ Sp(JD′ ), we must have |cnJD (e1)| = |cnJD (e2)| = 2. This implies that {e1, e2} ⊆ cnJD (e). There can be 3 possible cases:

• (a) |cnJD (e)| > 3. From {e1, e2} ⊆ cnJD (e) we know that |cnJD′ (e3)| = 3 and |cnJD′ (e)| = |cnJD (e)| - 1. Then we obtain SD(JD′ ) = SD(JD) - 1.
• (b) |cnJD (e)| = 3. Then |cnJD′ (e)| = 2. This means e ∈Sp(JD) and e /∈Sp(JD′ ). Contradiction to (⋆).
• (c) |cnJD (e)| < 3. Assume {e′1 , e′′ 1 } = cnJD (e1) and {e′2 , e′′ 2 } = cnJD (e2). We clearly have cnJD′ (e3) ⊆ cnJD (e1)∪cnJD (e2). Since {e1, e2} ⊆ cnJD (e), we get |cnJD (e)| = 2, e∈cnJD (e1), and e∈cnJD (e2). Thus |cnJD (e1) ∪ cnJD (e2)| ≤ 3 and |cnJD′ (e)| = 1. Since e3 ∈cnJD′ (e), we get e /∈cnJD′ (e3). From this we obtain that |cnJD′ (e3)| ≤ 2, which contradicts the assumption that e3 ∈ Sp(JD′ ).

Assume the remaining case where (⋆) is false. Note that for all e′ ∈D′ , where e′ ̸= e3, we have |cnJD′ (e′ )| ≤ |cnJD (e′ )|. Thus Sp(JD′) ⊆ Sp(JD) ∪ {e3}. Thus if Sp(JD′) ̸= Sp(JD) ∪ {e3}, then either e3 /∈Sp(JD′) or Sp(JD′) ⊊ Sp(JD). In any case, |Sp(JD′)| ≤ |Sp(JD)|.

Let D1 be the good set that results after applying RW exhaustively on D0. It is not hard to see the OD(JD1 )| ≤ 2k bound, which follows from the following lemma:

Lemma 7. For all e∈D1, |e| ≤ k and |dnJD1 (e)| ≤ 2|e|.

Stage 3 (Unraveling). Stage 2 guarantees a counter-example JD1 with few splits points and small out-degree. Functionality cannot be violated in JD1 , because I |= T and each node e in ΔJD1 satisfies every ⩽1R.C ∈ cl(T ) that ˆ e satisfies in I. Moreover, e also satisfies in JD1 the same concept names and Boolean combinations thereof as ˆ e satisfies in I. However, JD1 might not be a model of T because nodes might lack neighbors needed to satisfy existential concepts of the forms ∃α.C and ⩾2 R.C in cl(T ). This can be fixed using the standard unraveling technique for ALCIFbreg [Calvanese et al., 2009], which allows us to satisfy existential concepts by attaching to the nodes of JD1 tree-shaped structures obtained from I, which have branching ≤ |cl(T )|. The resulting structure J may be infinite, but the number of split points is preserved and the out-degree is still bounded by |cl(T )| + 2k. Furthermore, there is a homomorphism from J to I (coinciding with e↦→ ˆ e for the nodes in JD1 ) that preserves all concepts in cl(T ) and all paths that are relevant for Q1 and Q2. J is the desired counter-model. This concludes the proof of Proposition 3.

4 Deciding Query Containment

Similarly to tree-shaped structures, we define forest-shaped ones. Such a structure is essentially the union of a finite set of tree-shaped structures, which additionally allow any node to be directly related to the root of any tree.

Definition 8 (Forest-shaped structures). A forest of degree k with at most n roots, or simply an (n, k)-forest, is a subset F of S = {1, . . . , n}·{1, . . . , k}∗ such that w·c ∈ F and w ∈ S imply w ∈ F. The elements of F ∩ {1, . . . , n} are called roots of F. A structure I is an (n, k)-forest structure if ΔI is an (n, k)-forest and for each d1, d2 ∈ ΔI and each atomic role R, 〈d1, d2〉 ∈ RI implies {d1, d2} ∩ {1, . . . , n} ̸= ∅, d2 =d1 · c, or d1 =d2 · c for some c ∈ {1, . . . , k}. A structure I is (n, k)-forest-shaped if I is isomorphic to some (n, k)- forest structure.

We can now establish a crucial relationship between the counter-model J described in the previous section and forestshaped structures: by viewing split points as roots, we can view J as a forest. More formally:

Theorem 9. If J is a structure with |Sp(J)| < n and OD(J ) ≤ k, then J is (n, k)-forest-shaped.

Proof. Let R = Sp(J) if Sp(J) ̸= ∅, and R = {e}, where e ∈ ΔJ is arbitrary, otherwise. Let s1, . . . , sm be an enumeration of R. For each si ∈ R, let Ji =J |Si, where Si is the set of all nodes dl ∈ ΔJ such that J has a simple path d0, d1, d2, . . . , dl where d0 =si and either (i) di is a tree-neighbour of di-1 for every 1 < i < l, or (ii) dl =sj ∈ R with j ≤ i, and for each di, 1 ≤ i < l, di ̸∈ R. For each d ∈ ΔJ \ R there is exactly one Ji such that d ∈ ΔJi . Each node si ∈ R is the root of exactly one tree Ji, and may occur as a leaf of any Jj . Take the interpretation J ′ , where (a) ΔJ ′ = ⋃si∈R ΔJi , (b) for all atomic A, AJ ′ = ⋃si∈R AJi , (c) for all roles R, RJ ′ = ⋃si∈R rJi . It is easy to verify that J ′ is isomorphic to J , it is forest-shaped and the roots in J ′ are exactly the elements in R. Thus J ′ is (m, k)-forest-shaped, and also (n, k)-forest-shaped.

To recognize the existence of such counter-models, and thus decide query containment, we rely on 2-way alternating automata on infinite trees (2ATA) [Vardi, 1998] and adapt known techniques for query answering in expressive DLs [Calvanese et al., 2009].

Theorem 10. Given an ALCIFbreg TBox T and C2RPQs Q1 and Q2, deciding Q1 ⊆T Q2 is in 2EXPTIME. If Q2 is a 2RPQ, deciding Q1 ⊆T Q2 is in EXPTIME.

Proof. (Sketch.) Let m = |At(Q1)|, let k be the number of states over all atoms of Q1, and let ⃗z=AVars(Q1). By Proposition 3 and Theorem 9, Q1 ⊈T Q2 iff there is an (m′ , k′ )-forest shaped J and a match π for Q1 in J such that π(⃗z) ̸∈ Ans(Q2, J ), where m′ = |V(Q1)| + 2m + 1 and k′ = |cl(T )| + 2k.

An (m′ , k′ )-forest shaped structure can be represented as a labeled tree with branching degree max(m′ , k′ ). With some minor adaptations to the constructions in [Calvanese et al., 2009], we can build a 2ATA A that accepts a labeled tree T iff it represents an (m′ , k′ )-forest shaped model JT of T where Ans(Q1, J) ̸⊆ Ans(Q2, J). Every tree accepted by A is a counter-example, hence Q1 ⊈T Q2 iff the language of A is not empty. Roughly, A is obtained by intersecting three automata: AT that accepts T iff JT satisfies the constraints in T , AQ1 that accepts T iff there is a match π for Q1 in JT, and A¬Q2 that accepts T iff there is no match for Q2 in JT giving π(⃗z) as an answer.

In the case where Q2 is a 2RPQ all three automata are of small size (the state set is polynomial in the combined size of T , Q1, and Q2, the alphabet is single exponential, and the size of the acceptance condition is fixed). Hence we can test in single exponential time if the language of A is empty [Vardi, 1998].

In the case where Q2 is a C2RPQ, the automata AT and AQ1 are exactly the same as above. However, due to the presence of non-answer (i.e., existentially quantified) variables in Q2, to obtain A¬Q2 we need automata theoretic operations that cause an exponential blow-up in the size of the automata (in particular, we need projection, which requires to transform a 2ATA into an exponentially larger 1-way nondeterministic automaton (1NTA), and then complementation, which causes a blow-up in the size of the 1NTA). This results in the 2EXPTIME upper bound.

5 Lower Bounds

We first recall the DL ALCI, obtained fromALCIFbreg by disallowing ⩽1R.C from the syntax and allowing in concepts ∃R.C and ∀R.C only atomic roles R. It is well known that checking whether an ALCI TBox T has a model I is EXPTIME-hard [Baader et al., 2007], and checking whether T has a model I where a CQ Q has no match is 2EXPTIMEhard [Lutz, 2008]. It follows immediately that the bounds in Theorem 10 are tight.

Surprisingly, however, they are tight already for functional TBoxes, i.e., very simple TBoxes consisting of functionality constraints only, as we show next.

By examining the reductions which result in the above mentioned lower bounds, it is not hard to see that the bounds also apply if we ask I to be a finite-tree, that is, a tree-shaped structure with a finite domain and branching at most |cl(T )|.

Lemma 11. For ALCI, (†) checking whether a TBox T has a finite-tree model is EXPTIME-hard, and (‡) checking whether a TBox T has a finite-tree model I where a Boolean CQ has no match is 2EXPTIME-hard.

To prove our lower bounds, we first polynomially reduce problem (†) to containment of two 2RPQs w.r.t. functional TBoxes. Specifically, given an ALCI TBox T , we show how to construct a functional TBox Tf , and 2RPQs Q1(x, y) ← α1(x, y) and Q2(x, y) ← α2(x, y) such that T has a finitetree model iff Q1 ̸⊆Tf Q2. The idea is to use Q1 and functionality constraints to generate tree-shaped structures encoding interpretations of T , and to use Q2 to find errors in such structures. An error is either a mistake in the encoding of the interpretation or a violation of a constraint of T .

Let ∼C denote the NNF of ¬C and let cl′ (T ) = cl(T ) ∪ {R, ¬R | R or R- occurs in T }. Intuitively, Q1 is used to generate a finite tree in which each node "stores" the concepts of cl(T ) that the node satisfies and the roles that connect it to its parent. Let m = |cl(T )|, let γ1, . . . , γℓ be an enumeration of cl′ (T ), and let ¯ γ be the complementary symbol of γ, i.e., (a) if γ is a concept, then ¯ γ = ∼γ; (b) if γ is a role, then ¯ γ = ¬γ; (c) if γ is an expression ¬R then ¯ γ = R.

We can now define Q1(x, y) ← α1(x, y), where α1 is the automaton in Figure 2 that is built using an alphabet Σ consisting of the following roles and their inverses: Root, BT , B1, . . . ,Bm, Lγ1 , . . . ,Lγℓ . The TBox is defined as Tf = {⊤⊑⩽1R.⊤ | R ∈ Σ}, i.e., all roles are functional.

To understand how α1 works, a simple but crucial observation is that, if as role R- is functional, then by starting from a node n of a structure and traversing R · R- edges one gets back to n. We exploit this to explain how α1 generates (i.e., recognizes) finite trees encoding interpretations. From the initial state it first makes a Root-step to state s1, from where it starts generating the interpretation. From s1 it goes to state sℓ+1 via intermediate states that ensure that for each γi, 1 ≤ i ≤ ℓ, one of γi or ¯ γi is selected. Notice that, by the observation above, if α1 traverses a node n of a structure in state s1, in each of the states s2, . . . , sℓ+1 it will again traverse n.

In sℓ+1, α1 can decide whether to continue by generating a B1-child, or to continue by marking the node as terminal (via BT ). If α1 chooses the latter, it gets into su, from where it continues as follows: (i) if the current node is a Bm-successor of its parent, then it moves up in the tree and returns to state su; (ii) if the current node is a Bi-successor of its parent, where i < m, it moves up with Bi and then down to generate the Bi+1-child of the parent, together with its sub-tree. An example structure for the case m = 2 is given in Figure 3, where each βi, for 1 ≤ i ≤ ℓ, is either γi or ¯ γi .

There are two possible structural errors in the structure generated by α1: (A) when α1 reads Bi in the state su it might "introduce" a fresh Bi -edge to a child instead of moving up, and (B) α1 might not end up where it started, i.e., Root occurs more than once in the tree. To solve (A) and (B), and to ensure the satisfaction of T , we build α2, which we describe using regular expressions. For a role R, let R± =R·R- and R∓ =R-·R. Then α2 = Σ∗ ·(α1 2 + · · · + α8 2 )·Σ∗ . Intuitively, a match for Q2 in a structure generated by α1 means that the structure has one of eight errors, respectively encoded by the following expressions α1 2 , . . . , α8 2 :

Intuitively, we have a violation of ∀R.C if we can select a Bi-child that has R and L∼C in its label, or the node has Rin its label and its parent has L∼C.

where G1 = (B1 ·L±∼C ·B1) + · · · + (B-m·L±∼C ·Bm), and G2 = (B1·(L±¬R + L±∼C )·B1 ) · · · (Bm·(L±¬R +L±∼C )·B-m). Intuitively, we have a violation of ∃R.C if (a) the parent of the node is not an R-neighbor where C holds (ensured by ⋆), and (b) all the children are not R-neighbors where C holds (ensured by ⋆⋆).

By this construction we have that T has a finite-tree model iff Q1 ⊈Tf Q2. Then from Theorem 10 we obtain:

Theorem 12. Containment of two 2RPQs w.r.t. ALCIFbreg TBoxes is EXPTIME-complete, even for TBoxes consisting of functionality constraints only.

We can exploit the above ideas also to polynomially reduce (‡) to containment of an RPQ in a C2RPQ w.r.t. ALCIFbreg TBoxes. The query Q1 on the left and the TBox Tf remain the same. We assume that all variables in the query Q over T are different from x, y. For a role R, let αR = (⋃1≤i≤m Bi)·L±R + L±R·(⋃1≤i≤m Bi ). We build a new query Q′ from Q2 by replacing each atom R(z1, z2) by (αR + α2)(z1, z2), and adding the atom Σ∗ (x, y). Then T has a finite-tree counter-model for Q iff Q1 ⊈Tf Q′ . By combining this with Theorem 10, we obtain:

Theorem 13. Containment of a 2RPQ in a C2RPQ w.r.t. ALCIFbreg TBoxes is 2EXPTIME-complete, even for TBoxes consisting of functionality constraints only.

6 Regular ABoxes

Apart from the TBox, DL knowledge bases have an assertional component called ABox, which is a set of assertions a:C and (a, b):R, stating the participation of the (objects denoted by) individual names a, b, . . . in (the interpretation of) concepts C and roles R. Until now, in DLs that support regular languages over atomic roles as role expressions, ABox assertions (a, b):R are restricted to atomic or simple roles R, e.g., in [Calvanese et al., 2009]. The results of this paper yield the first algorithms and optimal complexity bounds for reasoning in the presence of NFAs or regular expressions in the ABox.

Formally, a ALCIFbreg KB is a pair K = 〈T ,A〉 where T is a TBox and A is a set of assertions of the form (a, b):α where a, b are individuals and α is a role. A structure I interprets each individual a as an element aI ∈ ΔI . We say that (a, b):α is satisfied in a structure I if 〈aI , bI 〉 ∈ αI . A model of the KB is a model of T that satisfies all the assertions in A. Given a Boolean C2RPQ Q, we say that K entails Q, written K |= Q, if Q has a match is every model of K. 4 Given a KB K = 〈T ,A〉 where A = {(a1, b1):α1, . . . , (an, bn):αn}, let QA ← α1(ua1 , vb1 ), . . . , αm(ubn , vbn ) be a Boolean C2RPQ obtained from A by using a fresh variable xa for each individual a. Then, I is a model of K iff I |= T and there is a match for QA in I. Hence, K is satisfiable iff QA ̸⊆T Q⊥, where Q⊥ is a query that does not have a match in any interpretation (such as Q⊥ ← α⊥(x, y) where α⊥ is an NFA whose language is the simple role R \ R). Moreover, given a C2RPQ Q, we can also decide query entailment w.r.t. K, by exploiting that K |= Q iff QA ⊆T Q. Hence we obtain:

Theorem 14. Let K be a ALCIFbreg KB whose ABox consists of assertions (a, b):α, for an NFA α over the alphabet of simple roles, and let Q be a Boolean C2RPQ. Then (i) deciding whether K is satisfiable is EXPTIME-complete, and (ii) deciding whether K |= Q is 2EXPTIME-complete.

7 Conclusions

We have closed the open problem of decidability of containment of 2RPQs and of C2RPQs in the presence of constraints, that range from simple functionality constraints to very expressive DL constraints, and have given optimal algorithms for the problem. Indeed, the upper bounds given here extend to the prominent DL SHIQ that underlies OWL Lite (which can be polynomially encoded into ALCIFbreg provided that numbers are coded in unary [Calvanese et al., 2009; Rudolph et al., 2008]). They also show decidability of query containment for the fragment SRIQ- of SROIQ that disallows nominals, role (ir)reflexivity axioms, and concepts of the form ∃Self.r. However, since the reduction of SRIQto ALCIFbreg is exponential in general [Kazakov, 2008], we only obtain a 2EXPTIME upper bound for 2RPQs and a 3EXPTIME upper bound for C2RPQs which are not known to be tight. We believe that our techniques can be extended with the ∃Self.r construct to obtain a tight upper bound for the DL ZIQ, which can simulate (with an exponential blow-up) full SRIQ. Our results are also relevant because they provide a necessary step towards solving containment of SPARQL 1.1 queries under the OWL 2 entailment regimes.