Regular Path Queries in Expressive Description Logics with Nominals

1 Introduction

OWL 2, the upcoming W3C Web Ontology Language [Cuenca Grau et al., 2008], is based on the expressive Description Logic (DL) SROIQ [Horrocks et al., 2006] and features several constructs considered important in ontology-based applications. A crucial challenge is to access OWL 2 ontologies via expressive, database inspired, query languages, such as (unions of) conjunctive queries, (U)CQs, or variants of regular path queries, RPQs (allowing for binary query atoms that are regular expressions), used in semi-structured data.

Reasoning over complex queries had yet to be addressed for expressive DLs that support expressive concept and role constructs plus different combinations of qualified number restrictions (Q), inverse roles (I), and nominals (O). In particular, this applies to SROQ, SROI, and SRIQ, three mutually incomparable sublogics of SROIQ. Indeed, the only algorithms for query entailment in expressive DLs with O are for UCQs in SHOQ [Glimm et al., 2008], and for UCQs without transitive roles in SHOI [Ortiz et al., 2008]; none of them supports complex role assertions as in the SR family. Calvanese et al. [2007] consider the DL ALCQIbreg which lacks nominals but supports I, Q, and regular expressions and (safe) Booleans over roles, capturing a large fragment of SRIQ. Their algorithm answers positive 2-way reg- Thomas Eiter and Magdalena Ortiz Institute of Information Systems Vienna University of Technology Favoritenstraße 9-11, Vienna, Austria

∗This work has been partially supported by the Austrian Science Fund (FWF) grant P20840, the EU project OntoRule (IST-2009231875), and the Mexican National Council for Science and Technology (CONACYT) grant 187697.

(eiter|ortiz)@kr.tuwien.ac.at

ular path queries (P2RPQs), which capture all the aforementioned query languages and are, to our knowledge, the most expressive query language considered so far.

In this paper, we address KB satisfiability, as well as entailment and containment of P2RPQs in the sublogics of SROIQ that allow for any two among Q, I, and O. Specifically, we show that KB satisfiability in SRIQ, SROI, and SROQ can be solved in 2EXPTIME. For SROQ and SROI, these are, to our knowledge, the first such bounds, and they all hold even when the numbers in the number restrictions are coded in binary. We also show that P2RPQ entailment is decidable, and so is containment q1 ⊆q2 if the DL has O or q1 has no regular expressions. These are the first decidability results for reasoning on queries in the DLs of the SR family, and hence in significant sublogics of OWL 2.

Our results are based on automata theoretic techniques, and are achieved indirectly by reducing (with an unavoidable exponential blowup) SROIQ to the novel DL ZOIQ, and tackling KB satisfiability and P2RPQ entailment and containment in its sublogics that allow for any two among Q, I, and O. ZOIQ is the DL that extends ALCQIbreg with O and concepts ∃S.Self. Specifically, we exploit the recently introduced fully enriched automata (FEA) [Bonatti et al., 2008] and reduce KB satisfiability in ZOIQ to their emptiness. Our construction yields a decision procedure for KB satisfiability in all sublogics of ZOIQ that enjoy the quasi-forest model property (see Section 3.1), and in particular for ZIQ, ZOQ, and ZOI. This is, to our knowledge, the first automata procedure that simultaneously handles Q, I, and O; it additionally considers Boolean role expressions and Self concepts. Relying on the results in [Bonatti et al., 2008], we obtain a tight EXPTIME upper bound for these logics, even with binary coding of numbers.

We then build on the techniques in [Calvanese et al., 2007] and reduce entailment of P2RPQs in the sublogics of ZOIQ to automata emptiness. This requires us to show how FEAs can be reduced to a simpler automata model. Further, we show that in DLs with O (and regular role expressions), containment of P2RPQs can be reduced to entailment, and hence obtain the first decidability and complexity results for containment of recursive queries in DLs. Specifically, we obtain (with unary coding of numbers), an optimal 2EXPTIME upper bound for P2RPQ entailment in ZIQ, ZOQ, and ZOI, and for P2RPQ containment in ZOQ and ZOI. For ZIQ, the same bound holds for containment of CQs in P2RPQs.

2 Preliminaries

Description Logics (DLs). The DL ALCOIQbSelf reg extends the basic DL ALC with nominals (O), inverse roles (I), qualified number restrictions (Q), regular expressions over roles (reg), safe Boolean role expressions (b) and inclusion axioms, and concepts of the form ∃S.Self (Self) as in SROIQ [Horrocks et al., 2006]. In the following, we use Z as an abbreviation for ALCbSelf reg ; thus we will deal with the logic ZOIQ and its sublogics ZIQ, ZOQ, and ZOI

