The description logic (DL) SROIQ [1] provides a logical foundation for the new version of the web ontology language OWL 2.1 In comparison to the DL SHOIN which underpins the rst version of OWL,2 SROIQ provides several new constructors for classes and axioms. One of the new powerful features of SROIQ are so-called complex role inclusion axioms (RIAs) which allow for expressing implications between role chains and roles R1 Rn v R. It is wellknown that unrestricted usage of such axioms can easily lead to undecidability for modal and description logics [2{5], with a notable exception of the DL E L++ [6]. Therefore certain syntactic restrictions are imposed on RIAs in SROIQ to regain decidability. Speci cally, the restrictions ensure that RIAs R1 Rn v R when viewed as production rules for context-free grammars R ! R1 : : : Rn induce a regular language. In fact, the tableau-based reasoning procedure for SROIQ [1] does not use the syntactic restrictions directly, but takes as an input the resulting non-deterministic nite automata for RIAs. This means that it is possible to use exactly the same procedure for any set of RIAs for which the corresponding regular automata can be constructed. Unfortunately, the syntactic restrictions on RIAs in SROIQ are not satis ed in all cases when the language induced by the RIAs is regular. In fact, it is not possible to come up with such a most general syntactic restriction since, given a context-free grammar, it is in general not possible to determine whether it de nes a regular language (see, e.g., [7]). In this paper we analyse several common use cases of RIAs which correspond to regular languages but cannot be expressed within SROIQ. We then propose an extension of the syntactic restrictions for RIAs, which can capture such cases. Our restrictions have several nice properties, which could allow for their seamless integration into future revisions of OWL: 1 http://www.w3.org/TR/owl2-syntax/ 2 http://www.w3.org/TR/owl-ref/
1. Our restrictions are conservative over the restrictions in SROIQ. That is, every set of RIAs that satis es the restriction in SROIQ will automatically satisfy our restrictions. 2. Our restrictions can be veri ed in polynomial time in the size of RIAs. 3. Our restrictions are constructive, which means that there is a procedure that builds the corresponding regular automaton for every set of RIAs that satisfy our restrictions.
Concepts atomic concept nominal top concept negation conjunction existential restriction min cardinality exists self
Syntax
Semantics A fag > :C C u D 9R:C >nS:C 9S:Self
AI (given) faI g
I
I n CI CI \ DI fx j RI (x; CI ) 6= ;g fx j jjSI (x; CI )jj fx j hx; xi 2 SI g
ng 4. Finally, for any set of RIAs that induce a regular language, there exists a set of RIAs (containing possibly new roles) that satis es our syntactic restrictions and preserves the semantics of the old roles. This means that unlike the restrictions in SROIQ, our syntactic restrictions allow to express any regular complex role inclusion properties. 2
In this section we introduce syntax and semantics of the DL SROIQ [1]. A SROIQ vocabulary consists of countably in nite sets NC of atomic concepts, NR of atomic roles, and NI of individuals. A SROIQ role is either r 2 NR, an inverse role r with r 2 NR, or the universal role U . A role chain is a sequence of roles = R1 Rn, n 0, where Ri 6= U , 1 i n; when n = 0, is called the empty role chain and is denoted by . With 1 2 we denote the concatenation of role chains 1 and 2, and with R (R ) we denote the role chain obtained by appending (prepending) R to . We denote by Inv(R) the inverse of a role R de ned by Inv(R) := r when R = r, Inv(R) = r when R = r , and Inv(R) = U when R = U . The inverse of a role chain = R1 Rn is a role chain Inv( ) := Inv(Rn) Inv(R1).
The syntax and semantics of SROIQ is summarised in Table 1. The set of SROIQ concepts is recursively de ned using the constructors in the upper part of the table, where A 2 NC , C, D are concepts, R, S roles, a an individual, and n a positive integer. A SROIQ ontology is a set O of axioms listed in the lower part of Table 1, where is a role chain, R(i) and S(i) are roles, C, D concepts, and a, b individuals.
A regular order on roles is an irre exive transitive binary relation on roles such that R1 R2 i Inv(R1) R2. A (complex) role inclusion axiom (RIA) R1 Rn v R is said to be -regular, if either: (i) n = 2 and R1 = R2 = R, or (ii) n = 1 and R1 = Inv(R), or (iii) Ri R for 1 i n, or (iv) R1 = R and Ri R for 1 < i n, or (v) Rn = R and Ri R for 1 i < n. It is assumed that all RIAs in O are regular for some order .
Given an ontology O, let O be the extension of O with RIAs Inv( ) v Inv(R) for every v R 2 O. Let vO R be the smallest relation between role chains and roles such that: (i) R vO R for every role R, and (ii) vO R and 1R 2 v R0 2 O implies 1 2 vO R0.
vO R.
Lemma 1. Given an ontology O, role chain , and role R, it is possible to decide in polynomial time whether Proof. We de ne a context-free grammar with terminal symbols sR and nonterminal symbols AR for every role R, and production rules AR ! sR for every role R and AR ! AR1 : : : ARn for every RIA R1 Rn v R 2 O. It is easy to show that AR ! sR1 : : : sRn w.r.t. this grammar i R1 Rn vO R. Since the word problem (membership in the language) for context-free grammars is decidable in polynomial time (see, e.g. [8]), then so is the property tu
A role S is simple (w.r.t. O) if vO S implies = R for some role R. It is required that all roles S(i) in Table 1 are simple w.r.t. O. Other constructors and axioms of SROIQ such as disjunction, universal restriction, role (ir)re exivity, and role (a)symetry can be expressed using the given ones.
The semantics of SROIQ is de ned using interpretations. An interpretation is a pair I = ( I ; I ) where I is a non-empty set called the domain of the interpretation and I is the interpretation function, which assigns to every A 2 NC a set AI I , to every r 2 NR a relation rI 2 I I , and to every a 2 NI an element aI 2 I . The interpretation is extended to roles by U I = I I and (r )I = fhx; yi j hy; xi 2 rI g, and to role chains by (R1 Rn)I = R1I RnI where is the composition of binary relations. The empty role chain is interpreted by I = fhx; xi j x 2 I g.
The interpretation of concepts is de ned according to the right column of the upper part of Table 1, where (x; V ) for I I , V I , and x 2 I denotes the set fy j hx; yi 2 ^ y 2 V g, and jjV jj denotes the cardinality of a set V I . An interpretation I satis es an axiom (written I j= ) if the respective condition to the right of the axiom in Table 1 holds; I is a model of an ontology O (written I j= O) if I satis es every axiom in O. We say that is a (logical) consequence of O or is entailed by O (written O j= ) if every model of O satis es . vO R. 3
Given an ontology O, for every role R, we de ne a language LO(R) consisting of role chains (viewed as nite words over roles) as follows:
LO(R) := f j
vO Rg
(
Example 1. Consider an ontology O consisting of the RIAs (
LO(isPartOf) = (isPartOf j isProperPartOf)+
Since isProperPartOf is implied only by axiom (
LO(isProperPartOf) = (isPartOf j isProperPartOf) isProperPartOf
Thus, the languages LO(isPartOf) and LO(isProperPartOf) induced by RIAs
(
In fact, there is no SROIQ ontology O that could express properties (
Axioms such as (
(
Recently, complex RIAs over parthood relations have been proposed as an alternative to SEP-triplet encoding [9]. The SEP-triplet encoding was introduced [10] as a technique to enable the propagation of some properties over parthood relations, while ensuring that other properties are not propagated. For example, if a nger is de ned as part of a hand, then an injury to a nger should be classi ed as an injury to the hand, however, the amputation of a nger should not be classi ed as an amputation of the hand. The SEP-triplet encoding does not use the parthood relations explicitly, but simulates them via inclusion axioms between special triplets of classes. Every primary class U gives rise to a triplet of classes consisting of the structure class US describing all parts of U including U itself, the entity class UE that is equivalent to U , and the part class UP describing the proper parts of U . Thus the axioms FingerE v FingerS, FingerP v FingerS, as well as HandE v HandS, HandP v HandS describe the relations between the classes within the triples, and one can use the axiom FingerS v HandP to express that nger is a proper part of hand. Several drawbacks of this encoding was mentioned and it had been argued that the explicit usage of the parthood relations can reduce the complexity of the ontology and at the same time eliminate the potential problems [9]. Thus, the axiom stating that nger is a proper part of hand can be written in this setting directly as follows:
(
Another situation where -regularity is too restrictive, is when \sibling relations" between elements having common parents are to be expressed. Such relations appear, for example, when speaking about parts that belong to the same vehicle. The sibling relations can be expressed using the following RIAs: isChildOf isChildOf
v isSiblingOf
isSiblingOf isSiblingOf v isSiblingOf
isSiblingOf isChildOf v isChildOf
(
LO(isChildOf) = ((isChildOf isChildOf ) j isSiblingOf) isChildOf (15) (16) In the next section, we demonstrate how our extended regularity conditions can capture such kind of axioms as well. 4
De nition 1. A preorder (a transitive re exive relation) - on roles is said to be admissible for an ontology O if: (i) 1R 2 v R0 2 O implies R - R0, and (ii) R - R0 implies Inv(R) - Inv(R0). We write R1 h R2 if R1 - R2 and R2 - R1, and R1 R2 if R1 - R2 and not R2 - R1.
De nition 2. Let O be an ontology and - and admissible preorder for O. We say that RIA v R0 is strati ed w.r.t. O and -, if for every R h R0 such that = 1R 2, there exist R1 and R2 such that 1R vO R1, R1 2 vO R0, R 2 vO R2, and 1R2 vO R0. We say that O is strati ed w.r.t - if every RIA v R such that vO R is strati ed w.r.t. O and -. We often omit \w.r.t. O" and \w.r.t. -" if O and - are clear from the context.
De nition 3. We say that a RIA 1R 2 v R0 is an overlap of two RIAs 1R1 v R10 and R2 2 v R20 (w.r.t. O) if either (i) R = R1, R10 vO R2, and R20 = R0, or (ii) R = R2, R20 vO R1, and R10 = R0. In cases (i) and (ii) we also say that the RIAs 1R1 v R10 and R2 2 v R20 overlap (w.r.t O).
In the next lemma recall that O is the extension of O with RIAs Inv( ) v Inv(R) such that v R 2 O.
Lemma 2. Let O be an ontology and - an admissible preorder for O. Then O is strati ed w.r.t. - if and only if: 1. Every RIA in O (and hence in O) is strati ed w.r.t. O and -; 2. Every overlap of two RIAs in O is strati ed w.r.t O and -.
Proof. The \only if" direction of the lemma follows immediately from the de nition of a strati ed ontology.
For proving the \if" direction of the lemma, without loss of generality we may assume that whenever 1R 2 v R0 2 O with R h R0, then either 1 or 2 is empty. Indeed, by Condition 1 of the lemma, there exist R1 such that 1R vO R1 and R1 2 vO R0. Hence by removing 1R 2 v R0 from O we preserve the relation vO and the conditions of the lemma.
We prove that 0 vO R00 implies that 0 v R00 is strati ed w.r.t. O and -. The proof is by two-fold induction: the outermost induction is over the length of 0, the innermost induction is over the proof of 0 vO R00 according to the de nition of vO. Pick an arbitrary R in 0 such that R h R00. The following cases match all possible ways of deriving 0 vO R00 using the de nition of vO: { 0 = R00 = R. In this case R00 v R00 is trivially strati ed. { 0 = 01 1 02R 03 such that 1 vO R1 and 01R1 02R 03 v R00 2 O.
In this case, by Condition 1 of the lemma, 01R1 02R 03 v R00 is strati ed. Thus, there exist R10 and R20 such that 01R1 02R vO R10, R10 03 vO R00, R 03 vO R20, and 01R1 02R20 vO R00. Since 1 vO R1, we have found R10 and R20 such that 01 1 02R vO R10, R10 03 vO R00, R 03 vO R20, and 01 1 02R20 v R00. { 0 = 01R 02 2 03 such that 2 vO R2 and 01R 02R2 03 vO R00. This case is analogous to the previous case. { 0 = 01 1R 2 such that 1R 2 vO R0, 01R0 v R00 2 O, and 1 is not empty.
Since 1R 2 vO R0 is a subproof of 0 v R00, by the induction hypothesis, 1R 2 v R0 is strati ed. Since R h R0 h R00, there exist R1 and R2 such that 1R vO R1, R1 2 vO R0, R 2 vO R2, and 1R2 vO R0. In particular, since R1 2 vO R0 and 01R0 v R00 2 O, we have 01R1 2 vO R00. Since 1 is not empty, 01R1 2 is shorter than 0 = 01 1R 2. Hence, by the induction hypothesis, 01R1 2 v R00 is strati ed. Since R h R10 h R00, there exists R10 such that 01R1 vO R10 and R10 2 vO R00. Thus, we have found R10 and R2 such that 01 1R vO R10, R 2 vO R2, R10 2 vO R00, and 01 1R2 vO R00. { 0 = 1R 2 02 such that 1R 2 vO R0, R0 02 v R00 2 O, and 02 is not empty.
This case is analogous to the previous case. { 0 = 01R 2 02 such that R 2 vO R2, R2 02 v R20 2 O, 02 is not empty, R20 vO R0, and 01R0 v R00 2 O.
In this case RIAs 01R2 02 v R00 is an overlap of two RIAs R2 02 v R20 and 01R0 v R00 in O. Hence, by Condition 2 of the lemma, 01R2 02 v R00 is strati ed. Since R h R2 h R00, there exists R1 such that 01R2 vO R1 and R1 02 vO R00. In particular, since R 2 vO R2 and 01R2 vO R1, we have 01R 2 vO R1. Since 02 is not empty, 01R 2 is shorter than 0 = 01R 2 02. Hence, by the induction hypothesis, 01R 2 vO R1 is strati ed. Since R h R1 h R00, there exists R10 such that 01R vO R10 and R10 2 vO R1. Thus we have found R10 and R0 such that 01R vO R10, R10 2 02 vO R00, R 2 02 vO R0, and 01R0 vO R00. { 0 = 01 1R 02 such that 1R vO R1, 01R1 v R10 2 O, 01 is not empty,
R10 vO R0, and R0 02 v R00 2 O. This case is analogous to the previous case. { 0 = 01R or 0 = R 02. This case is trivial. tu Lemma 3. Given an ontology O it is possible to decide in polynomial time in the size of O whether O is strati ed.
Proof. By Lemma 2, it is su cient to show that every RIA in O is strati ed and every overlap of two RIAs is strati ed. Hence there are only polynomially many RIAs to test. In order to test whether 1R 2 v R0 is strati ed for R, we enumerate all possible roles R10 and R20 and check whether 1R vO R10, R10 2 v R0, R 2 vO R20, and 1R20 vO R0. By Lemma 1, each of these conditions can be checked in polynomial time. tu
Now, as we have an algorithm for deciding whether an ontology is strati ed, it is easy to see that every ontology that satis es the original -regularity conditions for RIAs, is automatically strati ed for the ordering - de ned by R1 - R2 if either R1 = R2, or R1 = Inv(R2), or R1 R2. Indeed, the only overlap between -regular RIAs can occur between axioms 1R1 v R1 of type (v) and axioms R2 2 v R2 of type (iv) when R1 = R2 or R1 = Inv(R2), which can easily be shown to be strati ed since R1 vO R2 and R2 vO R1 in these cases.
Our next goal is to show that the set of RIAs in strati ed ontologies is always regular. Fix an ontology O and an admissible preorder - for O such that O is strati ed w.r.t. O. De ne the level of a role R w.r.t. - as follows: { If there is no R0 such that R0 R, then the level of R is 0; { Otherwise the level of R is the maximum over the levels of R0 R plus 1.
The level of a RIA v R is the level of R. We write O R0 if R O R0 for every R in . As in the proof of Lemma 2, without loss of generality, we can assume that for every RIA 1R 2 v R0 2 O with R h R0, either 1 or 2 is empty. Hence there are four types of RIAs in O possible: { Type 0: v R0, where R0; { Type 1: R1 v R0, where R1 h R0 and { Type 2: R2 v R0, where R2 h R0.
R0; Note that RIAs of the form R v R0 with R h R0 are of both Types 1 and 2.
One nice property of strati ed ontologies is that for proving vO R one can apply the RIAs in O in some particular order, namely: (i) apply RIAs in the non-decreasing order of their levels, (ii) for the same level, apply the RIAs in the non-decreasing order of their types. To formalize this strategy, we introduce a notion of strati ed proof : De nition 4. Given an ontology O, we de ne the relat0ioanss fvolinlo;Ow,s:0 n 0 between role chains and roles by induction on n i 2, 1. If v R0 2 O has Type 0 and level n, then v0n;O R0;
i 2. If role R has level n, then R vn;O R, i = 1; 2;
1 1 3. If 1 vn;O R1 and R1 v R0 2 O has Type 1 and level n, then 1 vn;O R0; 4. If 2 v2n;O R2 and R2 v R0 2 O has Type 2 and level n, then 2 vj2n;O R0; 5. If vin;O R and 1R 2 vjm;O R0 with (n; i) <lex (m; j) then 1 2 vm;O R0; where (n; i) <lex (m; j) if either n < m, or n = m and i < j. We say that a RIA v R0 has a strati ed proof in O if vin;O R0, for some n and i (0 i 2). Lemma 4. For every strati ed ontology O, if 0 vO R00 then 0 v R00 has a strati ed proof in O.
Proof (Sketch). We repeatedly apply the following transformation to the proof of 0 vO R00, which tries to swap the RIAs in O applied in the wrong order:
For every overlap 1R 2 v R0 of RIAs 1R v R1 and R2 2 v R0 of Types 2 and 1 in the proof of 0 vO R00, where R1 vO R2, and 1 and 2 are non-empty, we take R20 such that R1 2 vO R20 and 1R20 vO R0, which exists since O is strati ed, and replace the sub-proof of 1R 2 v R0 in 0 vO R00 with the proof using R1 2 vO R20 and 1R20 vO R0;
This transformation always terminates. Indeed, after each transformation step, either the number of axioms R1 Rn v R0 with n 2 used in the proof increases (when the proof of the overlap is replaced with a longer proof), or, otherwise, the number of such axioms remains the same, but the number of pairs ( 1R v R1; R2 2 v R0) of RIAs respectively of Types 2 and 1 such that 1 and 2 are non-empty and 1R v R1 is used in the proof before R2 2 v R0, decreases.
After the transformation terminates, it is easy to see that the proof becomes strati ed. tu Theorem 1. For every strati ed ontology O and role R one can construct an automaton for LO(R) which is at most exponential in the level of R in O. Proof (Sketch). By Lemma 4 for every 2 LO(R), the RIA v R has a strati ed proof. It is easy to show that the language generated by RIAs of the same level n and the same type is regular. This is a consequence of the fact that the RIAs of Types 1 and 2 of the same level correspond to left-linear and right-linear grammars respectively, which generate regular languages. The RIAs v R0 of Type 0 correspond to nite languages since the level of the roles in is smaller than the level of R0, and therefore, only one step rewritings are possible. Now the fact that LO(R) generated by RIAs of all levels is regular, follows from the fact that regular languages are closed under substitution. The size of the automaton for every level is at most polynomial in the size of O; thus the size of the automaton for LO(R) is at most exponential in the level of R. tu
Returning to Example 1, we can show that the set of RIAs (
On the other hand, RIAs (
The problem with (22) is more involved, since isChildOf isChildOf vO R does
not seem to hold for any role R introduced so far. Intuitively, by going to a child
and then going back to a parent, we should come to the \partner"|an individual
who has the same children as the initial individual. Hence we can introduce a
fresh role isPartnerOf, and add properties similar to those of isSiblingOf:
isChildOf isChildOf v isPartnerOf
isPartnerOf isPartnerOf v isPartnerOf
isChildOf isPartnerOf v isChildOf
isPartnerOf
v isPartnerOf
(24)
(25)
(26)
(27)
(28)
(29)
It is now possible to show that RIAs (
It is a natural question, whether any set of RIAs that induce regular languages, can be extended, as in the example above, to a set of RIAs that is strati ed. The following theorem gives a positive answer to this question.
Theorem 2. Let O be an ontology such that for every role R the language LO(R) is regular. Then there exists a conservative extension O0 of O which is strati ed for every preorder - that is admissible for O.
Proof. For every role R and a role chain we introduce a fresh role R . We use R as a synonym for R. For every R1, R2, 1, 2, and vO R we add axioms: R1R2 2 R21 v R11 2 v R Let O0 be the extension of O with the above axioms. It is easy to show that O0 is a conservative extension of O: for every model I of O one can interpret (R )I := Sf( 0)I j 0 vO Rg so that the axioms (28) and (29) are satis ed. Moreover, it can be shown that the resulting ontology is strati ed. First, the original RIAs follow from (28) and (29): if vO R for = R1R2 Rn, then R1 Rn v R1 Rn v R R1 Rn = RR1 Rn R1 Rn v RR2 Rn R2 Rn v v R . Hence by removing the original RIAs, the relation vO0 does not change. The remaining axioms of the form (28) and (29) are strati ed, since every overlap of axioms (28) R1R3 3 R3R2 2 R21 v R11 2 3 is provable by R1R3 3 R3R2 2 v R1R2 2 3 , R1R2 2 3 R21 v R11 2 3 , and by R3R2 2 R21 v R31 2 , R1R3 3 R31 2 v R11 2 3 .
The only problem with O0 is that it requires in nitely many axioms (28) and (29), since the number of new roles R is not bounded. To bound the number of roles, we use the regularity property for languages L (R). De ne L (R) := f 0 j 0 2 LO(R)g, and set R11 O R22 if and only if LOO1 (R1) = LO2 (OR2). By Myhill-Nerode theorem (see, e.g., [7]), since LO(R) is regular for each R, there are at most nitely many equivalence classes induced by O. Since O-equivalent roles have the same interpretations, we can identify those roles, and thus obtain only nitely many axioms of form (28) and (29).
In this paper we have introduced a notion of strati ed role inclusion axioms which provides a syntactically-checkable su cient condition for regularity of RIAs|a condition that ensures decidability of SROIQ. We have demonstrated that for every strati ed SROIQ ontology, one can construct a regular automaton representing the RIAs, which is worst case exponential in the size of the ontology. The result in [11] then implies that the complexity of reasoning with strati ed SROIQ ontologies remains the same as the complexity of original SROIQ, namely N2ExpTime-complete. Moreover, we have demonstrated that our conditions for regularity are in a sense maximal|every ontology O with regular RIAs can be conservatively extended to an ontology with strati ed RIAs.
Complex RIAs are closely related to interaction axioms in grammar modal logics i1 in X ! i1 in X [2, 12, 3]. Such axioms often cause undecidability, however in [12, 3] a decidable class called the regular grammar modal logics has been described. In [4] a decision procedure for this class is given by a translation into the two-variable guarded fragment. Because it is in general undecidable if the given interaction axioms are regular, the decision procedure assumes that a regular automaton for them is also provided. When applying these techniques to ontologies and complex RIAs, such a restriction poses a serious practical problem: the users are unlikely to provide such automata, and even if they do, it is in general not possible to verify if the automaton really corresponds to the given axioms. A solution to this problem, proposed in [13, 1], is to use a su cient syntactical condition for regularity called -regularity. Another su cient condition proposed in [14] requires associativity of RIAs, which means that if R1R2 v R10 and R10R3 v R0 then there exists R20 such that R2R3 v R20 and R1R20 v R0. It is easy to see that associativity is a partial case of our su cient conditions, when - is a total relation on roles. Note that Theorem 2 holds for any preorder -, and in particular, when - is total.
In this paper we have mainly addressed theoretical properties of ontologies with strati ed RIAs, and have argued that they can be used to model properties which otherwise are not possible to model within SROIQ. One problem that has not been addressed in this paper, is how to ensure that an ontology modeler produces strati ed RIAs in practice. We made a small experiment to check how many of complex RIAs in release 7 of Galen are strati ed. We found that the total of 385 complex role inclusions in Galen produce 3604 non-strati ed overlaps, for which additional axioms are required to x the problems. Clearly, the process of nding the missing axioms can be very time consuming. The conditions of strati ed overlaps in such cases could provide valuable hits for nding the missing axioms. Methods for nding strati ed axioms could be one of the topics for our future works.