Decidability and Complexity of ALCOIF with Transitive Closure (and More) Jean Christoph Jung1 and Carsten Lutz1 and Thomas Zeume2 1 Universität Bremen, Germany, {jeanjung,clu}@uni-bremen.de 2 TU Dortmund, Germany, thomas.zeume@cs.tu-dortmund.de Abstract. We prove that satisfiability and finite satisfiability in the de- scription 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. 1 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 clo- sure 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 exten- sion 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 satisfiabil- ity 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 2 Jean Christoph Jung and Carsten Lutz and Thomas Zeume 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 re- sults. 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 com- bination 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 un- decidable 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. 2 Preliminaries Let NC , NR , and NI be countably infinite sets of concept, role, and individual names. In ALCOI reg , concepts C and (regular) roles α are defined by C ::= > | A | {a} | ¬C | C u C | ∃α.C α ::= C? | r | r− | α∗ | α · α | α + α ALCOIF with Transitive Closure (and More) 3 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 {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 v 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 > v (¬A t C) u (¬C t A). We use RNf (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 essen- tial 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 ∈ RNf (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 v ∃(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 ∃(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 ∃(r + r− )∗ .B expresses that whenever A is true, then B is true some- where 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 ∪ {> v ∃(r ) .{a} u ∗ ∃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 > v ∃(r− )∗ .∀r− .⊥, func(r− ). (6) > v ∃r∗ .{a}t∃(r− )∗ .{a}, {a} v ¬∃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 t B0 A ≡ B u B0 A ≡ ∃α.B where A, B, B 0 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: 4 Jean Christoph Jung and Carsten Lutz and Thomas Zeume (i) if α contains a role name r ∈ 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 ≡ ∃β.B, A2 ≡ ∃β 0 .B, A ≡ A1 t A2 for some A1 , A2 ; (iv) if α = β · β 0 , then T contains A ≡ ∃β.A1 , A1 ≡ ∃β 0 .B, for some A1 ; (v) if α = β ∗ , then T contains A ≡ B t A1 , A1 ≡ ∃β.A, for some A1 . 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 0 in normal form such that T is (finitely) satisfiable iff T 0 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 t1 + t2 of terms t1 , t2 . A Presburger formula is an FO formula over atoms of the form t1 = t2 with t1 , t2 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(ϕ) 6= ∅. 3 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 – Tbool denote all concept definitions in T that are not of the form A ≡ ∃α.B, – Treg denote the set of all concept definitions A ≡ ∃α.B in T such that no r ∈ RNf (T ) occurs in α, and – Tr denote the set of all A ≡ ∃α.B such that r ∈ RNf (T ) is the only role name that occurs in α, plus T ∩ {func(r), func(r− )}. Then Tbool ∪ Treg is an ALCOI reg -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 ∈ ∆I , the type realized by d is tpI (d) = {A used in T | d ∈ AI }. We say that I realizes the set of types Γ if Γ = {tpI (d) | d ∈ ∆I }. For each type t, we denote with #t (I) the cardinality of the set {d ∈ ∆I | tpI (d) = t}, writing #t (I) = ∞ if t is realized infinitely often in I. ALCOIF with Transitive Closure (and More) 5 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 Ireg of Tbool ∪ Treg that realizes Γ ; 2. there are (finite) interpretations Ir , r ∈ RNf (T ) such that, for all r, s ∈ RNf (T ): (a) Ir |= Tbool ∪ Tr ; (b) Ir realizes Γ ; (c) #t (Ir ) = #t (Is ) for all t ∈ Γ . 4 Finite Satisfiability The characterization provided in Proposition 1 gives rise to a transparent deci- sion procedure for finite satisfiability via a reduction to satisfiability in ALCOI reg (to check Condition 1) and to satisfiability in the existential fragment of Pres- burger 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 {t1 , . . . , tn } be the set of all types for T . For every r ∈ RNf (T ), one can construct in time single exponential in T an existential Presburger for- mula ϕT ,r with n free variables such that, for all a = (a1 , . . . , an ) ∈ Nn , the following are equivalent: 1. a ∈ Mod(ϕT ,r ); 2. there is a model I of Tbool ∪ Tr such that #ti (I) = ai , 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 Tb = Tbool ∪ Treg ∪ {> v t u t} ∪ {> v ∃b r. u t | t ∈ Γ }, t∈Γ where rb is a fresh role name and u t denotes the conjunction of all A ∈ t and ¬A for all A ∈ / t that occur in T . Satisfiability in ALCOI reg is ExpTime- complete [3], but we have to be careful since Tb 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 Tb is polynomial in the size of T . 6 Jean Christoph Jung and Carsten Lutz and Thomas Zeume Shape A: Shape B: Fig. 1. Possible shapes of connected components of functional relations. To verify Condition 2, for every r ∈ RNf (T ) we construct the existential Presburger formula ϕT ,r (x1 , . . . , xn ) from Lemma 2. Then, the sentence ^ ^ ^ ϕ = ∃x ϕT ,r (x1 , . . . , xn ) ∧ (xi > 0) ∧ (xi = 0) r∈RNf (T ) ti ∈Γ ti ∈Γ / 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 ob- servation is that if func(r) ∈ 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), pos- sibly 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 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 con- nection 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 (Tn , τn ), we denote the subtree of (T, τ ) rooted at n ∈ T . As our main automata model, we use two-way alternating parity tree au- tomata (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 en- coding 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, Σ, q0 , δ, ρ) where Q is a set of states, q0 ∈ Q is the initial state, δ is a transition function, and ρ : Q → N is a priority ALCOIF with Transitive Closure (and More) 7 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 Tbool ∪ Tr , 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 na such that τ (na ) = (t, M ) and A ∈ t for some A ≡ {a} ∈ Tbool , (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 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 ∈ {−, tgt}, then there is a node n0 above n with τ (n0 ) of the form (t0 , M ), M ∈ {root, loop, src}. A well-formed tree τ represents the following interpretation Iτ : – ∆Iτ = {n ∈ T | τ (n) 6= ◦}; – aIτ = na for all nominals {a}; – AIτ = {n ∈ T | τ (n) = (t, M ) and A ∈ t} for all concept names A; – (n, n0 ) ∈ rIτ if one of the following is satisfied: • n 6= n0 , n ∈ Tn0 , and all nodes on the path from n to n0 are labeled ◦, • n is marked with src and n0 ∈ Tn is marked with tgt, or • n = n0 and n is marked with loop. Conversely, whenever I is a finite model of func(r), then there is a finite, well- formed 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. 8 Jean Christoph Jung and Carsten Lutz and Thomas Zeume Lemma 3. For every r ∈ RNf (T ), one can construct in time polynomial in the size of T a 2APTA Ar with polynomially many states such that L(Ar ) = {τ | τ is well-formed and Iτ |= Tbool ∪ Tr }. 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 well- formedness of τ and verifies that Iτ |= 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 verifies that when τ (n) = (t, X) and A ≡ C ∈ Tbool ∪ Tr , then A ∈ t iff n ∈ C Iτ . For the definitions in Tbool , this only requires a ‘local’ check of t. For concept definitions A ≡ ∃α.B ∈ 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 finite automaton B on finite words and tracing runs of B through Iτ . If func(r− ) ∈ Tr , then A1 additionally ensures that every node has at least one successor labeled with “◦”. t u 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, σ, q1 · · · qm ), meaning that when B is in state q and reads symbol σ, then it can send the states q1 , . . . , qm 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, σ, q1 · · · qm ) as a grammar rule q → σq1 . . . qm . 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 (x1 , . . . , xk ) such that for all a ∈ Nk , we have a ∈ Mod(ϕ) iff there is a word w ∈ L(G) such that the number of occurrences of σi in w is ai , for all i ∈ {1, . . . , k}. Recall that t1 , . . . , tn are all types for T . For each r ∈ 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 σ ∈ Σ (assuming some fixed order). The formula ϕT ,r from Lemma 2 is then n ^ X  ϕT ,r (x1 , . . . , xn ) := ∃y ϕGr (y) ∧ xi = y(ti ,M ) . i=1 M ∈{−,root,loop,src,tgt} ALCOIF with Transitive Closure (and More) 9 5 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 Condi- tions 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 Ireg of Tbool ∪ Treg that realizes Γfin ∪ Γinf ; 2. there are countable interpretations Ir , r ∈ RNf (T ), s.t., for all r, s ∈ RNf (T ): (a) Ir |= Tbool ∪ Tr ; (b) Ir realizes Γfin ∪ Γinf ; (c) #t (Ir ) = #t (Is ) for all t ∈ Γfin ; (d) #t (Ir ) = ∞ for all t ∈ Γinf . The requirement of Ir being countable in Point 2 is harmless since ALCOIF − reg is a fragment of first-order logic with countably infinite conjunctions and disjunc- tions, 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 = {t1 , . . . , tn } and Γinf be disjoint sets of types for T . For every r ∈ RNf (T ), there is a set PT ,r of existential Presburger formulas with n free variables s.t., for all a = (a1 , . . . , an ) ∈ Nn , the following are equivalent: 1. a ∈ Mod(ϕ) for some ϕ ∈ PT ,r ; 2. there is a model I of Tbool ∪ Tr that realizes exactly the types in Γfin ∪ Γinf such that #ti (I) = ai 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 PT ,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 = {t1 , . . . , tn }, Γ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 ∈ PT ,r , for r ∈ RNf (T ) 10 Jean Christoph Jung and Carsten Lutz and Thomas Zeume V as in Lemma 4 such that the sentence ϕ = ∃x1 . . . ∃xn r∈RNf (T ) ϕr (x1 , . . . , xn ) 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. t u Now for the proof of Lemma 4. We start by encoding (potentially infinite) models Ir of Tbool ∪ Tr as infinite trees. The encoding is essentially the same as in the previous section except that now we also have to deal with models Ir 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 Σ 0 = Σ ∪ {(t, fold) | t a type for T } where Σ is as in the previous section. Under the new encoding, a Σ 0 -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 Σ 0 -labeled tree τ is defined as in the previous section except that additionally (n, n0 ) ∈ rIτ if n is the predecessor of n0 in T and n0 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) Ar that accepts exactly the encodings of models of Tbool ∪ Tr , 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 ∈ RNf (T ), one can construct in time single exponential in the size of T an NPTA Ar over Σ 0 with exponentially many states such that L(Ar ) = {τ | τ is well-formed and Iτ |= Tbool ∪ Tr }. Parity Tree Automata and Presburger Arithmetic. We aim to construct the Pres- burger formulas from Lemma 4 using the NPTAs from Lemma 5. The sets Γfin and Γinf give rise to disjoint subsets Σfin and Σinf of Σ 0 , that is, Σfin = {(t, M ) ∈ Σ 0 | t ∈ Σfin } and likewise for Σinf . Let A = (Q, Σ, q0 , δ, ρ) be an NPTA and let Σfin , Σ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 Σ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. ALCOIF with Transitive Closure (and More) 11 An A-obligation is a triple (q, σ, Ψ ) ∈ Q × Σ 0 × 2Σinf such that there is a Σ \ Σfin -labeled tree τ ∈ L(Aq ) with τ (ε) = σ and #σ0 (τ ) = ∞ for all σ 0 ∈ Ψ . 0 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 OA be the set of all A-obligations. An A-obligation set is a set S = {(q1 , σ1 , Ψ1 ), . . . , (qm , σm , Ψm )} ⊆ 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 Σfin = {σ1 , . . . , σk } and Σinf be disjoint subsets of Σ 0 . Then there is a family (ϕS )S∈SA of formulas of existential Presburger arithmetic such that for every a = (a1 , . . . , ak ) ∈ Nk , the following are equivalent: 1. a ∈ Mod(ϕS ) for some S ∈ SA ; 2. there is a τ ∈ L(A) such that (a) #σi (τ ) = ai for 1 ≤ i ≤ k and (b) #σ (τ ) = ∞ for every σ ∈ Σinf . Given A, Σinf , Σfin , and an S ∈ 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, σ, Ψ ) ∈ Q × Σ 0 × 2Σinf , it is decidable in NP whether (q, σ, Ψ ) is an A-obligation. 6 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 diffi- cult to adapt the presented approach to more modest extensions of ALCOIF − reg such as local (unqualified) functionality restrictions. Another interesting exten- sion 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]. Acknowledgements. Jung and Lutz were supported by ERC consolidator grant 647289 CODA. 12 Jean Christoph Jung and Carsten Lutz and Thomas Zeume References 1. Baader, F.: Augmenting concept languages by transitive closure of roles: An al- ternative to terminological cycles. In: Proceedings of IJCAI. pp. 446–451. Morgan Kaufmann (1991) 2. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017) 3. Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched µ-calculi. Logical Methods in Computer Science 4(3) (2008) 4. Bonatti, P.A., Peron, A.: On the undecidability of logics with converse, nominals, recursion and counting. Artif. Intell. 158(1), 75–96 (2004) 5. Calvanese, D., Eiter, T., Ortiz, M.: Regular path queries in expressive description logics with nominals. In: Proceedings of IJCAI. pp. 714–720 (2009) 6. De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proceedings of AAAI. pp. 205–212 (1994) 7. Duc, C.L., Lamolle, M.: Decidability of description logics with transitive closure of roles in concept and role inclusion axioms. In: Proceedings of DL. CEUR Workshop Proceedings, vol. 573. CEUR-WS.org (2010) 8. Duc, C.L., Lamolle, M., Curé, O.: A decision procedure for SHOIQ with transitive closure of roles. In: Proceedings of ISWC. LNCS, vol. 8218, pp. 264–279. Springer (2013) 9. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979) 10. Giacomo, G.D.: Decidability of class-based knowledge representation formalisms. Ph.D. thesis, Universita di Roma “La Sapienza” (1995) 11. Giacomo, G.D., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Proceedings of KR. pp. 316–327. Morgan Kaufmann (1996) 12. Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings of LICS. pp. 306–317. IEEE Computer Society (1997) 13. Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Arch. Math. Log. 38(4-5), 313–354 (1999) 14. Haase, C.: A survival guide to presburger arithmetic. SIGLOG News 5(3), 67–82 (2018) 15. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proceed- ings of KR. pp. 57–67 (2006) 16. Keisler, H.J.: Model Theory for Infinitary Logic: Logic with Countable Conjunc- tions and Finite Quantifiers. North Holland Publishing Company (1971) 17. Kieronski, E.: Decidability issues for two-variable logics with several linear orders. In: Proceedings of CSL. pp. 337–351 (2011) 18. Kieronski, E., Otto, M.: Small substructures and decidability issues for first-order logic with two variables. J. Symb. Log. 77(3), 729–765 (2012) 19. Kieronski, E., Pratt-Hartmann, I., Tendera, L.: Two-variable logics with counting and semantic constraints. SIGLOG News 5(3), 22–43 (2018), https://dl.acm.org/citation.cfm?id=3242958 20. Kotek, T., Simkus, M., Veith, H., Zuleger, F.: Extending ALCQIO with trees. In: Proceedings of LICS. pp. 511–522 (2015) 21. Otto, M.: Two variable first-order logic over ordered domains. J. Symb. Log. 66(2), 685–702 (2001) ALCOIF with Transitive Closure (and More) 13 22. OWL Working Group, W.: OWL 2 Web Ontology Language: Docu- ment Overview. W3C Recommendation (27 October 2009), available at http://www.w3.org/TR/owl2-overview/ 23. Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two- variable logic with counting. SIAM J. Comput. 29(4), 1083–1117 (2000) 24. Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quan- tifiers. Journal of Logic, Language and Information 14(3), 369–395 (2005) 25. Pratt-Hartmann, I.: Complexity of the guarded two-variable fragment with count- ing quantifiers. J. Log. Comput. 17(1), 133–155 (2007) 26. Pratt-Hartmann, I.: The two-variable fragment with counting and equivalence. Mathematical Logic Quarterly 61(6), 474–515 (2015) 27. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. pp. 92— -101 (1929) 28. Rudolph, S.: Undecidability results for database-inspired reasoning problems in very expressive description logics. In: Proceedings of KR. pp. 247–257. AAAI Press (2016) 29. Schwentick, T., Zeume, T.: Two-variable logic with two order relations. Logical Methods in Computer Science 8(1) (2012) 30. Slutzki, G.: Alternating tree automata. Theor. Comput. Sci. 41, 305–318 (1985) 31. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artif. Intell. Res. 12, 199–217 (2000) 32. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Proceedings of ICALP. pp. 628–641 (1998) 33. Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Proceedings of CADE. pp. 337–352 (2005) 34. Zeume, T., Harwath, F.: Order-invariance of two-variable logic is decidable. In: Proceedings of LICS. pp. 807–816 (2016)