Syntax. Let C, R, and I be fixed, countably infinite sets of concept, role, and individual names, respectively. We assume that C contains ⊤ and ⊥, denoting respectively the universal and the empty concept, and that R contains T and B, denoting respectively the universal and the empty role. Atomic concepts B, concepts C, atomic roles R, simple roles S, and roles T, obey the following EBNF grammar, where a∈I, A∈C, P ∈R, and P ̸=T:

An expression is a concept or a role. Subconcepts, subroles, and subexpressions are defined in the natural way.

An assertion has the form C(a), S(a, b), or a̸=b, where C and S are as above and a, b ∈ I. A concept inclusion axiom (CIA) has the form C ⊑C′ , where C and C′ are concepts, and a Boolean role inclusion axiom (BRIA) has the form S⊑S′ , where S and S′ are simple roles. A ZOIQ knowledge base (KB) is a pair K = 〈A, T 〉, where A is a finite set of assertions (called ABox), and T is a finite set of CIAs and BRIAs (called TBox). W.l.o.g. we assume that A is non-empty.

We also consider three sublogics of ZOIQ that result by disallowing different constructors in concepts and roles:

• ZIQ disallows {a} (nominal concepts);
• ZOQ disallows P - (inverse roles);
• ZOI disallows ⩾ nS.C, ⩽ nS.C (number restrictions).

Semantics. We rely on the usual notion of interpretation I = (ΔI , ·I ), consisting of a domain ΔI ̸= ∅ and a valuation function ·I [Baader et al., 2003]. The semantics of concept and role constructs (including the constructs for regular expressions over roles) is the standard one. We just note that (∃S.Self)I = {x | (x, x) ∈ SI } and (id(C))I = {(x, x) | x ∈ CI }.

I is a model of a concept C, denoted I |= C, if CI ̸=∅. Satisfaction of an assertion (resp., CIA, BRIA) γ by I, denoted I |= γ, is defined as usual. I is a model of an ABox (resp., TBox) Γ, denoted I |= Γ, if I |= γ for each γ in Γ. I is a model of a KB K = 〈A, T 〉 if I |= A and I |= T . The knowledge base satisfiability problem consists on deciding whether a given KB K has a model.

Query Entailment and Containment. A positive 2-way regular path query (P2RPQ) is a formula q = ∃⃗x.ϕ(⃗x), where

ϕ(⃗x) is built using ∧ and ∨ from atoms C(z) and T(z, z′ ), where z, z′ are variables from ⃗x or individuals, C is a concept and T a role. 1 If all atomic concepts and roles in ϕ occur in a KB K, then q is a query over K. Note that P2RPQs generalize conjunctive RPQs [Calvanese et al., 2000], in which the formula ϕ(⃗x) is built using only conjunction, and ordinary conjunctive queries (CQs), where in addition only atomic concepts and roles may be used in atoms. 2

Given an interpretation I, a match π for I and q is an assignment of an element π(x) ∈ ΔI to each variable x in ⃗x that makes ϕ true in the usual sense. I satisfies q, denoted I |= q, if there is a match π for I and q.

• Query entailment is the problem of deciding, given a KB K and a query q over K, whether I |= q for each model I of K, denoted K |= q.
• Query containment is the problem of deciding, given a KB K and two queries q1 and q2 over K, whether I |= q1 implies I |= q2 for each model I of K, denoted K |= q1 ⊆ q2.

We observe that KB (un)satisfiability trivially reduces to query entailment: K is unsatisfiable iff K |= ∃x.⊥(x).

3 Reasoning with automata in the Z family

In this section, we reduce KB satisfiability to emptiness of automata that run over infinite labeled forests.

Reducing KB to concept satisfiability. We rewrite a ZOIQ KB K = 〈A, T 〉 into a normal concept CK, which is a concept in negation normal form (NNF) not containing ⊤, ⊥, T, or B.

To do so, we first eliminate all BRIAs, replacing each S ⊑ S′ in T by a CIA ∃(S \ S′ ).⊤ ⊑ ⊥ (cf. [Rudolph et al., 2008]). The special symbols ⊤, ⊥ and B are simulated via fresh concept names A⊤, A⊥ and a fresh role name PB, by adding C ⊔ ¬C ⊑ A⊤ and A⊤ ⊑ ¬A⊥ for some concept C, and adding A⊤ ⊑ ∀PB.A⊥.

To eliminate T, we add an assertion PU(a, b) for each pair of individuals a, b occurring in A, where PU is a fresh role name. Then we replace in K each occurrence of T by the role RT, where RT = (PU ∪ {P | P ∈ R occurs in K})∗ if no inverse roles P - occur in K, and RT = (PU ∪ {P, P - | P ∈ R occurs in K})∗ otherwise.

As usual, using nominals, the ABox is internalized into the TBox: assertions C(a), S(a, b), and a ̸= b become CIAs {a} ⊑ C, {a} ⊑ ∃S.{b}, and {a} ⊑ ¬{b}, respectively. Finally, using the role RT, the BRIA-free TBox T is internalized into a concept CT = ∀RT. ⊔C1⊑C2∈T (¬C1 ⊔ C2). We thus obtain:

