Introduction

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 [15,22].

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 [1,2,5]. The decidability status of very expressive DLs with transitive closure is somewhat unclear. Decidability of the extension of SHOIQ with transitive closure has been claimed in [8], but according to personal communication with the authors there are problems in the construction and a corrected version has not yet been published. In this paper, we prove that satisfiability in the extension of ALCOIF with transitive closure is decidable where 'F' refers to global functionality restrictions, that is, roles can be declared to be partial functions in the TBox. We establish the same result for finite satisfiability (which does not coincide with the unrestricted case) and show that both problems are in NExpTime, thus NExpTime-complete and not harder than in the case without transitive closure. Our decision procedures are based on a decomposition of the TBox into parts that are only loosely related, and on reductions to satisfiability in ALCOI with regular role expressions and to the existential fragment of Presburger arithmetic.

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 satisfiability in ALCOIF extended with ω-regular expressions is undecidable [28].

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 satisfiability is decidable and ExpTime-complete in the extension of PDL with any two of nominals, converse, and functional relations [6,10,11]. For the combination of all three, decidability is open. Our result can be viewed as showing decidability in a special case, that is, under the syntactic restriction given above. A related frontier of undecidability is that satisfiability in the µ-calculus is undecidable when nominals, converse, and functional relations are added [4].

Another interesting perspective is provided by the fact that ALCOIF is an expressive fragment of C 2 [12,23,24], two variable first-order logic with counting quantifiers, and in fact even of the guarded fragment GC 2 of C 2 [25]. It is known that C 2 easily becomes undecidable when (an unrestricted number of) relations can be declared to have special semantic properties such as being a linear order [21], a transitive relation [13], or an equivalence relation [18]; see also [19] for an overview. In fact, the same is true for GC 2 . For example, GC 2 is undecidable when two equivalence relations are added [26] and also when three linear orders are added that can only be used in guards [17]. Decidability can sometimes be achieved when only a limited number of special relations is admitted. For example, finite satisfiability is decidable in C 2 extended with a single equivalence relation [26] and in the two variable fragment without counting when two linear orders are added [29,34]. In the logic studied in this paper, it is possible to express that a role is transitive, an equivalence relation, a linear order, or a forest, respectively, possibly using fresh auxiliary symbols. Thus, our results show that (finite) satisfiability of ALCOIF remains decidable when we admit that an unbounded number of relations is declared to have any of the mentioned semantic properties, in marked contrast to C 2 and GC 2 . We remark that finite satisfiability in ALCOIQ extended with forests has been shown in [20]. Our results capture the ALCOIF fragment of this DL, reprove decidability in NExpTime of finite satisfiability and establish the same upper bound for unrestricted satisfiability.

where A ranges over N C , a over N I , and r over N R . We use C D to abbreviate ¬(¬C ¬D), refer to a concept of the form {a} as a nominal, and to a role of the form C? as a test. An ALCOIF reg -TBox is a finite set of concept inclusions C D with C, D ALCOI reg -concepts and functionality assertions func(R) with R a role name or of the form r − with r a role name. A concept definition takes the form A ≡ C with A a concept name and C an ALCOI reg -concept, and it is an abbreviation for the concept inclusion (¬A C) (¬C A). We use RN f (T ) to denote the set of role names r such that func(r) ∈ T or func(r − ) ∈ T . For the semantics, we refer to [2]. When speaking about (finite) satisfiability, we generally mean the satisfiability of a TBox.

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 satisfies the following condition:

