The Influence of the Test Operator on the Expressive Powers of PDL-Like Logics Linh Anh Nguyen Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland nguyen@mimuw.edu.pl Abstract. Berman and Paterson proved that Test-Free PDL is weaker than PDL. As the description logics ALC trans and ALC reg are, respec- tively, variants of Test-Free PDL and PDL, there is a concept of ALC reg that is not equivalent to any concept of ALC trans . Generalizing this, we show that there is a concept of ALC reg that is not equivalent to any concept of the logic that extends ALC trans with inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the de- terministic Horn fragment of ALC reg . 1 Introduction Propositional Dynamic Logic (PDL) is a well-known modal logic for reasoning about computer programs [5,7]. Its variant ALC reg is a description logic (DL) for reasoning about terminological knowledge [16]. Berman and Paterson [2] proved that Test-Free PDL is weaker than PDL. In particular, they gave a formula of PDL that is not equivalent to any formula of Test-Free PDL. This means that there is a concept of ALC reg that is not equivalent to any concept of ALC trans (a variant of Test-Free PDL). While bisimulations are usually used for separat- ing the expressive powers of modal and description logics (see, e.g., [3,4,10]), the proof given by Berman and Paterson [2] exploits the fact that “over a sin- gle symbol alphabet, the regular sets are precisely those which are ultimately periodic” (see [6, Theorem 3.1.2]) and is somehow similar to the proof of that connectivity is inexpressible in first-order logic. Generalizing the result and method of Berman and Paterson, in Section 3 we prove that there is a concept of ALC reg that is not equivalent to any concept of the DL ALCIOQUSelf trans , which extends ALC trans with inverse roles (I), nominals (O), qualified number restrictions (Q), the universal role (U) and local reflexivity of roles (Self ) as of the DL SROIQ [8]. That is, extending ALC trans with the features I, O, Q, U and Self does not help in expressing the test operator. Modifying the proof of Berman and Paterson [2] for dealing with the features O, Q, U and Self can be done in a rather straightforward way (see our Lemmas 1, 3, 4 and their proofs). However, dealing with inverse roles (I) 2 L.A. Nguyen requires an advanced refinement, as regular sets over an alphabet consisting of an atomic role and its inverse need not be ultimately periodic. The proof of our Lemma 2 is more sophisticated than the proof of [6, Theorem 3.1.2]. In Section 4, we provide a result stating that using regular RBoxes and acyclic TBoxes for ALCIOQUSelf trans does not help in expressing tests, but using simple stratified TBoxes under the stratified semantics on the background allows us to express every concept by another without tests. A further result states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALC reg . This suggests that tests can be eliminated from tractable1 Horn fragments of PDL-like logics. 2 Preliminaries This section provides notions and definitions related with syntax and semantics of DLs [1]. We denote the sets of concept names, role names and individual names by C, R+ and I, respectively. A concept name is an atomic concept, a role name is an atomic role. Let R = R+ ∪ R− , where R− = {r | r ∈ R+ } and r is called the inverse of r. We call elements of R basic roles. We distinguish a subset of R+ whose elements are called simple roles. If r ∈ R+ is a simple role, then r is also a simple role. The set Σ = C ∪ R+ ∪ I is called the signature. Let Φ ⊆ {I, O, Q, U, Self }, where the symbols mean inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles, respectively. Roles and concepts of the DLs ALC, ALC +Φ, (ALC +Φ)trans and (ALC +Φ)reg are defined as follows. If L = ALC, then: – if r ∈ R+ , then r is a role of L, – if A ∈ C, then A is a concept of L, – > and ⊥ are concepts of L, – if C and D are concepts of L and R is a role of L, then ¬C, C t D, C u D, ∃R.C and ∀R.C are concepts of L. If L = ALC +Φ, then additionally: – if I ∈ Φ and R is a role of L, then R is a role of L, – if O ∈ Φ and a ∈ I, then {a} is a concept of L, – if Q ∈ Φ, n ∈ N, C is a concept of L, R is a simple role of L (i.e., a simple role that is a role of L), then ≥ n R.C and ≤ n R.C are concepts of L, – if U ∈ Φ, then U is a role of L, – if Self ∈ Φ and r ∈ R+ , then ∃r.Self is a concept of L. If L = (ALC +Φ)trans , then additionally: – ε is a role of L, – if R and S are roles of L and are different from U , then R t S, R ◦ S and R∗ are roles of L. 1 I.e., with a PTime or lower data complexity. The Influence of the Test Operator on the Expressive Power 3 I ⊥I = ∅ >I = ∆I {a}I = {aI } (¬C)I = ∆I \ C I R = (RI )−1 (C u D)I = C I ∩ DI (C t D)I = C I ∪ DI εI = {hx, xi | x ∈ ∆I } (∃R.C)I = {x ∈ ∆I | ∃y (hx, yi ∈ RI ∧ y ∈ C I )} (R ◦ S)I = RI ◦ S I (∀R.C)I = {x ∈ ∆I | ∀y (hx, yi ∈ RI ⇒ y ∈ C I )} (R t S)I = RI ∪ S I (∃R.Self )I = {x ∈ ∆I | hx, xi ∈ RI } (R∗ )I = (RI )∗ (≥ n R.C)I = {x ∈ ∆I | ]{y | hx, yi ∈ RI ∧ y ∈ C I } ≥ n} (C?)I = {hx, xi | x ∈ C I } (≤ n R.C)I = {x ∈ ∆I | ]{y | hx, yi ∈ RI ∧ y ∈ C I } ≤ n} U I = ∆I × ∆I Fig. 1. Semantics of complex concepts and complex roles. If L = (ALC +Φ)reg , then additionally: – if C is a concept of L, then C? is a role of L. This constructor is called the test operator. When Φ = ∅, we shorten the names (ALC +Φ)trans and (ALC +Φ)reg to ALC trans and ALC reg , respectively. Similarly, we write ALCIOQUSelf trans to denote (ALC +Φ)trans with Φ = {I, O, Q, U, Self }, and so on. We denote atomic concepts by letters like A or B, atomic roles by letters like r or s, and individual names by letters like a or b. We use letters C and D to denote (arbitrary) concepts, R and S to denote (arbitrary) roles. An interpretation is a pair I = h∆I , ·I i, where ∆I is a non-empty set, called the domain, and ·I is the interpretation function of I that maps each a ∈ I to aI ∈ ∆I , each A ∈ C to a subset AI of ∆I , and each r ∈ R+ to a relation rI ⊆ ∆I × ∆I . The function ·I is extended to interpret complex roles and concepts as specified in Figure 1. Concepts C and D are equivalent, denoted by C ≡ D, if C I = DI for all interpretations I. Similarly, roles R and S are equivalent, denoted by R ≡ S, if RI = S I for all interpretations I. If L is a sublogic of L0 (like (ALC +Φ)trans is a sublogic of (ALC +Φ)reg ), then we say that L is weaker (or less expressive) than L0 (in expressing concepts) if there exists a concept C of L0 that is not equivalent to any concept of L. 2.1 RBoxes A finite set S of context-free production rules over R is called a context-free semi- Thue system over R. It is symmetric if R → S k . . . S 1 belongs to S for every production rule R → S1 . . . Sk of S.2 It is regular if the language consisting of words derivable from any R ∈ R is regular. Assume that R is derivable from itself. 2 If k = 0, then the RHS (right hand side) of each of the rules represents the empty word ε. 4 L.A. Nguyen A role inclusion axiom (RIA) has the form S1 ◦ · · · ◦ Sk v R, where k ≥ 0 and S1 , . . . , Sk , R are basic roles. If k = 0, then the LHS (left hand side) of the inclusion stands for ε. A (regular) RBox is a finite set R of RIAs such that S = {R → S1 . . . Sk | (S1 ◦ · · · ◦ Sk v R) ∈ R} is a regular and symmetric semi-Thue system with the property that only ε and words with length 1 can be derived from any simple role R ∈ R. An RBox is allowed for a DL L if it uses inverse roles only when they are allowed for L. Since it is undecidable whether a context-free semi-Thue system is regular, we assume that each RBox R is accompanied by a mapping πR that associates each R ∈ R with a regular expression πR (R) that generates the set of words derivable from R using the rules of the corresponding semi-Thue system. If S1 ◦ · · · ◦ Sk v R is a RIA of R, then we call R an intensional predi- cate specified by R. An interpretation I validates a RIA S1 ◦ · · · ◦ Sk v R if (S1 ◦ · · · ◦ Sk )I ⊆ RI . It is a model of an RBox R if it validates all RIAs of R. 2.2 TBoxes A TBox axiom (or terminological axiom) is either a general concept inclusion . . (GCI) C v D or a concept equivalence C = D. A concept equivalence A = D (where A ∈ C) is called a concept definition. A TBox is a finite set of TBox axioms. It is allowed for a DL L if it uses only concepts of L. An interpretation . I validates C v D (resp. C = D) if C I ⊆ DI (resp. C I = DI ). It is a model of a TBox T if it validates all axioms of T . A TBox T is acyclic if there exist concept names A1 , . . . , An such that T . consists of n axioms and the i-th axiom of T is of the form Ai = C, C v Ai or Ai v C, where C does not use the concept names Ai , . . . , An . The concept names A1 , . . . , An are called intensional predicates specified by T . A TBox T is called a simple stratified TBox if there exists a partition (T1 , . . . , Tn ) of T , called a stratification of T , such that, for each 1 ≤ i ≤ n, Ti = {Ci,j v Ai,j | 1 ≤ j ≤ ni }, where each Ai,j is a concept name that does not occur in T1 , . . . , Ti−1 and may occur at the LHS of v in the axioms of Ti only under the scope of u, t and ∃. The concept names Ai,j , for 1 ≤ i ≤ n and 1 ≤ j ≤ ni , are called intensional predicates specified by T . Note that negation (¬) is allowed at the LHS of v in GCIs of a simple stratified TBox, but it can be applied only to concepts that do not use the predicates defined in the current or later strata. 3 The First Result In this section, we prove the following theorem: Theorem 1. There is no concept of ALCIOQUSelf trans equiv- alent to the concept C = ∃((r ◦ A?)∗ ◦ r ◦ B? ◦ r ◦ A?).> or C = ∃((r ◦ A?)∗ ◦ r ◦ (¬A)? ◦ r ◦ A?).> of ALC reg . The Influence of the Test Operator on the Expressive Power 5 To prove this theorem we will use a family of interpretations Im = h∆Im , ·Im i, m > 1, illustrated and specified as follows: w2m w1 wm−1 wm wm+1 w2m−1 r / ··· r / r / r / r / ··· r / r / B B A A B A A r  ai  w0  r B ^== == r =  w−1 w−m+1 w−m w−m−1 w−2m+1 w−2m o ··· o o o o ··· o o r r r r r r r A A B A A B – ∆Im = {w−2m , w−2m+1 , . . . , w2m }, – rIm = {hwi , wi+1 i, hw2m , w−2m i | −2m ≤ i < 2m}, – sIm = ∅ for s ∈ R+ − {r}, – B Im = {w−2m , w−m , w0 , wm , w2m }, – AIm = ∆Im − B Im , – C Im = ∅ for C ∈ C − {A, B}, – aIm = w2m for a ∈ I. Note that |∆Im | = 4m + 1. Comparing Im with the structure Am used in [2], note that the domain of Am has the size 2m+1, Am does not deal with nominals, and only one propositional variable is interpreted in Am as a non-empty subset of the domain. Observe that, for C being one of the two concepts mentioned in Theorem 1, w0 ∈ C Im but wm ∈ / C Im . The structure of the proof of Theorem 1 is as follows. Given any concept D of ALCIOQUSelf trans , we first transform it to a concept D2 of ALCIOtrans over the signature {r, A, B, a} such that D2Im = DIm for all m > 1 (see Lemma 1). We then transform D2 to a concept D3 such that D3Im = D2Im for all m > 1, the ∗ operator is used only for rn and rn for some n (see Lemma 2), and for every subconcept ∃R.D30 or ∀R.D30 of D3 , R is of the form r, r, (rn )∗ or (rn )∗ for some n ≥ 1 (see Lemma 3). Next, we show that there exists m > 1 such that w0 ∈ D3Im ⇔ wm ∈ D3Im (see Lemma 4). Thus, for that m, C Im 6= D3Im , and therefore, C is not equivalent to D (since D3Im = D2Im = DIm ). Lemma 1. For any concept C of ALCIOQUSelf trans , there exists a concept D of ALCIOtrans over the signature {r, A, B, a} such that DIm = C Im for all m > 1. Proof. Let D be the concept obtained from C by: – replacing every subconcept 6 L.A. Nguyen • ≥ n R.E, where n ≥ 2, by ⊥, • ≤ 0 R.E by ∀R.¬E, • ≥ 1 R.E by ∃R.E, • ∃U.E by ∃r∗ .E, • ≥ 0 R.E by >, • ∀U.E by ∀r∗ .E, • ≤ n R.E, where n ≥ 1, by >, • ∃R.Self by ⊥, – replacing every concept name different from A and B by ⊥, – replacing every nominal {b}, where b 6= a, by {a}, – replacing every role name s different from r by ∅, – repeatedly replacing every role ∅ t R or R t ∅ by R, every role ∅∗ by ε, and every role ∅, ∅ ◦ R or R ◦ ∅ by ∅, – replacing every subconcept ∃∅.E by ⊥, and every ∀∅.E by >. It is easy to see that D satisfies the properties mentioned in the lemma.  We treat a word R1 . . . Rk over the alphabet {r, r} as the role R1 ◦ · · · ◦ Rk , and by Rn we denote the composition of n copies of R. Thus, R0 = ε. Conversely, a role R without tests that uses only basic roles r and r is treated as a regular expression over the alphabet {r, r} (where t stands for ∪, and ◦ for ;). For such a role R, by L(R) we denote the regular language generated by R. For a word R over the alphabet {r, r}, by |R| we denote the length of R (defined in the usual way), and by ||R|| we denote the norm of R, which is defined as follows: ||ε|| = 0, ||r|| = 1, ||r|| = −1, ||RS|| = ||R|| + ||S||. Observe that, for words R and S over the alphabet {r, r}, if ||R|| = ||S||, then RIm = S Im for all m > 1. Lemma 2. Let R be a role without tests that uses only basic roles r and r. Then, there exists a role S such that S Im = RIm for all m > 1 and the ∗ operator can be used in S only for rn and rn for some n. Proof. Since L(R) is a regular language, by the pumping lemma, there exists an integer p > 0 such that every word from L(R) of length at least p can be represented as xyz such that |y| > 0, |xy| ≤ p and xy i z ∈ L(R) for all i ≥ 0. Let n = p(p − 1) · · · 2 · 1 and let L0 be the language obtained from L(R) by deleting all words y such that there exists x ∈ L(R) with |x| < |y| and ||x|| = ||y||. By pumping(x, y, z) we denote the formula xyz ∈ L0 ∧ |y| > 0 ∧ |xy| ≤ p ∧ ∀i ≥ 0 xy i z ∈ L(R). Observe that, if w0 = xyz ∈ L0 and pumping(x, y, z) holds, then: – ||y|| =6 0 because otherwise we would have xz ∈ L(R), |xz| < |w0 | and ||xz|| = ||w0 ||, which contradict the definition of L0 ; – if ||y|| > 0 then, for all i ≥ 0, there exists u ∈ L(R) with ||u|| = ||w0 (rn )i ||; – if ||y|| < 0 then, for all i ≥ 0, there exists u ∈ L(R) with ||u|| = ||w0 (rn )i ||. Denote this observation by (?). For each integer j, 0 ≤ j < n, let Kj+ = {||xyz|| : pumping(x, y, z), n | (||xyz|| − j) and ||y|| > 0} Kj− = {||xyz|| : pumping(x, y, z), n | (||xyz|| − j) and ||y|| < 0}. The Influence of the Test Operator on the Expressive Power 7 For intuition, informally, we intend to define S to be the role G G G S1 t (( S2 ) ◦ (rn )∗ ) t (( S3 ) ◦ (rn )∗ ), (1) where S1 , S2 and S3 are the finite sets of words over the alphabet {r, r} con- structed as follows: – S1 := {x ∈ L0 : |x| < p}, S2 := ∅, S3 := ∅; – for each j from 0 to n − 1 do • if Kj+ 6= ∅ then - if Kj+ does not have a minimum then add rj to both S2 and S3 ; - else: let k = min Kj+ , if k ≥ 0 then S2 := S2 ∪ {rk } else S2 := S2 ∪ {(r)−k } (for this second case, notice that −k is a positive integer); • if Kj− 6= ∅ then - if Kj− does not have a maximum then add rj to both S2 and S3 ; - else: let k = max Kj− , if k ≥ 0 then S3 := S3 ∪ {rk } else S3 := S3 ∪ {(r)−k }. Formally, we define S to be the role obtained from (1) by deleting any i-th main disjunct such that Si is empty, for i ∈ {1, 2, 3}. To prove that S Im = RIm for all m > 1 it is sufficient to show that: 1. if w ∈ L(S), then there exists u ∈ L(R) such that ||u|| = ||w||, 2. if w ∈ L(R), then there exists u ∈ L(S) such that ||u|| = ||w||. Consider the assertion (1) and let w ∈ L(S). There are the following cases: – Case w ∈ S1 : We have that w ∈ L0 ⊆ L(R). Just take u = w. – Case w = rj (rn )h , Kj+ 6= ∅ and Kj+ does not have a minimum: Thus, there exists w0 = xyz ∈ L0 such that pumping(x, y, z) holds, ||y|| > 0 and ||w0 || = j + n · h0 for some h0 < h. By (?), there exists u ∈ L(R) such that ||u|| = ||w||. – Case w = rk (rn )h , Kj+ 6= ∅, k = min Kj+ and k ≥ 0: Thus, there exists w0 = xyz ∈ L0 such that pumping(x, y, z) holds, ||y|| > 0 and ||w0 || = k. By (?), there exists u ∈ L(R) such that ||u|| = ||w||. – Case w = (r)−k (rn )h , Kj+ 6= ∅, k = min Kj+ and k < 0: Thus, there exists xyz ∈ L0 such that pumping(x, y, z) holds, ||y|| > 0 and ||w0 || = k. Notice that ||(r)−k || = k. By (?), there exists u ∈ L(R) such that ||u|| = ||w||. – Case w = rj (rn )h , Kj− 6= ∅ and Kj− does not have a maximum: Thus, there exists w0 = xyz ∈ L0 such that pumping(x, y, z) holds, ||y|| < 0 and ||w0 || = j + n · h0 for some h0 > h. By (?), there exists u ∈ L(R) such that ||u|| = ||w||. – The four previous cases are related to S2 . The four remaining cases, which are related to S3 , can be dealt with in a similar way. Consider the assertion (2) and let w ∈ L(R). There exists w0 ∈ L0 such that ||w || = ||w||. If |w0 | < p, then w0 ∈ S1 and we can just take u = w0 . Suppose 0 |w0 | ≥ p. Thus, w0 can be represented as xyz such that pumping(x, y, z) holds. There are the following cases: 8 L.A. Nguyen – Case ||y|| > 0: There exists 0 ≤ j < n such that ||w0 || ∈ Kj+ and ||w0 || = j + n · i for some integer i. Consider the following subcases. • Case Kj+ does not have a minimum: Thus, rj ∈ S2 . Taking u = rj (rn )i , we have that u ∈ L(S) and ||u|| = ||w0 || = ||w||. • Case k = min Kj+ and k ≥ 0: Thus, rk ∈ S2 . Observe that ||w0 || ≥ k 0 and n | (||w0 || − k). Taking u = r||w || , we have that u ∈ L(S) and ||u|| = ||w0 || = ||w||. • Case k = min Kj+ and k < 0: Thus, (r)−k ∈ S2 . Observe that ||w0 || ≥ k 0 and n | (||w0 || − k). Taking u = (r)−k (r||w ||−k ), we have that u ∈ L(S) and ||u|| = ||w0 || = ||w||. – The case when ||y|| < 0 is dual to the above case and can be dealt with analogously.  Let C denote the set of concepts C of ALCIOtrans over the signature {r, A, B, a} such that, for every subconcept ∃R.D or ∀R.D of C, R is of the form r, r, (rn )∗ or (rn )∗ for some n ≥ 1. Lemma 3. For any concept C of ALCIOtrans over the signature {r, A, B, a}, there exists a concept D ∈ C such that DIm = C Im for all m > 1. Proof. Let E be the concept obtained from C by replacing every role R by a role S that satisfies the conditions mentioned in Lemma 2. We have E Im = C Im for all m > 1. Then, let D be obtained from E by repeatedly applying the following transformations: ∃(R t S).F ≡ ∃R.F t ∃R.F ∀(R t S).F ≡ ∀R.F u ∀R.F ∃(R ◦ S).F ≡ ∃R.∃S.F ∀(R ◦ S).F ≡ ∀R.∀S.F ∃ε.F ≡ F ∀ε.F ≡ F. It is clear that D ∈ C and DIm = E Im = C Im for all m > 1.  For a concept C ∈ C, by nr (C) we denote the number of occurrences of ∃r, ∃r, ∀r and ∀r in C. Lemma 4. For any concept C ∈ C and integers m and k such that m > 1, 4m + 1 is prime and nr (C) < m − |k|, we have wk ∈ C Im ⇔ wk+m ∈ C Im . Proof. This proof is similar to the one of [2, Lemma 3]. The intuition is as follows: – a concept C 0 can distinguish wk and wk+m only if nr (C 0 ) is large enough so that the checking can recognize that the neighborhood of wk differs from the corresponding neighborhood of wk+m , in particular, to recognize that the first one contains wm+1 (resp. w−m−1 ) and the second one contains w−2m (resp. w2m ); the reason is that, since 4m + 1 is prime, either ((rn )∗ )Im = ∆Im × ∆Im or hwi , wj i ∈ ((rn )∗ )Im iff j = i; – since nr (C) < m − |k|, C cannot distinguish wk and wk+m . The Influence of the Test Operator on the Expressive Power 9 Observe that −m < k < m. We prove this lemma by induction on the structure of C. The cases when C is A, B, > or ⊥ are trivial. The cases when C is of the form D u E or ∀R.D are reduced to the cases of ¬(¬D t ¬E) and ¬∃R.¬D, respectively. – Case C = {a}: Since aIm = w2m , wk ∈ / C Im and wk+m ∈ / C Im . – Case C = ¬D: We have nr (D) = nr (C). By induction, wk ∈ DIm ⇔ wk+m ∈ DIm , and hence, wk ∈ C Im ⇔ wk+m ∈ C Im . – Case C = DtE: We have nr (D) ≤ nr (C) and nr (E) ≤ nr (C). By induction, wk ∈ DIm ⇔ wk+m ∈ DIm and wk ∈ E Im ⇔ wk+m ∈ E Im , which imply that wk ∈ C Im ⇔ wk+m ∈ C Im . – Case C = ∃r.D: We have nr (D) = nr (C) − 1 < m − |k| − 1 ≤ m − |k + 1|. By induction, wk+1 ∈ DIm ⇔ wk+1+m ∈ DIm . Hence, wk ∈ (∃r.D)Im ⇔ wk+m ∈ (∃r.D)Im , which means wk ∈ C Im ⇔ wk+m ∈ C Im . – Case C = ∃r.D: We have nr (D) = nr (C) − 1 < m − |k| − 1 ≤ m − |k − 1|. By induction, wk−1 ∈ DIm ⇔ wk−1+m ∈ DIm . Similarly to the previous case, this implies that wk ∈ (∃r.D)Im ⇔ wk+m ∈ (∃r.D)Im , which means wk ∈ C Im ⇔ wk+m ∈ C Im . – Case C = ∃(rn )∗ .D and (4m + 1)|n : We have hwi , wj i ∈ ((rn )∗ )Im iff j = i. Hence, wk ∈ (∃(rn )∗ .D)Im ⇔ wk ∈ DIm wk+m ∈ (∃(rn )∗ .D)Im ⇔ wk+m ∈ DIm . We have nr (D) = nr (C). By induction, wk ∈ DIm ⇔ wk+m ∈ DIm . There- fore, wk ∈ C Im ⇔ wk+m ∈ C Im . – Case C = ∃(rn )∗ .D and (4m + 1)6 | n : Since 4m + 1 is prime, 0, n, 2n, 3n, . . . , (4m)n have all 4m + 1 different residues modulo 4m + 1. Hence, hwi , wj i ∈ ((rn )∗ )Im for all wi , wj ∈ ∆Im , and wk ∈ (∃(rn )∗ .D)Im ⇔ wk+m ∈ (∃(rn )∗ .D)Im , because they are both equivalent to that there exists wj ∈ DIm . Therefore, wk ∈ C Im ⇔ wk+m ∈ C Im . – The case C = ∃(rn )∗ .D is similar to the two previous cases.  We now recall and prove Theorem 1. Theorem 1 There is no concept of ALCIOQUSelf trans equiv- alent to the concept C = ∃((r ◦ A?)∗ ◦ r ◦ B? ◦ r ◦ A?).> or ∗ C = ∃((r ◦ A?) ◦ r ◦ (¬A)? ◦ r ◦ A?).> of ALC reg . Proof. For a contradiction, suppose D is a concept of ALCIOQUSelf trans equiv- alent to C. By Lemma 1, there exists a concept D2 of ALCIOtrans over the signa- ture {r, A, B, a} such that D2Im = DIm for all m > 1. By Lemma 3, there exists a concept D3 ∈ C such that D3Im = D2Im for all m > 1. Let m be an integer such that m > nr (D3 ) and 4m + 1 is prime. By Lemma 4, w0 ∈ D3Im ⇔ wm ∈ D3Im . This contradicts the facts that D3Im = D2Im = DIm = C Im , w0 ∈ C Im and wm ∈/ C Im .  10 L.A. Nguyen Corollary 1. For any Φ ⊆ {I, O, Q, U, Self }, (ALC +Φ)trans is weaker than (ALC +Φ)reg in expressing concepts. 4 Dealing with RBoxes and TBoxes The result of the previous section roughly states that, without using RBoxes and TBoxes, it is hard to eliminate tests, at least it is impossible to eliminate tests from ALCIOQUSelf reg without decreasing the expressive power. As expected, using acyclic TBoxes that consist only of concept definitions do not help in expressing tests. The first result of this section states that using RBoxes and acyclic TBoxes that are defined more liberally as in Section 2 does not help either. The second result states that, however, using simple stratified TBoxes under the stratified semantics on the background, it is possible to express every concept by another without tests. The third result states that tests can be eliminated from the deterministic Horn fragment of ALC reg . Due to the lack of space, proofs of these results are provided only in the long version [11] of the current paper. 4.1 The Case with RBoxes and Acyclic TBoxes We say that a concept C is inexpressible in a DL L even when using RBoxes and acyclic TBoxes if, for every concept D, every RBox R and every acyclic TBox T of L such that the intensional predicates specified by R and T do not occur in C, there exists a model I of R and T such that C I 6= DI . Proposition 1. The concept C = ∃((r ◦ A?)∗ ◦ r ◦ B? ◦ r ◦ A?).> or ∗ C = ∃((r ◦ A?) ◦ r ◦ (¬A)? ◦ r ◦ A?).> of ALC reg is inexpressible in ALCIOQUSelf trans even when using RBoxes and acyclic TBoxes. 4.2 Eliminating Tests from Concepts by Simple Stratified TBoxes Let T be a simple stratified TBox. An interpretation I is called a standard model of T (under the stratified semantics) if there exist a partition (T1 , . . . , Tn ) of T and interpretations J0 , . . . , Jn such that: – Ti = {Ci,j v Ai,j | 1 ≤ j ≤ ni } for 1 ≤ i ≤ n, – Jn = I and ∆Ji = ∆I for all 0 ≤ i < n, – xJ0 = xI for all x ∈ Σ − {Ai,j | 1 ≤ i ≤ n and 1 ≤ j ≤ ni }, – for each 1 ≤ i ≤ n, xJi = xJi−1 for all x ∈ Σ−{Ai0 ,j | i ≤ i0 ≤ n, 1 ≤ j ≤ ni0 } and AJ i,j , for 1 ≤ j ≤ ni , are the smallest subsets of ∆ i Ji such that AJ Ji i,j = Ci,j . i It can be shown that, for every interpretation J0 , there exists a unique standard model I of T such that ∆I = ∆J0 and xI = xJ0 for all x ∈ Σ −{Ai,j | 1 ≤ i ≤ n and 1 ≤ j ≤ ni }. We call it the standard model of T based on J0 . In what follows, let Φ ⊆ {I, O, Q, U, Self } (in general, extending Φ with other features does not affect Proposition 2 given below). Let C be a concept of (ALC +Φ)reg , D a concept and T a simple stratified TBox of (ALC +Φ)trans such The Influence of the Test Operator on the Expressive Power 11 that the intensional predicates specified by T do not occur in C. We say that C is expressed by D and T under the stratified semantics if, for every standard model I of T , C I = DI . Proposition 2. Every concept of (ALC +Φ)reg can be expressed by a concept and a simple stratified TBox of (ALC +Φ)trans under the stratified semantics. 4.3 Eliminating Tests from Horn TBoxes The previous subsection deals with eliminating tests from a standing alone con- cept by using a simple stratified TBox under the stratified semantics. Roughly speaking, it suggests that tests in PDL-like roles can be eliminated by using fixpoints outside roles. The result of this subsection states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALC reg . This is possible because the traditional semantics of such TBoxes has a fixpoint char- acterization. A role can be treated as a regular expression over the alphabet R+ ∪{C? | C is a concept}, where t and ◦ stand for ∪ and semicolon, respectively. Conversely, a word over this alphabet can be treated as a role. Given a role R, let L(R) denote the regular language generated by R and let ∀∃R.C be a new concept constructor whose semantics in an interpretation I is specified as follows: \ (∀∃R.C)I = {(∀S.∃S 0 .C)I | SS 0 ∈ L(R)}. Observe that, if R ∈ R+ , then ∀∃R.C ≡ ∀R.C u ∃R.C. The deterministic Horn fragment of ALC reg , denoted by D-Horn-ALC reg , is designed with the intention to be (probably) the most expressive fragment of ALC reg that has a PTime data complexity (under the traditional semantics). A D-Horn-ALC reg TBox axiom is an expression of the form Cl v Cr , where Cl and Cr are concepts defined by the following BNF grammar, with A ∈ C and s ∈ R+ : Cl ::= > | A | Cl u Cl | Cl t Cl | ∃Rl .Cl | ∀∃Rl .Cl (2) Rl ::= s | Rl ◦ Rl | Rl t Rl | Rl∗ | Cl ? (3) Cr ::= > | ⊥ | A | ¬Cl | Cr u Cr | ¬Cl t Cr | ∃Rr .Cr | ∀Rl .Cr (4) Rr ::= s | Rr ◦ Rr | Cr ? (5) A D-Horn-ALC reg TBox is a finite set of D-Horn-ALC reg TBox axioms. Remark 1. A (reduced) ABox is a finite set of assertions of the form A(a), ¬A(a) or r(a, b) (where A ∈ C and r ∈ R+ ). A knowledge base in D-Horn-ALC reg is a pair hT , Ai consisting of a D-Horn-ALC reg TBox T and an ABox A. The notion of whether an interpretation is a model of an ABox or a knowledge base is defined in the usual way. A knowledge base is satisfiable if it has a model. It can be proved that checking whether a given knowledge base hT , Ai in D-Horn-ALC reg 12 L.A. Nguyen is satisfiable is solvable in polynomial time in the size of the ABox A.3 That is, D-Horn-ALC reg has a PTime data complexity. If ∀∃ in (2) is replaced by ∀, then instead of D-Horn-ALC reg we obtain the general Horn fragment of ALC reg with a NP-hard data complexity for the satisfiability problem.4  The following theorem states that tests can be eliminated from D-Horn-ALC reg . Theorem 2. For every D-Horn-ALC reg TBox T over a signature Σ, there ex- ists a D-Horn-ALC reg TBox T 0 without tests over a signature Σ 0 ⊇ Σ such that: 0 1. for every model I of T , there exists a model I 0 of T 0 such that ∆I = ∆I 0 and xI = xI for all x ∈ Σ, 0 2. for every model I 0 of T 0 , the interpretation I over Σ specified by ∆I = ∆I I I0 and x = x for all x ∈ Σ is a model of T . 5 Conclusions Generalizing the result and method of Berman and Paterson [2], we have proved that there is a concept of ALC reg that is not equivalent to any concept of the DL that extends ALC trans with inverse roles, nominals, qualified number re- strictions, the universal role and local reflexivity of roles. This implies, among others, that CPDL (Converse-PDL) is more expressive than Test-Free CPDL, and GCPDL (Graded Converse-PDL) is more expressive than Test-Free GCPDL. Extending our result by applying the technique of [2], it can also be proved that CPDLn+1 (CPDL with at most n+1 levels of nesting of tests) is more expressive than CPDLn , and similarly for GCPDL. The other results of this paper state that, on the other hand, using simple stratified TBoxes under the stratified semantics on the background, it is possi- ble to express every concept by another without tests. Furthermore, tests can be eliminated from the deterministic Horn fragment D-Horn-ALC reg of ALC reg . If one extends D-Horn-ALC reg with other features (e.g., I, O, Q, U and Self ) appropriately so that the resulting language still has a PTime data complexity (cf. Horn-SHIQ [9], Horn-SROIQ [15] and Horn-DL [14]), then our elimination technique (presented in the long version [11] of the current paper) can still be applied. Besides, it is hard to define a fragment of ALC reg that is more expressive than D-Horn-ALC reg and still has a PTime data complexity under the tradi- tional semantics. So, we have a tendency to claim that tests can be eliminated from tractable Horn fragments of PDL-like logics. 3 A more general result was proved in [13] for D-Horn-CPDLreg , which extends D-Horn-ALC reg with inverse roles and regular RBoxes. 4 The hardness was shown for the general Horn fragment of ALC [12]. The Influence of the Test Operator on the Expressive Power 13 References 1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applica- tions. Cambridge University Press (2003) 2. Berman, F., Paterson, M.: Propositional dynamic logic is weaker without tests. Theor. Comput. Sci. 16, 321–328 (1981) 3. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2002) 4. Divroodi, A., Nguyen, L.: On bisimulations for description logics. Inf. Sci. 295, 465–493 (2015) 5. Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Com- put. Syst. Sci. 18(2), 194–211 (1979) 6. Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill, Inc. (1966) 7. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000) 8. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Pro- ceedings of KR. pp. 57–67. AAAI Press (2006) 9. Hustadt, U., Motik, B., Sattler, U.: Reasoning in description logics by a reduction to disjunctive Datalog. J. Autom. Reasoning 39(3), 351–384 (2007) 10. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: Model-theoretic charac- terizations and rewritability. In: Proceedings of IJCAI. pp. 983–988 (2011) 11. Nguyen, L.: A long version of the current paper. Available at http://www.mimuw. edu.pl/~nguyen/EPT.pdf 12. Nguyen, L.: Horn knowledge bases in regular description logics with PTime data complexity. Fundamenta Informaticae 104(4), 349–384 (2010) 13. Nguyen, L.: A deterministic Horn fragment of CPDLreg with PTime data complex- ity. Manuscript, http://www.mimuw.edu.pl/~nguyen/DHornCPDLreg.pdf (2018) 14. Nguyen, L., Nguyen, T., Szalas, A.: Towards richer rule languages with polynomial data complexity for the Semantic Web. Data Knowl. Eng. 96, 57–77 (2015) 15. Ortiz, M., Rudolph, S., Simkus, M.: Query answering in the Horn fragments of the description logics SHOIQ and SROIQ. In: Proc. of IJCAI. pp. 1039–1044 (2011) 16. Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proceedings of IJCAI. pp. 466–471 (1991)