Proposition 3.1. Given a ZOIQ KB K, one can construct in linear time a normal concept CK such that: (i) if K is in L, then CK is in L, for L any of ZOIQ, ZOI, or ZOQ; (ii) if K is in ZIQ, then CK is in ZOIQ and all nominals in it stem from ABox internalization; (iii) for every P2RPQ q, K ̸|= q iff there is some I such that I |= CK and I ̸|=q.

1 Such queries are called Boolean; it is well known that queries with answer variables are reducible to Boolean ones.

2 The restriction in CQs to atomic concept atoms is w.l.o.g., since complex concepts can be defined in the TBox. Instead, roles containing regular expressions cannot be defined in the TBox, and hence conjunctive RPQs and P2RPQs properly extend CQs.

3.1 Quasi-Forest Model Properties

We show now that ZIQ, ZOI, and ZOQ enjoy the quasiforest model property. This allows us to decide concept satisfiability (and query entailment) by deciding the existence of quasi-forest models (where the query has no match).

A forest is a set F ⊆IN∗ such that x·c∈F and x∈IN+ imply x∈F; its elements are called nodes. For each x∈F, succ(x) = {x·c ∈ F | c ∈ IN} is the set of successors of x; x is their predecessor. F has branching degree k, if |succ(x)| ≤k for each x∈F. By roots(F) we denote the roots of F, i.e., the nodes with no predecessor. F is a tree if |roots(F)|=1. The tree of F rooted at c is Tc = {c · x | x∈ IN∗ }∩F .

An (infinite) path in F is an (infinite) tree P ⊆F with branching degree 1. By convention, x · ε=x and (x · i)·-1=x.

A Σ-labeled forest (resp. tree) is a pair 〈F, V 〉, where F is a forest (resp. tree) and V : F →Σ is a labeling function.

Definition 3.2 (Quasi-forest models). Let C be a ZOIQ concept. An interpretation I is a quasi-forest model of C if:

• ΔI is a forest,
• aI ∈ roots(ΔI ) for each individual a occurring in C,
• aI ∈CI for some individual a occurring in C, and
• for every x, y ∈ ΔI such that (x, y)∈RI for some role R, either (i) {x, y}∩roots(ΔI ) ̸=∅, (ii) x=y, (iii) y ∈ succ(x), or (iv) x ∈ succ(y).

Note that (x, y) ∈RI may hold if (i) x or y is a root of ΔI (due to nominals), (ii) y is x itself (due to ∃S.Self concepts), or, as usual in logics with inverses, (iii) y is in succ(x) or (iv) y is the predecessor of x.

The above definition generalizes those of related logics (e.g., in [Bonatti et al., 2008; Calvanese et al., 2007; Sattler & Vardi, 2001]), and accommodates all constructs of ZOIQ.

The following proposition states that to decide query entailment, we only need to consider quasi-forest models.

Proposition 3.3. Let C be a normal ZOIQ concept such that (a) C is a ZOQ or ZOI concept, or (b) C is obtained from a ZIQ KB as in Proposition 3.1. Then, for every P2RPQ q, if C has a model I with I ̸|=q, then it has a quasi forest model I ′ with I ′ ̸|=q.

Proof (sketch). Every model I of C can be used to obtain a quasi forest model I ′ of C, such that I ′ is a counterexample to query entailment whenever I is. If C is a ZOI or ZOQ concept, we can proceed along the lines of the proofs in [Bonatti et al., 2008; Sattler and Vardi, 2001], respecting Boolean role constructs and Self. When C is a ZOIQ concept obtained from a rewriting a ZIQ KB, the impact of its nominals (which all stem from ABox internalization) can be confined to the roots of the quasi-forest model. In this case, we can proceed as in [Bonatti et al., 2008], again respecting Boolean role constructs and Self.

Note that Proposition 3.3 does not hold for arbitrary ZOIQ concepts, even in the absence of Boolean roles, regular expressions, and concepts of the form ∃S.Self [Tobies, 2000]. 3

3 Prop. 3.3 fails also in the presence of arbitrary role negation, as opposed to role difference, even if regular role expressions and all of O, I, and Q are disallowed.

3.2 Enriched Automata

For deciding KB satisfiability in the sublogics of ZOIQ, we build on the techniques of [Bonatti et al., 2008] that use fully enriched automata (FEAs). FEAs extend two-way alternating parity tree automata by adding graded and root transitions.

For a set W, let B(W) be the set of Boolean formulas constructible with atoms W∪{t, f} and ∧, ∨. We say that V ⊆W satisfies ϕ ∈ B(W), if assigning t to all v ∈V and f to all w∈W \V makes ϕ true. For b > 0, let Db ={-1, ε} ∪ {〈0〉, . . . , 〈b〉} ∪ {[0], . . . , [b]} ∪ {〈root〉, [root]}.