( * ) if the role α * occurs in T and the role name r ∈ RN f (T ) occurs in α outside of tests, then no other role name occurs in α outside of tests.

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 ∃(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 ∃(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 ∃(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 finitely satisfiable iff T ∪ { ∃(r − ) * .{a} ∃r * .{b}, func(r)} is satisfiable, where the role name r and individual names a, b are fresh. Thus, finite satisfiability can be reduced to unrestricted satisfiability 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 infinite trees) by ∃(r − ) * .∀r − .⊥, func(r − ).

(6) ∃r * .{a} ∃(r − ) * .{a}, {a} ¬∃r.∃r * .{a}, 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 finite set of concept definitions of the form

A ≡ {a} A ≡ ¬B A ≡ B B A ≡ B B A ≡ ∃α.B

where A, B, B are concept names and of functionality assertions such that func(r − ) ∈ T implies func(r) ∈ T and every concept equation A ≡ ∃α.B ∈ T satisfies the following conditions:

(i) if α contains a role name r ∈ RN f (T ), then it contains no other role name;

(ii) for every test C? that occurs in α, C is a concept name;

(iii) if α = β + β , then T contains A 1 ≡ ∃β.B, A 2 ≡ ∃β .B, A ≡ A 1 A 2 for some A 1 , A 2 ; (iv) if α = β • β , then T contains A ≡ ∃β.A 1 , A 1 ≡ ∃β .B, for some A 1 ; (v) if α = β * , then T contains A ≡ B A 1 , A 1 ≡ ∃β.A, for some A 1 .

Conditions (iii)-(v) are inspired by the Fischer-Ladner closure in PDL [9]. The following lemma shows that we can work with TBoxes in normal form without loss of generality.

Lemma 1. Every ALCOIF −

reg -TBox T can be converted in polynomial time into a TBox T in normal form such that T is (finitely) satisfiable iff T is (finitely) satisfiable.

Presburger Arithmetic. Presburger arithmetic is the first-order (FO) theory of the non-negative integers with addition Th(N, 0, 1, +) [14,27]. More precisely, a term is a constant 0 or 1, a variable, or the sum t 1 + t 2 of terms t 1 , t 2 . A Presburger formula is an FO formula over atoms of the form t 1 = t 2 with t 1 , t 2 terms. An existential Presburger formula is a Presburger formula of the shape ∃x ϕ(x, y) where ϕ is quantifier-free, and x, y are tuples of variables. If ϕ(y) is a Presburger formula with free variables y and a ∈ N has the same arity as y, then a is a model of ϕ if N |= ϕ(a). We use Mod(ϕ) to denote the set of all models of ϕ and say that ϕ is satisfiable if Mod(ϕ) = ∅.

Decomposing TBoxes

As a foundation for our decision procedures, we show that (finite) satisfiability of an ALCOIF − reg -TBox T can be decided by checking the (finite) satisfiability 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 ALCOI reg -TBox or an ALCOIF − reg -TBox that contains only a single role name.

Let T be an ALCOIF − reg -TBox in normal form. Let -T bool denote all concept definitions in T that are not of the form A ≡ ∃α.B, -T reg denote the set of all concept definitions A ≡ ∃α.B in T such that no r ∈ RN f (T ) occurs in α, and -T r denote the set of all A ≡ ∃α.B such that r ∈ RN f (T ) is the only role name that occurs in α, plus T ∩ {func(r), func(r − )}.

Then T bool ∪ T reg is an ALCOI reg -TBox and every TBox T bool ∪ T r 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 ∈ ∆ I , the type realized by d is tp

I (d) = {A used in T | d ∈ A I }. We say that I realizes the set of types Γ if Γ = {tp I (d) | d ∈ ∆ I }.

For each type t, we denote with # t (I) the cardinality of the set {d ∈ ∆

I | tp I (d) = t}, writing # t (I) = ∞ if t is realized infinitely often in I. Proposition 1. An ALCOIF −

reg -TBox T is (finitely) satisfiable iff there is a set Γ of types for T such that 1. there is a model I reg of T bool ∪ T reg that realizes Γ ; 2. there are (finite) interpretations I r , r ∈ RN f (T ) such that, for all r, s ∈ RN f (T ):

(a) I r |= T bool ∪ T r ; (b) I r realizes Γ ; (c) # t (I r ) = # t (I s ) for all t ∈ Γ .

Finite Satisfiability

The characterization provided in Proposition 1 gives rise to a transparent decision procedure for finite satisfiability via a reduction to satisfiability in ALCOI reg (to check Condition 1) and to satisfiability in the existential fragment of Presburger arithmetic (to check the finite version of Condition 2). This reduction yields a NExpTime upper bound and since finite satisfiability in ALCOIF is NExpTime-hard [31], we obtain the following.

Theorem 1. Finite satisfiability in ALCOIF − reg is NExpTime-complete.

The central observation for checking Condition 2 via Presburger arithmetic is the following.

Lemma 2. Let {t 1 , . . . , t n } be the set of all types for T . For every r ∈ RN f (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 = (a 1 , . . . , a n ) ∈ N n , the following are equivalent:

1. a ∈ Mod(ϕ T ,r ); 2. there is a model I of T bool ∪ T r such that # ti (I) = a i , for all i ∈ {1, . . . , n}.

Before proving Lemma 2, let us first 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 satisfiability of the ALCOI reg -TBox

T = T bool ∪ T reg ∪ { t∈Γ t} ∪ { ∃ r. t | t ∈ Γ },

where r is a fresh role name and t denotes the conjunction of all A ∈ t and ¬A for all A / ∈ t that occur in T . Satisfiability in ALCOI reg is ExpTimecomplete [3], but we have to be careful since T is of size (single) exponential in the size of T . Fortunately, a slight modification of the algorithm in [3] achieves that the runtime is single exponential only in the number of concept names and concepts of the form ∃r.C in the input TBox, and the number of such concepts in T is polynomial in the size of T . To verify Condition 2, for every r ∈ RN f (T ) we construct the existential Presburger formula ϕ T ,r (x 1 , . . . , x n ) from Lemma 2. Then, the sentence

ϕ = ∃x r∈RN f (T ) ϕ T ,r (x 1 , . . . , x n ) ∧ ti∈Γ (x i > 0) ∧ ti / ∈Γ (x i = 0)

is satisfiable iff Condition 2 is true. It remains to note that satisfiability of existential Presburger formulas is NP-complete [33,14].

The rest of the section is devoted to the proof of Lemma 2. A crucial observation is that if func(r) ∈ T , then according to the semantics r I must have a rather restricted form in every model I of T . More precisely, every maximal connected component of the directed graph (∆ I , r I ) 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 finite trees whose language is the set of all finite models of T bool ∪ T r , 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 [33].

Trees and Tree Automata. A tree is a prefix-closed subset T ⊆ (N \ {0}) * . A node w ∈ T is a successor of v ∈ T and v is a predecessor of w if w = v • i for some i ∈ N. A tree is binary if every inner node has exactly two successors. Let Σ be a finite alphabet. A Σ-labeled tree is a pair (T, τ ) where T is a tree and τ : T → Σ assigns a letter from Σ to each node in T . We will sometimes write only τ for the Σ-labeled tree (T, τ ) if T is understood. By (T n , τ n ), we denote the subtree of (T, τ ) rooted at n ∈ T .

As our main automata model, we use two-way alternating parity tree automata (2APTA) over finite Σ-labeled binary trees [30,32]. Note that there is no a priori bound on the degree of the structures in Figure 1. For the automata construction, however, we prefer to work with binary trees, relying on our encoding of interpretations as trees to bridge the gap. If both func(r) ∈ T and func(r − ) ∈ T , then the components are actually paths or cycles rather than trees. To achieve a uniform construction, we also encode those as binary trees.

Formally, a 2APTA is a tuple A = (Q, Σ, q 0 , δ, ρ) where Q is a set of states, q 0 ∈ 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 σ ∈ Σ to a positive Boolean formula δ(q, σ) over the truth constants true and false and transitions of the form p, ♦p, p, ♦ − p with p ∈ 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) ∈ T . We show how to construct a 2APTA that accepts precisely the models of T bool ∪ T r , suitably encoded.

We first 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 fit all components beneath the root and to fit all successors beneath any node inside a component. We use the alphabet

Σ = {•} ∪ {(t, M ) | t a type for T and M ∈ {−, root, loop, src, tgt}}.

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 {a} in T , there is a unique node n a such that τ (n a ) = (t, M ) and A ∈ t for some A ≡ {a} ∈ T bool , (ii) there is some n ∈ T with τ (n) = (t, M ) for some M , and (iii) for all n ∈ T :

1. if τ (n) = (t, M ) with M ∈ {root, loop}, then for all nodes n below n, τ (n ) has the form • or (t , −); 2. if τ (n) = (t, src), then for all nodes n below n, τ (n ) has the form •, (t , −), or (t , tgt), and there is a unique node n below n with τ (n ) of the form (t , tgt); 3. if τ (n) = (t, M ) with M ∈ {−, tgt}, then there is a node n above n with τ (n ) of the form (t , M ), M ∈ {root, loop, src}.

A well-formed tree τ represents the following interpretation I τ :

-

∆ Iτ = {n ∈ T | τ (n) = •}; -a Iτ = n a for all nominals {a}; -A Iτ = {n ∈ T | τ (n) = (t, M ) and A ∈ t} for all concept names A; -(n, n ) ∈ r Iτ if one of the following is satisfied: • n = n , n ∈ T n

, and all nodes on the path from n to n are labeled •,

• n is marked with src and n ∈ T n is marked with tgt, or • n = n and n is marked with loop.

Conversely, whenever I is a finite model of func(r), then there is a finite, wellformed tree τ such that I and I τ are isomorphic. Note in particular that if some d ∈ ∆ 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 ∈ RN f (T ), one can construct in time polynomial in the size of T a 2APTA A r with polynomially many states such that

L(A r ) = {τ | τ is well-formed and I τ |= T bool ∪ T r }.

Proof. (sketch) The automaton A r is the intersection of a 2APTA A 0 that checks well-formedness of the input tree τ and a 2APTA A 1 that assumes wellformedness of τ and verifies that I τ |= T bool ∪ T r . The 2APTA A 0 is easy to construct, details are omitted.

The automaton A 1 sends a copy of itself to every node n of the input tree τ and verifies that when τ (n) = (t, X) and A ≡ C ∈ T bool ∪ T r , then A ∈ t iff n ∈ C Iτ . For the definitions in T bool , this only requires a 'local' check of t. For concept definitions A ≡ ∃α.B ∈ T r 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 finite automaton B on finite words and tracing runs of B through I τ .

If func(r − ) ∈ T r , then A 1 additionally ensures that every node has at least one successor labeled with "•".

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 finite trees (NTA) B, incurring at most a single exponential blow-up in the number of states [30,32]. Details on NTAs can be found in the appendix. Here, we only recall that the transition relation contains tuples of the form (q, σ, q 1 • • • q m ), meaning that when B is in state q and reads symbol σ, then it can send the states q 1 , . . . , q m to the m successors of the current node. We can view B as a context free grammar (CFG) G by interpreting the states as non-terminal symbols with the initial state being the start symbol, the input symbols as the terminal symbols, and each transition (q, σ, q 1 • • • q m ) as a grammar rule q → σq 1 . . . q m . Then for any tree τ accepted by B, there is a word accepted by G in which all symbols have the same multiplicities as in τ , and vice versa. We make use of the following result.

Theorem 2. [33, Theorem 4] Given a CFG G over alphabet Σ = {σ 1 , . . . , σ k }, one can compute in linear time an existential Presburger formula ϕ G (x 1 , . . . , x k ) such that for all a ∈ N k , we have a ∈ Mod(ϕ) iff there is a word w ∈ L(G) such that the number of occurrences of σ i in w is a i , for all i ∈ {1, . . . , k}.

Recall that t 1 , . . . , t n are all types for T . For each r ∈ RN f (T ), let G r be the CFG obtained from A r as described above, and let ϕ Gr (y) be the Presburger formula from Theorem 2, where y is the sequence of all variables y σ with σ ∈ Σ (assuming some fixed order). The formula ϕ T ,r from Lemma 2 is then ϕ T ,r (x 1 , . . . , x n ) := ∃y ϕ Gr (y) ∧ n i=1

x i = M ∈{−,root,loop,src,tgt} y (ti,M ) .

Unrestricted Satisfiability

Unrestricted satisfiability 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 satisfied. For Condition 1, this amounts to the same ALCOI reg satisfiability check as before. For Condition 2, the crucial difference is that the components in Figure 1 can now be infinite. A natural way to adapt the approach used in the previous section to check Condition 2 would thus be to replace 2APTA on finite trees with 2APTA on infinite 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 refinement of Proposition 1.

Proposition 2. An ALCOIF −

reg -TBox T is satisfiable iff there are disjoint sets Γ fin , Γ inf of types for T such that 1. there is a model I reg of T bool ∪ T reg that realizes Γ fin ∪ Γ inf ; 2. there are countable interpretations I r , r ∈ RN f (T ), s.t., for all r, s ∈ RN f (T ):

(a) I r |= T bool ∪ T r ; (b) I r realizes Γ fin ∪ Γ inf ; (c) # t (I r ) = # t (I s ) for all t ∈ Γ fin ; (d) # t (I r ) = ∞ for all t ∈ Γ inf .

The requirement of I r being countable in Point 2 is harmless since ALCOIF − reg is a fragment of first-order logic with countably infinite conjunctions and disjunctions, which enjoys the downwards Löwenheim-Skolem property [16]. Initially, we thus guess two sets of types Γ fin and Γ inf instead of a single set Γ . The central technical observation to deal with Condition 2 is as follows.

Lemma 4. Let Γ fin = {t 1 , . . . , t n } and Γ inf be disjoint sets of types for T . For every r ∈ RN f (T ), there is a set P T ,r of existential Presburger formulas with n free variables s.t., for all a = (a 1 , . . . , a n ) ∈ N n , the following are equivalent:

1. a ∈ Mod(ϕ) for some ϕ ∈ P T ,r ; 2. there is a model I of T bool ∪ T r that realizes exactly the types in

Γ fin ∪ Γ inf such that # ti (I) = a i for 1 ≤ i ≤ n and # t (I) = ∞ for all t ∈ Γ inf .

Moreover, there is a non-deterministic exponential time procedure that, given T , Γ fin , Γ inf , and r, generates exactly the formulas in P T ,r as possible outputs.

Before proving Lemma 4, we first observe that it yields the intended result.

Theorem 3. Satisfiability in ALCOIF − reg is NExpTime-complete.

Proof. The lower bound is inherited from ALCOIF [31]. For the upper bound, we guess disjoint sets Γ fin = {t 1 , . . . , t n }, Γ inf and verify Conditions 1 and 2 from Proposition 2. Condition 1 can be treated as in the proof of Theorem 1. Observe that Condition 2 is satisfied iff there are formulas ϕ r ∈ P T ,r , for r ∈ RN f (T )

as in Lemma 4 such that the sentence ϕ = ∃x 1 . . . ∃x n r∈RN f (T ) ϕ r (x 1 , . . . , x n ) is satisfiable. It remains to note that these formulas can be 'guessed' using the non-deterministic procedure from Lemma 4, and that satisfiability of ϕ can be checked in non-deterministic exponential time.

Now for the proof of Lemma 4. We start by encoding (potentially infinite) models I r of T bool ∪ T r as infinite trees. The encoding is essentially the same as in the previous section except that now we also have to deal with models I r that do not have a root, that is, in which some nodes have an infinite outgoing r-path.

Informally, these are represented by choosing an arbitrary element d that has an infinite outgoing r-path, marking it with root, and 'folding' all nodes reachable from d via r below d-the folded nodes are marked with an additional marker fold. Formally, we use the extended alphabet Σ = Σ ∪ {(t, fold) | t a type for T } where Σ is as in the previous section. Under the new encoding, a Σ -labeled tree is well-formed if it is well-formed in the sense of the previous section with the exception that nodes marked with root are allowed to have a single outgoing path marked with fold. The interpretation I τ associated to a well-formed Σ -labeled tree τ is defined as in the previous section except that additionally (n, n ) ∈ r Iτ if n is the predecessor of n in T and n is marked with fold. Conversely, whenever I is a countable model of func(r), then there is a well-formed tree τ such that I and I τ are isomorphic. One can construct a non-deterministic parity tree automaton (NPTA) A r that accepts exactly the encodings of models of T bool ∪ T r , by first constructing a 2APTA over infinite trees essentially as in the proof of Lemma 3 and then converting it into an NPTA, which is possible in exponential time [32].

Lemma 5. For every r ∈ RN f (T ), one can construct in time single exponential in the size of T an NPTA A r over Σ with exponentially many states such that L(A r ) = {τ | τ is well-formed and I τ |= T bool ∪ T r }.

Parity Tree Automata and Presburger Arithmetic. We aim to construct the Presburger formulas from Lemma 4 using the NPTAs from Lemma 5. The sets Γ fin and Γ inf give rise to disjoint subsets Σ fin and Σ inf of Σ , that is, Σ fin = {(t, M ) ∈ Σ | t ∈ Σ fin } and likewise for Σ inf . Let A = (Q, Σ, q 0 , δ, ρ) be an NPTA and let Σ fin , Σ inf be disjoint subsets of Σ . We denote with A q the variant of A that has q as initial state. We are interested in the multiplicities of the symbols from Σ fin 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 finite initial piece of T that is minimal with the property of containing all occurrences of symbols from Σ fin 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 infinite tree and has only symbols from Σ inf . Now, the initial piece can be described by an NTA on finite 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 ∞ (in the overall tree) and thus we only need to ensure that these components exist.

An A-obligation is a triple (q, σ, Ψ ) ∈ Q × Σ × 2 Σ inf such that there is a Σ \ Σ fin -labeled tree τ ∈ L(A q ) with τ (ε) = σ and # σ (τ ) = ∞ for all σ ∈ Ψ . 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 infinitely often while there is no restriction on the number of occurrences of other symbols from Σ inf . Let O A be the set of all A-obligations. An A-obligation set is a set S = {(q 1 , σ 1 , Ψ 1 ), . . . , (q m , σ m , Ψ m )} ⊆ O A such that Ψ 1 , . . . , Ψ m is a partition of Σ inf with possibly some Ψ i being the empty set. Let S A 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, Σ , q 0 , δ, ρ) be an NPTA and let Σ fin = {σ 1 , . . . , σ k } and Σ inf be disjoint subsets of Σ . Then there is a family (ϕ S ) S∈S A of formulas of existential Presburger arithmetic such that for every a = (a 1 , . . . , a k ) ∈ N k , the following are equivalent: 1. a ∈ Mod(ϕ S ) for some S ∈ S A ; 2. there is a τ ∈ L(A) such that (a) # σi (τ ) = a i for 1 ≤ i ≤ k and (b) # σ (τ ) = ∞ for every σ ∈ Σ inf .

Given A, Σ inf , Σ fin , and an S ∈ S A , ϕ S can be constructed in polynomial time.

Given Lemma 6 it is not hard to provide the desired set of formulas P T ,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, σ, Ψ ) ∈ Q × Σ × 2 Σ inf , it is decidable in NP whether (q, σ, Ψ ) is an A-obligation.

Conclusions

The most interesting question left open in this paper is whether satisfiability in unrestricted ALCOIF reg (equivalently: in PDL extended with nominals, inverse roles, and functional relations) is decidable. However, it even appears to be difficult to adapt the presented approach to more modest extensions of ALCOIF − reg such as local (unqualified) 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 [7] and it is not difficult to add to our approach role hierarchies restricted to role names and their inverses subject to the additional condition that functional roles do not have subroles. It is also interesting to note that adding guarded Boolean operators on roles, as typically indicated by the letter b in DL names, results in undecidability even when restricted to role names and their inverses [17].