We prove that satis ability and nite satis ability in the description logic ALCOIF reg are NExpTime-complete when every regular role expression of the form contains either no functional role or only a single role name (and possibly its inverse). Notably, this encompasses the extension of ALCOIF with transitive closure of roles and the modal logic of linear orders and successor, with converse.
There has been a long quest for description logics (DLs) that are as expressive
as possible while still being decidable. This has resulted in a prominent family
of very expressive DLs such as ALCOIF and SHOIQ that support nominals,
inverse roles, and functional roles or generalizations thereof. The combination
of these three expressive means is technically challenging but also conceived as
being very useful in applications. In fact, the member SROIQ of this family of
DLs has been standardized as the OWL 2 DL ontology language by the W3C
[
A natural feature of DLs that has not been included in OWL 2 is a transitive
closure operator on roles and, more generally, regular expressions over roles [
We also make a step towards regular role expressions in ALCOIF . In the
results stated above, we in fact admit such expressions under the restriction that
every regular role expression of the form contains either no functional role
or only a single role name (and possibly its inverse). While this certainly is a
strong restriction, the extension still provides non-trivial expressive power. For
example, it makes it possible to speak about the length of role paths modulo a
constant and to express the until operator of temporal logic. The decidability of
unrestricted ALCOIF with regular role expressions remains an open problem.
One may take it as an indication of being close to undecidability that satis ability
in ALCOIF extended with !-regular expressions is undecidable [
Apart from the DL view, there are other interesting perspectives on our
results. One is related to propositional dynamic logic (PDL). It is known that
satis ability is decidable and ExpTime-complete in the extension of PDL with
any two of nominals, converse, and functional relations [
Another interesting perspective is provided by the fact that ALCOIF is an
expressive fragment of C2 [
Let NC, NR, and NI be countably in nite sets of concept, role, and individual
names. In ALCOIreg, concepts C and (regular) roles are de ned by
C ::= > j A j fag j :C j C u C j 9 :C
::= C? j r j r j
j
j
+
where A ranges over NC, a over NI, and r over NR. We use C t D to abbreviate
:(:C u :D), refer to a concept of the form fag as a nominal, and to a role of
the form C? as a test. An ALCOIF reg-TBox is a nite set of concept inclusions
C v D with C; D ALCOIreg-concepts and functionality assertions func(R) with
R a role name or of the form r with r a role name. A concept de nition takes
the form A C with A a concept name and C an ALCOIreg-concept, and it
is an abbreviation for the concept inclusion > v (:A t C) u (:C t A). We use
RNf (T ) to denote the set of role names r such that func(r) 2 T or func(r ) 2 T .
For the semantics, we refer to [
Throughout the paper, we adopt a syntactic restriction on roles that is essential for our approach to work. An ALCOIF reg-TBox T is an ALCOIF reg-TBox that satis es the following condition: ( ) if the role occurs in T and the role name r 2 RNf (T ) occurs in of tests, then no other role name occurs in outside of tests. outside Note that ALCOIF reg contains the natural extension ALCOIF + of ALCOIF with transitive closure of roles, without any syntactic restrictions on the latter. We give some examples that further illustrate the expressive power of ALCOIF reg. Example 1. (1) A v 9(r r r) :B expresses that every A can reach a B along some r-path of length divisible by 3. Adding func(r) does not violate ( ).
(2) A v 9(C? r) :B expresses that every A can reach a B along an r-path on which C is true at every node, similar to the until operator of temporal logic. Adding func(r) does not violate ( ).
(3) A v 9(r + r ) :B expresses that whenever A is true, then B is true somewhere in the same maximal connected component of the role name r. Adding func(r) does not violate ( )
(4) An ALCOIF reg-TBox T is nitely satis able i T [ f> v 9(r ) :fag u 9r :fbg; func(r)g is satis able, where the role name r and individual names a; b are fresh. Thus, nite satis ability can be reduced to unrestricted satis ability in polynomial time.
(5) We can simulate a transitive relation by the regular role r r and an equivalence relation by the regular role (r + r) . We can enforce that the role name r is interpreted as a forest (of potentially in nite trees) by > v 9(r ) :8r :?; func(r ).
(6) > v 9r :fagt9(r ) :fag; fag v :9r:9r :fag; func(r); func(r ) enforces that r r is a (strict) linear order with successor relation r.
In the remainder of the paper, it will be convenient to work with TBoxes T in normal form, meaning that T is a nite set of concept de nitions of the form A fag
A :B
A
B t B0
A
B u B0
A
9 :B
where A; B; B0 are concept names and of functionality assertions such that
func(r ) 2 T implies func(r) 2 T and every concept equation A 9 :B 2 T
satis es the following conditions:
(i) if contains a role name r 2 RNf (T ), then it contains no other role name;
(ii) for every test C? that occurs in , C is a concept name;
(iii) if = + 0, then T contains A1 9 :B, A2 9 0:B, A
some A1; A2;
(iv) if = 0, then T contains A 9 :A1, A1 9 0:B, for some A1;
(v) if = , then T contains A B t A1, A1 9 :A, for some A1.
A1 t A2 for
Conditions (iii)-(v) are inspired by the Fischer-Ladner closure in PDL [
Lemma 1. Every ALCOIF reg-TBox T can be converted in polynomial time into a TBox T 0 in normal form such that T is ( nitely) satis able i T 0 is ( nitely) satis able.
Presburger Arithmetic. Presburger arithmetic is the rst-order (FO) theory of
the non-negative integers with addition Th(N; 0; 1; +) [
As a foundation for our decision procedures, we show that ( nite) satis ability of an ALCOIF reg-TBox T can be decided by checking the ( nite) satis ability of certain subsets of T while ensuring a rather modest form of synchronization via the multiplicity of types. An important feature of this decomposition is that each of the subsets is either an ALCOIreg-TBox or an ALCOIF reg-TBox that contains only a single role name.
Let T be an ALCOIF reg-TBox in normal form. Let { Tbool denote all concept de nitions in T that are not of the form A 9 :B, { Treg denote the set of all concept de nitions A 9 :B in T such that no r 2 RNf (T ) occurs in , and { Tr denote the set of all A 9 :B such that r 2 RNf (T ) is the only role name that occurs in , plus T \ ffunc(r); func(r )g.
Then Tbool [ Treg is an ALCOIreg-TBox and every TBox Tbool [ Tr contains no role name other than r.
A type for T is a set t of concept names used in T . For an interpretation I and d 2 I , the type realized by d is tpI (d) = fA used in T j d 2 AI g: We say that I realizes the set of types if = ftpI (d) j d 2 I g. For each type t, we denote with #t(I) the cardinality of the set fd 2 I j tpI (d) = tg, writing #t(I) = 1 if t is realized in nitely often in I. Proposition 1. An ALCOIF reg-TBox T is ( nitely) satis able i there is a set of types for T such that 1. there is a model Ireg of Tbool [ Treg that realizes ; 2. there are ( nite) interpretations Ir, r 2 RNf (T ) such that, for all r; s 2 RNf (T ): (a) Ir j= Tbool [ Tr; (b) Ir realizes ; (c) #t(Ir) = #t(Is) for all t 2
. 4
The characterization provided in Proposition 1 gives rise to a transparent
decision procedure for nite satis ability via a reduction to satis ability in ALCOIreg
(to check Condition 1) and to satis ability in the existential fragment of
Presburger arithmetic (to check the nite version of Condition 2). This reduction
yields a NExpTime upper bound and since nite satis ability in ALCOIF is
NExpTime-hard [
Theorem 1. Finite satis ability in ALCOIF reg is NExpTime-complete. The central observation for checking Condition 2 via Presburger arithmetic is the following.
Lemma 2. Let ft1; : : : ; tng be the set of all types for T . For every r 2 RNf (T ),
one can construct in time single exponential in T an existential Presburger
formula 'T ;r with n free variables such that, for all a = (a1; : : : ; an) 2 Nn, the
following are equivalent:
1. a 2 Mod('T ;r);
2. there is a model I of Tbool [ Tr such that #ti (I) = ai, for all i 2 f1; : : : ; ng.
Before proving Lemma 2, let us rst summarize how it yields the upper bound in
Theorem 1. We guess a set of types for T and verify Conditions 1 and 2 from
Proposition 1. Condition 1 is equivalent to satis ability of the ALCOIreg-TBox
Tb = Tbool [ Treg [ f> v tt2 u tg [ f> v 9rb: u t j t 2
g;
where rb is a fresh role name and u t denotes the conjunction of all A 2 t and
:A for all A 2= t that occur in T . Satis ability in ALCOIreg is
ExpTimecomplete [
Shape B:
The rest of the section is devoted to the proof of Lemma 2. A crucial
observation is that if func(r) 2 T , then according to the semantics rI must have
a rather restricted form in every model I of T . More precisely, every maximal
connected component of the directed graph ( I ; rI ) takes one of the two forms
depicted in Figure 1, that is, it is a tree after reversing the edges (Shape A),
possibly with a single additional outgoing edge at the root (Shape B). This enables
the construction of an automaton on nite trees whose language is the set of all
nite models of Tbool [ Tr, under a suitable encoding that (among other things)
only implicitly represents the extra outgoing edge of the root in components of
Shape B. Having these tree automata in place, we then exploit the close
connection between tree automata and context free languages and the fact that the
Parikh image of any context free language (which under our encoding describes
type multiplicities) can be described by a Presburger formula [
As our main automata model, we use two-way alternating parity tree
automata (2APTA) over nite -labeled binary trees [
Formally, a 2APTA is a tuple A = (Q; ; q0; ; ) where Q is a set of states, q0 2 Q is the initial state, is a transition function, and : Q ! N is a priority function that assigns a priority to each state. The transition function maps each state q and input letter 2 to a positive Boolean formula (q; ) over the truth constants true and false and transitions of the form p; p; p; p with p 2 Q. We use L(A) to denote the set of -labeled trees that are accepted by A, see the appendix for details.
Automata Construction. Let func(r) 2 T . We show how to construct a 2APTA that accepts precisely the models of Tbool [ Tr, suitably encoded.
We rst describe how interpretations that consist of disjoint components of Shape A or B can be represented as binary -labeled trees, for a suitable . Ideally, we would like to make the root of each component a successor of the root of the -labeled tree and use a marker to represent the end point of the extra edge of components of Shape B. Since we work with binary trees, however, we have to introduce intermediate nodes labeled with a dummy symbol \ " to t all components beneath the root and to t all successors beneath any node inside a component. We use the alphabet
= f g [ f(t; M ) j t a type for T and M 2 f ; root; loop; src; tgtgg: We use root to mark the root of components of Shape A, and loop and src to mark the root of components of Shape B, depending on whether the edge outgoing from the root also ends at the root or not. In the latter case, we use tgt to mark the target of the edge outgoing from the root.
A -labeled tree (T; ) is well-formed if (i) for every nominal fag in T , there is a unique node na such that (na) = (t; M ) and A 2 t for some A fag 2 Tbool, (ii) there is some n 2 T with (n) = (t; M ) for some M , and (iii) for all n 2 T : 1. if (n) = (t; M ) with M 2 froot; loopg, then for all nodes n0 below n, (n0) has the form or (t0; ); 2. if (n) = (t; src), then for all nodes n0 below n, (n0) has the form , (t0; ), or (t0; tgt), and there is a unique node n0 below n with (n0) of the form (t0; tgt); 3. if (n) = (t; M ) with M 2 f ; tgtg, then there is a node n0 above n with (n0) of the form (t0; M ), M 2 froot; loop; srcg.
A well-formed tree
represents the following interpretation I : { I = fn 2 T j (n) 6= g; { aI = na for all nominals f g
a ; { AI = fn 2 T j (n) = (t; M ) and A 2 tg for all concept names A; { (n; n0) 2 rI if one of the following is satis ed: n 6= n0, n 2 Tn0 , and all nodes on the path from n to n0 are labeled , n is marked with src and n0 2 Tn is marked with tgt, or n = n0 and n is marked with loop.
Conversely, whenever I is a nite model of func(r), then there is a nite, wellformed tree such that I and I are isomorphic. Note in particular that if some d 2 I has only a single r-predecessor e, then in the node that represents d can have one successor representing e and another dummy successor labeled \ ". We next construct the desired 2APTAs. Lemma 3. For every r 2 RNf (T ), one can construct in time polynomial in the size of T a 2APTA Ar with polynomially many states such that L(Ar) = f j
is well-formed and I j= Tbool [ Trg: Proof. (sketch) The automaton Ar is the intersection of a 2APTA A0 that checks well-formedness of the input tree and a 2APTA A1 that assumes wellformedness of and veri es that I j= Tbool [ Tr. The 2APTA A0 is easy to construct, details are omitted.
The automaton A1 sends a copy of itself to every node n of the input tree and veri es that when (n) = (t; X) and A C 2 Tbool [ Tr, then A 2 t i n 2 CI . For the de nitions in Tbool, this only requires a `local' check of t. For concept de nitions A 9 :B 2 Tr the automaton needs to verify the (non-)existence of an -path that starts at n and ends in a node whose type includes B. This is implemented by representing as a nite automaton B on nite words and tracing runs of B through I .
If func(r ) 2 Tr, then A1 additionally ensures that every node has at least
one successor labeled with \ ".
tu
From 2APTAs to Presburger Arithmetic. It is well-known that every 2APTA A
can be translated to an equivalent non-deterministic top-down automaton on
nite trees (NTA) B, incurring at most a single exponential blow-up in the
number of states [
Theorem 2. [33, Theorem 4] Given a CFG G over alphabet = f 1; : : : ; kg, one can compute in linear time an existential Presburger formula 'G(x1; : : : ; xk) such that for all a 2 Nk, we have a 2 Mod(') i there is a word w 2 L(G) such that the number of occurrences of i in w is ai, for all i 2 f1; : : : ; kg. Recall that t1; : : : ; tn are all types for T . For each r 2 RNf (T ), let Gr be the CFG obtained from Ar as described above, and let 'Gr (y) be the Presburger formula from Theorem 2, where y is the sequence of all variables y with 2 (assuming some xed order). The formula 'T ;r from Lemma 2 is then 'T ;r(x1; : : : ; xn) := 9y 'Gr (y) ^ n ^ xi = M2f ;root;loop;src;tgtg
y(ti;M) :
Unrestricted satis ability can again be decided by Proposition 1, that is, by guessing a set of types for the input TBox T and then verifying that Conditions 1 and 2 from that proposition are satis ed. For Condition 1, this amounts to the same ALCOIreg satis ability check as before. For Condition 2, the crucial di erence is that the components in Figure 1 can now be in nite. A natural way to adapt the approach used in the previous section to check Condition 2 would thus be to replace 2APTA on nite trees with 2APTA on in nite trees, and to then translate the latter into existential sentences of the variant of Presburger arithmetic that also admits the value !. It is, however, not clear how such a translation can be achieved. We thus pursue an alternative approach, based on the following slight re nement of Proposition 1.
Proposition 2. An ALCOIF reg-TBox T is satis able i there are disjoint sets n; inf of types for T such that 1. there is a model Ireg of Tbool [ Treg that realizes n [ inf ; 2. there are countable interpretations Ir, r 2 RNf (T ), s.t., for all r; s 2 RNf (T ): (a) Ir j= Tbool [ Tr; (b) Ir realizes n [ inf ; (c) #t(Ir) = #t(Is) for all t 2 (d) #t(Ir) = 1 for all t 2 inf .
n;
The requirement of Ir being countable in Point 2 is harmless since ALCOIF reg
is a fragment of rst-order logic with countably in nite conjunctions and
disjunctions, which enjoys the downwards Lowenheim-Skolem property [
Lemma 4. Let n = ft1; : : : ; tng and inf be disjoint sets of types for T . For
every r 2 RNf (T ), there is a set PT ;r of existential Presburger formulas with n
free variables s.t., for all a = (a1; : : : ; an) 2 Nn, the following are equivalent:
1. a 2 Mod(') for some ' 2 PT ;r;
2. there is a model I of Tbool [ Tr that realizes exactly the types in
such that #ti (I) = ai for 1 i n and #t(I) = 1 for all t 2 inf .
n [ inf
Moreover, there is a non-deterministic exponential time procedure that, given T ,
n, inf , and r, generates exactly the formulas in PT ;r as possible outputs.
Before proving Lemma 4, we rst observe that it yields the intended result.
Theorem 3. Satis ability in ALCOIF reg is NExpTime-complete.
Proof. The lower bound is inherited from ALCOIF [
Let A = (Q; ; q0; ; ) be an NPTA and let n; inf be disjoint subsets of 0. We denote with Aq the variant of A that has q as initial state. We are interested in the multiplicities of the symbols from n and inf in trees accepted by A. In this context, it is convenient to think of the trees (T; ) accepted by A as being partitioned into several components. One component is the nite initial piece of T that is minimal with the property of containing all occurrences of symbols from n and having only symbols from inf on the leaf nodes. Each leaf node is then the root of another component that takes the form of a potentially in nite tree and has only symbols from inf . Now, the initial piece can be described by an NTA on nite trees and thus translated into an existential Presburger formula as before while the multiplicity of all symbols in the other components is already known to be 1 (in the overall tree) and thus we only need to ensure that these components exist.
An A-obligation is a triple (q; ; ) 2 Q 0 2 inf such that there is a 0 n n-labeled tree 2 L(Aq) with (") = and # 0 ( ) = 1 for all 0 2 . Informally, an A-obligation describes a component of a tree that is not the initial component, whose root is labeled with , and in which each symbol from occurs in nitely often while there is no restriction on the number of occurrences of other symbols from inf . Let OA be the set of all A-obligations. An A-obligation set is a set S = f(q1; 1; 1); : : : ; (qm; m; m)g OA such that 1; : : : ; m is a partition of inf with possibly some i being the empty set. Let SA denote the set of all A-obligation sets. The number of obligations in each A-obligation set S is at most single exponential in the size of T and S can be represented in single exponential space. The number of A-obligation sets is at most double exponential in the size of T .
Lemma 6. Let A = (Q; 0; q0; ; ) be an NPTA and let n = f 1; : : : ; kg and inf be disjoint subsets of 0. Then there is a family ('S )S2SA of formulas of existential Presburger arithmetic such that for every a = (a1; : : : ; ak) 2 Nk, the following are equivalent: Given A, inf , 1. a 2 Mod('S ) for some S 2 SA; 2. there is a 2 L(A) such that (a) # i ( ) = ai for 1 i k and (b) # ( ) = 1 for every 2 inf .
n, and an S 2 SA; 'S can be constructed in polynomial time.
Given Lemma 6 it is not hard to provide the desired set of formulas PT ;r from Lemma 4. Moreover, the existence of the non-deterministic exponential time procedure that generates them is a consequence of (the last sentence in) Lemma 6, the fact that we can generate all candidates for A-obligation sets with a non-deterministic polynomial time procedure, and the fact proved in the appendix that given a triple (q; ; ) 2 Q 0 2 inf , it is decidable in NP whether (q; ; ) is an A-obligation. 6
The most interesting question left open in this paper is whether satis ability in
unrestricted ALCOIF reg (equivalently: in PDL extended with nominals, inverse
roles, and functional relations) is decidable. However, it even appears to be di
cult to adapt the presented approach to more modest extensions of ALCOIF reg
such as local (unquali ed) functionality restrictions. Another interesting
extension is with role hierarchies, transitioning from ALCOIF reg to SHOIF reg. It is
known that adding role hierarchies over regular roles leads to undecidability [