Definition 3.4. A fully enriched automaton (FEA) with index n is a tuple A = 〈Σ, b, Q, δ, q0, F〉, where Σ is a finite input alphabet, b > 0 is a counting bound, Q is a finite set of states, δ : Q × Σ → B(Db × Q) is a transition function, q0 ∈ Q is an initial state, and F = (G1, . . . ,Gn), with G1 ⊆ G2 ⊆ · · · ⊆ Gn = Q, is a parity acceptance condition.

Intuitively, a graded transition (〈i〉, q) (resp., ([i], q)), sends off a copy of A in state q to i+1 (resp., to all but i) successor nodes, and a root transition 〈root〉 (resp., [root]), sends off a copy of A in state q to one (resp., to all) roots.

The acceptance of a forest F by A can be formalized through the notion of run, which is a tree labeled by elements of F ×Q. Intuitively, in a run, a node y labeled by (x, q) describes a copy of A that is in state q and reads node x of F. The conditions on a run ensure that the labels of adjacent nodes satisfy the transition function of A.

Definition 3.5. A run of A over a labeled forest 〈F, V 〉 is a F×Q-labeled tree 〈Tr, r〉 such that

• (i) r(root(Tr)) = (c, q0) for some c ∈ roots(F), and
• (ii) for every y ∈ Tr with r(y) = (x, q), some W ⊆Db × Q satisfying δ(q, V (x)) exists such that, for all (d, s) ∈W:
• if d ∈ {-1, ε}, then x·d is defined and there is some j ∈ IN such that x·j ∈ Tr and r(x·j) = (x·d, s);
• if d = 〈n〉, then there is some M ⊆ succ(x) with |M| > n such that, for each z ∈ M, there is some j ∈ IN such that x·j ∈ Tr and r(x·j) = (z, s);
• if d = [n], then there is some M ⊆ succ(x) with |M| ≤ n such that, for each z ∈ succ(x) \M, there is some j ∈ IN such that x·j ∈ Tr and r(x·j) = (z, s);
• if d = 〈root〉, then there is some c ∈ roots(F) and j ∈ IN such that x·j ∈ Tr and r(x·j) = (c, s);
• if d = [root], then for each c ∈ roots(F) there is some j ∈ IN such that x·j ∈ Tr and r(x·j) = (c, s).

The run 〈Tr, r〉 is accepting if, for each infinite path P of Tr, there is an even i such that Inf(〈P, r〉)∩Gi ̸=∅ and Inf (〈P, r〉) ∩ Gi-1 =∅, where Inf(〈P, r〉) is the set of all states q ∈Q such that {y ∈P | ∃x.r(y)=(x, q)} is infinite.

A FEA A accepts a labeled forest 〈F, V 〉 if it has some accepting run over 〈F, V 〉. The set of all forests accepted by A is L(A). The non-emptiness problem is the problem of deciding whether L (A) ̸= ∅ for a given FEA A.

Theorem 3.6 ([Bonatti et al., 2008]). The non-emptiness problem for a FEA A = 〈Σ, b, Q, δ, q0, F〉 with index k can be solved in time (b + 2)O(|Q|3 ·k2 ·log k·log b2 ) .

3.3 Reducing Satisfiability to Automata Emptiness

In the rest of this section, C denotes a normal ZOIQ concept. To represent a quasi-forest model I of C as a labeled forest, we label each individual with the set of atomic concepts (i.e., concept names and nominals) it satisfies. For atomic roles, we add R to the label of x whenever (x, x′ )∈RI and x′ is not a root. Arcs leading to roots are handled as in [Bonatti et al., 2008], by adding a special symbol ↑Ra to the label of x whenever (x, aI )∈RI . Finally, we represent loops (x, x)∈RI using special labels RSelf .

Definition 3.7. We denote by RC and IC respectively the sets of role and individual names occurring in C, by CIC the set of atomic concepts occurring in C, and we define RC = RC ∪ {P - | P ∈ RC}. We also define:

The forest encoding of a quasi-forest model I of C is the ΣClabeled forest 〈ΔI ,LI 〉 such that for each x∈ΔI :

Now we define a FEA AC that accepts a labeled forest F =〈Δ,L〉 if F represents a quasi-forest model I of C, or if it can be homomorphically embedded into such a forest. Note that AC can not ensure that an accepted forest is nominal unique, i.e., that each a∈IC occurs in exactly one root; instead, it enforces that any two roots sharing a nominal are indistinguishable by its transition function.

The construction, given for a normal ZOIQ concept, combines in a novel way techniques that had been used separately for different combinations of nominals, inverses, and counting [Bonatti et al., 2008; Sattler and Vardi, 2001], with techniques for Boolean roles [Calvanese et al., 2002; 2007] and ∃S.Self concepts [Ortiz, 2008]. As Bonatti et al., we employ FEAs; however, while they and Sattler and Vardi build an automaton for a specific guess (a partition of the nominals into equivalence classes that are interpreted as the same root, and a set of atomic concepts satisfied by each class), we defer the existence of a guess to the emptiness test of AC. This is more convenient for query answering, although it requires additional states and more involved transitions to properly handle the connections from each node to the nominals.

In what follows, we extend the syntax to allow for negation of simple roles and of the symbols in Θ(C). We let ∼E denote the NNF of an expression E, and Inv(S) denote the role obtained from a simple role S by replacing P by P - and P - by P, for each P ∈ RC. The (syntactic) closure Cl (C) of a ZOIQ concept C contains all concepts and simple roles that are relevant for deciding the satisfiability of C. It contains C and is closed under subconcepts, subroles, ∼, and Inv(S). Concerning concepts with regular role expressions, it is analogous to the standard Fischer-Ladner closure of PDL. Formally, Cl(C) is as in [Ortiz, 2008] (where atomic concepts may now be nominal concepts), extended with ≥ 1S.C for each ∃S.C ∈ Cl(C), and with ≤ 0S.∼C for each ∀S.C ∈ Cl (C), with S a simple role.

Definition 3.8. Let bC denote the maximal number n occurring in a number restriction in C, and let a1, . . . ,ak be a fixed, arbitrary enumeration of the elements of IC. The automaton AC = 〈ΣC, bC, QC, δC, q0C , FC〉 is defined as follows:

• ΣC = 2Θ(C) is as in Definition 3.7;
• QC = Cl(C)∪{q0C }∪Θ(C)∪QICl ∪ · · · ∪Qbin,

where Θ(C) = {s, ¬s | s ∈ Θ(C)} and QICl, . . . , Qbin are explained below, along with the transition function. Below, S and C respectively contain all simple roles S, ∼S and concepts C, ∼C such that ≥ nS.C or ≤ nS.C is in Cl(C), I contains each {a} and ¬{a} such that a ∈ IC, and CL = Cl (C) ∪ Θ(C).

• FC = (∅, {∀R∗ .C | ∀R∗ .C ∈ Cl(C)},QC) is the acceptance condition [Calvanese et al., 2002; 2007].
• There are transitions for each σ ∈ ΣC as defined below. First, we have

This initial transition checks that the input forest encodes a quasi-model of C. Its three conjuncts respectively check that (i) some root is in the interpretation of C, (ii) each nominal is interpreted as some root, and (iii) all pairs of roots interpreting the same nominals have identical labels and satisfy the same expressions in the closure. For testing (iii), AC moves to the states in QICl. For each such state, there are transitions

Transitions that use the states Cl(C) to inductively decompose simple roles, concepts (except number restrictions and ∃S.Self concepts), and regular role expressions within concepts are as usual, see e.g., [Calvanese et al., 2002; 2007]. We recall that propagation of ∀T.C (resp., ∃T.C) in the case where T =R∗ is by δC(∀R∗ .C, σ) = (ε, C)∧(ε, ∀R.∀R∗ .C) (resp., δC(∃R∗ .C, σ) = (ε, C) ∨ (ε, ∃R.∃R∗ .C)).

For each ∃S.Self in Cl (C), we have

as in [Ortiz, 2008]. For each ∃S.C and ∀S.C in Cl (C) where S is simple, we respectively have

We next give the transitions that ensure satisfaction of the number restrictions. They are novel and differ from all previous approaches. In ZOIQ, to ensure that ≥ nS.C or

≤ n S.C is satisfied at some node x of a forest F we must take all nodes x′ into account for which (x, x′ )∈SI may hold in the encoded interpretation I. This x′ may be (cf. Def. 3.2): (i) a root of F, (ii) x itself, (iii) a node in succ(x), or (iv) the predecessor of x in F . Our transitions are more involved than those in [Bonatti et al., 2008] for two reasons. First, we must consider the four cases above, while they consider either just (i) and (iii) or (iii) and (iv). Second, as we are not building an automaton for a specific guess, verifying which roots of F take part in the satisfaction of a number restriction is more complicated, and special care is needed to ensure that roots interpreting more than one nominal are not counted more than once. The transitions differ also from those in [Calvanese et al., 2002; 2007; Ortiz, 2008], which use non-graded automata and count the successors of x one-by-one; this requires exponentially many states if n is coded in binary.

For each ≥ n S.C in Cl (C), we define:

where for m ≥ 0, NR∧(m, S, C) = ϕ1 ∨ ϕ2 ∨ ϕ3 ∨ϕ4 and

To understand these transitions, suppose satisfaction of ≥ nS.C is verified at node x. Then, among the nodes of type (i) to (iv) above, there must exist distinct nodes x′1 , . . . , x′n for which the following holds: (*) x is related to x′j via S and x′j satisfies C. These nodes are grouped further into two kinds: the roots, in (i), and nodes that are not roots, in (ii) to (iv). The first transition searches for some i such that i nodes of the first group and m=n-i of the second group satisfy (*). The latter check is done via NR∧(m, S,C). Its disjuncts ϕ1 to ϕ4 correspond to the four possible ways in which these m nodes can be found among the nodes of types (ii) to (iv), viz.:

• (ϕ1) m successors of x satisfy (*),
• (ϕ2) x itself and (at least) m-1 successors of x satisfy (*),
• (ϕ3) the predecessor of x and (at least) m-1 successors of x satisfy (*), or
• (ϕ4) x itself, the predecessor of x, and (at least) m-2 successors of x satisfy (*).

Finally, the following transitions for each 〈〈root〉i , S,C〉 in Qroots check whether i roots satisfy (*):

The transitions for concepts ≤ nS.C are analogous. They use states 〈[root]i , S,C〉 in Qroots, states 〈∨, α,C〉 in Qbin, and states in QNom. Note that in the above transitions, the automaton moves to the auxiliary states in Qroots and Qbin. Then, for each ¬a ∨¬a′ in QNom, there is a transition

and for each 〈◦, α, C〉 in Qbin, there is a transition

The automaton also moves to the states SSelf in QSelf (resp. ↑Sa in Q↑), to verify whether a node x is connected by S to itself (resp. to a root where a holds). Then the simple role S is decomposed using, for each q ∈ Q↑,

and similar transitions for all q ∈QSelf .

Finally, the automaton checks the label of the current node for atomic expressions and special symbols. For each s∈Θ(C),

The automaton AC provides the desired reduction.

Lemma 3.9. Let C be a normal ZOIQ concept. If L (AC) ̸= ∅ then C is satisfiable, and if C has a quasi-forest model, then L(AC) ̸= ∅.

Proof (sketch). If C has a quasi-forest model, it is routine to verify that AC accepts its forest encoding. The converse is less direct, as AC also accepts forests F that are not nominal unique. However, one can verify that if F has two subtrees whose roots r and r′ have the same labels and satisfy the same concepts in the closure, then a run of AC on F visiting both can be modified into one visiting only one of them. Hence, if L (AC) ̸= ∅ then AC accepts some nominal-unique F . To show that such an F corresponds to a model of C is easy.

From this and Propositions 3.1 and 3.3, we obtain:

Theorem 3.10. Let K be a ZIQ, ZOI, or ZOQ KB. Then we can construct from K a concept CK such that L (ACK ) ̸= ∅ iff K is satisfiable.

For a given KB K and the concept CK obtained from it, one can easily verify that for ACK (i) the number of states is polynomial in the size of K, (ii) the alphabet size and the counting bound are at most single exponential, even when numbers are coded in binary, and (iii) the index is fixed. Hence Theorems 3.6 and 3.10 yield an EXPTIME upper bound for KB satisfiability in all sublogics of ZOIQ that enjoy the quasi-forest model property. Since a matching lower bound is known for much weaker DLs, we obtain our first main result.

Theorem 3.11. KB satisfiability in ZIQ, ZOQ, and ZOI is EXPTIME-complete.

4 Query Entailment and Containment

To decide query entailment, we follow the ideas in [Calvanese et al., 2007], which use complementation, projection, and intersection of automata. How to complement and do projection on FEAs is open. Therefore, we exploit the fact that root transitions can be easily removed from FEAs [Bonatti et al., 2008], and then show how to eliminate also graded transitions, obtaining an automaton for which we know how to perform complementation and projection.

For b > 0, let D′b = {-1, ε} ∪ {〈0〉, . . . , 〈b〉} ∪ {[0], . . . , [b]}. A two-way graded alternating parity tree automaton (2GAPA) is a FEA with transition function δ : Q × Σ → B(D′b ×Q), i.e., there are no 〈root〉 or [root] transitions.

A FEA A with counting bound b and s states is convertible into an 2GAPA with the same index and counting bound and with O(s·b) states, accepting the tree-encoding of each forest in L(A) [Bonatti et al., 2008]. The tree encoding of a forest F is the tree obtained from F by placing a new root above the roots of F .

We now show how to eliminate graded transitions from a 2GAPA. For this, we need to restrict the attention to trees with a bounded branching degree k ≥ 1. We call a tree T ⊆ {1, . . . , k}∗ with roots(T ) = {ε} a k-tree.

Definition 4.1. A two-way alternating parity automaton (2APA) over infinite Σ-labeled k-trees is a tuple A = 〈Σ, k,Q, δ, q0, F〉, where Σ, Q, q0, and F are as for FEAs, and the transition function is δ : Q×Σ → B([-1..k] ×Q), with [-1..k] = {-1, ε, 1, . . . , k}.

A run 〈Tr, r〉 of a 2APA over a labeled k-tree 〈T, V 〉 is a T ×Q-labeled tree satisfying: ε ∈ Tr; r(ε) = (ε, q0); and for each y ∈ Tr with r(y) = (x, q) and δ(q, V (x)) = ϕ, there is a (possibly empty) set {(d1, q1), . . . , (dn, qn)} ⊆ [-1..k]×Q that satisfies ϕ and such that, for all i ∈ {1, . . . , n}, y·i ∈ Tr, x·di is defined, and r(y·i) = (x·di, qi).

Lemma 4.2. Let A = 〈Σ, b,Q, δ, q0, F〉 be a 2GAPA and k ≥ 1. There is a 2APA A′ with the same index and O(|Q| · b · k) states accepting the same set of Σ-labeled k-trees as A.

Proof (sketch). We let A′ = 〈Σ, k, Q⊎Q′ , δ′ , q0, F ′ 〉, where

For each σ ∈ Σ, the transition function δ′ is defined as follows. First, for all q ∈ Q, δ′ (q, σ) is obtained from δ(q, σ) by replacing each (〈n〉, q) with (ε, 〈n+1, q, 1〉) and each ([n], q) with (ε, [n+1, q, 1]). For 1≤i≤b+1 and 1≤j≤k, we define:

and additionally, we have:

Intuitively, from state 〈i, q, j〉, a copy of A′ is sent off in state q, to at least i successor nodes starting from the j-th one. Similarly, from state [i, q, j], no copy of A′ is sent off in state q, for at most i-1 successor nodes starting from the j-th one. Finally, if F=(G1, . . . ,Gn-1,Q), we have

One can show that a Σ-labeled k-tree is accepted by A′ iff it is accepted by A.

Note that Lemma 4.2 does not ensure equivalence between the 2GAPA and the resulting 2APA, since a 2GAPA may accept trees of arbitrary degree. However, it is sufficient for our purposes: an analysis of the proof of Proposition 3.3 reveals that, if K ̸|= q for K in ZIQ, ZOQ, or ZOI, 4 then there is a counterexample quasi-forest model I of degree bounded by bK·|Cl(C)|. Hence, the tree encoding of I has degree bounded by the maximum k of bK · |Cl (C)| and |IK|.

4 We assume w.l.o.g. that all concepts appearing in q are atomic, and that all concept and role names occurring in q occur also in K.

For deciding the entailment of a P2RPQ q, we use the technique in [Calvanese et al., 2007] extended to ZOIQ (nominals in q are handled essentially as the query constants there, while Self is handled as in [Ortiz, 2008]). For a k-tree T whose nodes are labeled with subsets of Θ(C), let IT be the interpretation of K represented by T. We define from q a 2APA AXq that accepts a labeled k-tree T X iff it explicitly finds a match for IT X and q on the nodes of T X . Technically, the node labels of T X are allowed to contain, besides elements of Θ(C), also elements of X, where X is the set of (existentially quantified) variables in q. The elements of X are treated as atomic concepts that are enforced to hold in a single node of T X (on a tree-structure, such a condition can be easily enforced by means of a 2APA), and AXq relies on such elements to check for a match for IT X and q. We then convert AXq to a one-way nondeterministic parity automaton (1NPA) A1q , from which we then project out 5 the elements of X, obtaining a 1NPAA2q . In this way, A2q accepts a k-tree T whose nodes are labeled with subsets of Θ(C), iff there exists a match for IT and q. By complementing A2q , we obtain a 1NPAA¬q accepting a k-tree T iff there is no match for IT and q. Finally, to check K |= q, we transform the FEA ACK to a 2GAPA, then to a 2APA (cf. Lemma 4.2), and finally to a 1NPA, which we intersect with A¬q. A complexity analysis of the various operations allows us to show the following:

Theorem 4.3. Given a KB K in ZIQ, ZOQ, or ZOI and a P2PRQ q, deciding K |= q is in 2EXPTIME in the total size of q and K (under unary number coding in number restrictions).

To address query containment, we extend the relationship with query answering, which is well-known for plain CQs in the relational case, to our richer setting. Indeed, K |= q1 ⊆ q2 iff Kq1 |= q2, where Kq1 = 〈Aq1 , T 〉 is the KB obtained from K = 〈A, T 〉 by first "freezing" q1 = ∃⃗x.ϕ(⃗x), i.e., considering each variable in ⃗x as a fresh individual in Kq1 , and then asserting ϕ(⃗x) to hold in Aq1 . When ϕ(⃗x) is (or can be reduced to) a conjunction ∧1≤i≤n αi of atoms, where each αi is of the form C(z) or S(z, z′ ), with S a simple role, we have that Aq1 = A ∪ {αi | 1 ≤ i ≤ n}, i.e., the frozen qi can be directly represented as an ABox. Otherwise, we can represent the whole of ϕ(⃗x) by means of a single ABox assertion Cϕ(⃗x)(a), where a is a fresh individual, and Cϕ(⃗x) is the concept obtained from ϕ(⃗x) by replacing ∧ by ⊓, ∨ by ⊔, each atom C(z) by ¬{z} ⊔ C, and each atom T (z, z′ ) by ¬{z} ⊔ ∃T.{z′ }. Note that in the latter case we need to introduce nominals, even when they were not present in K.

Theorem 4.4. K |= q1 ⊆ q2 is in 2EXPTIME wrt. the total size of q1, q2, and K (i) if K is a ZOQ or ZOI KB and q1, q2 are P2RPQs over K, or (ii) if K is a ZIQ KB, q1 is a conjunctive query, and q2 is a P2RPQ over K.

5 Reasoning in the SR family

The automata techniques devised above can be also fruitfully exploited for fragments of the DL.

5 Projection cannot be done directly on a two-way automaton.

SROIQ is similar to ZOIQ, but lacks Boolean and regular role expressions. Instead, it has an RBox R comprising (i) role inclusions R1 ◦ · · · ◦Rn ⊑ R under certain restrictions, and (ii) assertions about roles Irr(R), Ref(R), Sym(R), Dis(R,R′ ) [Horrocks et al., 2008]. Its sublogics SRIQ, SROQ, SROI are analogous to ZIQ, ZOQ, ZOI.

To exploit our automata-based algorithms for reasoning in (sublogics of) SROIQ, we can transform each SROIQ KB K into a ZOIQ KB Ψ(K). The rewriting Ψ(K) is like the one in [Ortiz, 2008] from SRIQ to ZIQ (alias ALCQIb+reg ); as nominal concepts cause no change, we do not repeat it here. Intuitively, the rewriting replaces each role R in K with a regular expression ρR. We note that this need not be done for the roles in the ABox, which can be treated by closing the role assertions wrt. the RBox. The models of K are models of the resulting Ψ(K), and conversely, each model I of Ψ(K) can be turned into a model of K by setting RI =(ρR)I (cf. [Kazakov, 2008]). Assertions about roles are simulated using BRIAs and CIAs. Based on this, we obtain:

Proposition 5.1. A SROIQ KB K can be rewritten into an equisatisfiable ZOIQ KB Ψ(K). Further, if K is in SRIQ, SROI, or SROQ, then Ψ(K) is in ZIQ, ZOI, or ZOQ, respectively.

The ZOIQ KB Ψ(K) can be constructed in time polynomial in the combined sizes of A, T , and the largest regular expression ρR used, denoted by ρK (which can be exponential in R) [Ortiz, 2008]. Hence we obtain:

Theorem 5.2. Satisfiability of a KB K = 〈A, T ,R〉 in any of SRIQ, SROI, and SROQ is in EXPTIME wrt. the total size of T , A, and ρK, and in 2EXPTIME wrt. the size of K.

For SRIQ, this is known to be optimal [Kazakov, 2008]. Note that this holds even if the number restrictions are coded in binary, and that we obtain a single exponential upper bound whenever ρK is polynomial in R.

By making again use of the rewriting above, we can reduce also query answering in SROIQ to ZOIQ.

Proposition 5.3. Let K be a SROIQ KB and q a P2RPQ over K, and let q′ be obtained from q by replacing each occurrence of each role R by ρR. Then K |= q iff Ψ(K) |= q′ .

Note that the rewriting of q into q′ may introduce regular expressions, even if they were not originally present in q. To verify K |= q1 ⊆ q2, for two P2RPQs q1 and q2, then we can proceed by "freezing" q1 and treating it as an ABox, as described in Section 4. We obtain the following upper bounds:

Theorem 5.4. Given K= 〈A, T , R〉 and q1, q2 P2RPQs over K, K |= q2 and K |= q1 ⊆ q2 are decidable in 2EXPTIME in the total size of A, T , ρK, q1, q2 and in 3EXPTIME in the total size of K, q1, q2 (assuming unary coding of numbers in the number restrictions) when (i) K is a SROQ or SROI KB, or (ii) K is a SRIQ KB and q1 is a conjunctive query.

Our results also apply to the corresponding SR logics extended with safe Boolean roles, as in [Rudolph et al., 2008].

6 Conclusion

In this paper, we have substantially pushed the frontier of decidability for query entailment and containment over very expressive DLs, and in particular for the DLs of the SR family that underlie relevant fragments of OWL. Our techniques rely heavily on the quasi-forest model property of the considered DLs, and their applicability for settings where this fails is not apparent. Indeed, the fact that Proposition 3.3 fails in ALCB, the extension of ALC with arbitrary role negation, already implies undecidability of query entailment [Pratt-Hartmann, 2008]. We remark that [Pratt-Hartmann, 2008] shows also decidability of CQ answering for the guarded two-variable fragment of FOL, but the latter captures neither nominals nor regular expressions over roles. In fact, the decidability of ZOIQ remains open, even for KB satisfiability.