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 first 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 R 1 • • • R n R. It is wellknown that unrestricted usage of such axioms can easily lead to undecidability for modal and description logics [2][3][4][5], with a notable exception of the DL EL ++ [6]. Therefore certain syntactic restrictions are imposed on RIAs in SROIQ to regain decidability. Specifically, the restrictions ensure that RIAs R 1 • • • R n R when viewed as production rules for context-free grammars R → R 1 . . . R n 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 finite 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 satisfied 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 defines 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. Our restrictions are conservative over the restrictions in SROIQ. That is, every set of RIAs that satisfies the restriction in SROIQ will automatically satisfy our restrictions. 2. Our restrictions can be verified 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. 1. The syntax and semantics of SROIQ 4. Finally, for any set of RIAs that induce a regular language, there exists a set of RIAs (containing possibly new roles) that satisfies 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.
In this section we introduce syntax and semantics of the DL SROIQ [1]. A SROIQ vocabulary consists of countably infinite sets N C of atomic concepts, N R of atomic roles, and
ρ 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 defined by Inv(R)
The syntax and semantics of SROIQ is summarised in Table 1. The set of SROIQ concepts is recursively defined using the constructors in the upper part of the table, where A ∈ N C , 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 irreflexive transitive binary relation ≺ on roles such that
It is assumed that all RIAs in O are regular for some order ≺.
Given an ontology O, let Ō be the extension of O with RIAs Inv(ρ) Inv(R) for every ρ R ∈ O. Let ρ O R be the smallest relation between role chains and roles such that: (i) R O R for every role R, and (ii)
Lemma 1. Given an ontology O, role chain ρ, and role R, it is possible to decide in polynomial time whether ρ O R.
Proof. We define a context-free grammar with terminal symbols s R and nonterminal symbols A R for every role R, and production rules A R → s R for every role R and
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 ρ O R. 1 are simple w.r.t. O. Other constructors and axioms of SROIQ such as disjunction, universal restriction, role (ir)reflexivity, and role (a)symetry can be expressed using the given ones.
The semantics of SROIQ is defined 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 ∈ N C a set A I ⊆ ∆ I , to every r ∈ N R a relation r I ∈ ∆ I × ∆ I , and to every a ∈ N I an element a I ∈ ∆ I . The interpretation is extended to roles by U I = ∆ I × ∆ I and (r − ) I = { x, y | y, x ∈ r I }, and to role chains by (R
where • is the composition of binary relations. The empty role chain is interpreted by
The interpretation of concepts is defined according to the right column of the upper part of Table 1, where δ(x, V ) for δ ⊆ ∆ I × ∆ I , V ⊆ ∆ I , and x ∈ ∆ I denotes the set {y | x, y ∈ δ ∧ y ∈ V }, and ||V || denotes the cardinality of a set V ⊆ ∆ I . An interpretation I satisfies an axiom α (written I |= α) if the respective condition to the right of the axiom in Table 1
Given an ontology O, for every role R, we define a language L O (R) consisting of role chains (viewed as finite words over roles) as follows:
We say that the set of RIAs of O is regular if the language L O (R) is regular for every role R. It has been shown in [1] that ≺-regularity for RIAs implies regularity. The converse of this property, however, does not always hold, as we demonstrate in the following example.
Example 1. Consider an ontology O consisting of the RIAs ( 2)-( 4) below:
RIAs ( 2)-( 4) express properties of parthood relations isPartOf and isProperPartOf: axiom (2) says that isProperPartOf is a sub-relation of isPartOf; axiom (3) says that isPartOf is transitive; finally, axiom (4) says that if x is a part of y which is a proper part of z, then x is a proper part of z. Since any role chain consisting of isPartOf and isProperPartOf can be rewritten to isPartOf by applying axioms ( 2) and ( 3), it is easy to see that:
Since isProperPartOf is implied only by axiom (4), it is easy to see that:
Thus, the languages L O (isPartOf) and L O (isProperPartOf) induced by RIAs (2)-( 4) are regular. However, there is no ordering ≺ for which axioms (2)-( 4) are ≺-regular. Indeed, by conditions (i)-(v) of ≺-regularity, it follows from (2) that isProperPartOf ≺ isPartOf, and from (4) that isPartOf ≺ isProperPartOf, which contradicts the fact that ≺ is a transitive irreflexive relation.
In fact, there is no SROIQ ontology O that could express properties (2)-(4) using ≺-regular RIAs. It is easy to show by induction over the definition of
This means that for every role R, the language L O (R) can contain only words over R, Inv(R), or R with R ≺ R. Clearly, this is not possible if L O (isPartOf) and L O (isProperPartOf) contain the languages defined in ( 5) and (6).
Axioms such as ( 2)-( 4) in Example 1 naturally appear in ontologies describing parthood relations, such as those between anatomical parts of the human body. For example, release 7 of the GRAIL version of the Galen ontology3 contains the following axioms that are analogous to (2)-( 4):
Complex RIAs such as ( 7)-( 9) are used in Galen to propagate properties over chains of various parthood relations. For example, the next axiom taken from Galen expresses that every instance of body structure contained in spinal canal is a structural component of nervous system:
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 finger is defined as part of a hand, then an injury to a finger should be classified as an injury to the hand, however, the amputation of a finger should not be classified 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 U S describing all parts of U including U itself, the entity class U E that is equivalent to U , and the part class U P describing the proper parts of U . Thus the axioms Finger E Finger S , Finger P Finger S , as well as Hand E Hand S , Hand P Hand S describe the relations between the classes within the triples, and one can use the axiom Finger S Hand P to express that finger 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 finger is a proper part of hand can be written in this setting directly as follows:
The explicit usage of parthood relation requires, however, complex RIAs such as (2)-(3), which do not satisfy ≺-regularity conditions of SROIQ. This would not be a problem for ontologies expressible within the tractable DL EL ++ [6] such as SNoMed CT,4 since EL ++ does not require regularity for RIAs. But it could be a problem when an expressivity beyond EL ++ is required, such as for translating the Galen ontology into OWL 2. In this paper we propose an extension of regularity conditions, which, in particular, can handle axioms such as ( 2)-(3).
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:
It can easily be shown that properties ( 12)-( 14) could not be expressed using ≺-regular RIAs since this would require that isChildOf ≺ isSiblingOf and isSiblingOf ≺ isChildOf. On the other hand, they induce regular languages:
In the next section, we demonstrate how our extended regularity conditions can capture such kind of axioms as well.
Definition 1. A preorder (a transitive reflexive relation) on roles is said to be admissible for an ontology O if:
Definition 2. Let O be an ontology and and admissible preorder for O. We say that RIA ρ R is stratified w.r.t. O and , if for every R R such that ρ = ρ 1 Rρ 2 , there exist R is an overlap of two RIAs Proof. The "only if" direction of the lemma follows immediately from the definition of a stratified ontology.
For proving the "if" direction of the lemma, without loss of generality we may assume that whenever ρ 1 Rρ 2 R ∈ O with R R , then either ρ 1 or ρ 2 is empty. Indeed, by Condition 1 of the lemma, there exist R 1 such that ρ 1 R O R 1 and R 1 ρ 2 O R . Hence by removing ρ 1 Rρ 2 R from O we preserve the relation O and the conditions of the lemma.
We prove that ρ O R implies that ρ R is stratified w.r.t. O and . The proof is by two-fold induction: the outermost induction is over the length of ρ , the innermost induction is over the proof of ρ O R according to the definition of O . Pick an arbitrary R in ρ such that R R . The following cases match all possible ways of deriving ρ O R using the definition of O :
In this case, by Condition 1 of the lemma,
and ρ 2 is not empty.
This case is analogous to the previous case.
Hence, by the induction hypothesis,
This case is analogous to the previous case.
ρ = ρ 1 R or ρ = Rρ 2 . This case is trivial. Lemma 3. Given an ontology O it is possible to decide in polynomial time in the size of O whether O is stratified.
Proof. By Lemma 2, it is sufficient to show that every RIA in O is stratified and every overlap of two RIAs is stratified. Hence there are only polynomially many RIAs to test. In order to test whether ρ 1 Rρ 2 R is stratified for R, we enumerate all possible roles R 1 and R 2 and check whether
and ρ 1 R 2 O R . By Lemma 1, each of these conditions can be checked in polynomial time. Now, as we have an algorithm for deciding whether an ontology is stratified, it is easy to see that every ontology that satisfies the original ≺-regularity conditions for RIAs, is automatically stratified for the ordering defined by
Indeed, the only overlap between ≺-regular RIAs can occur between axioms
, which can easily be shown to be stratified since R 1 O R 2 and R 2 O R 1 in these cases.
Our next goal is to show that the set of RIAs in stratified ontologies is always regular. Fix an ontology O and an admissible preorder for O such that O is stratified w.r.t. O. Define the level of a role R w.r.t. as follows:
As in the proof of Lemma 2, without loss of generality, we can assume that for every RIA ρ 1 Rρ 2 R ∈ O with R R , either ρ 1 or ρ 2 is empty. Hence there are four types of RIAs in Ō possible:
Note that RIAs of the form R R with R R are of both Types 1 and 2. One nice property of stratified ontologies is that for proving ρ O R one can apply the RIAs in Ō 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 stratified proof : Definition 4. Given an ontology O, we define the relations i n,O , 0 ≤ i ≤ 2, n ≥ 0 between role chains and roles by induction on n ≥ 0 as follows:
where (n, i) < lex (m, j) if either n < m, or n = m and i < j. We say that a RIA ρ R has a stratified proof in O if ρ i n,O R , for some n and i (0
Proof (Sketch). We repeatedly apply the following transformation to the proof of ρ O R , which tries to swap the RIAs in Ō applied in the wrong order:
For every overlap ρ 1 Rρ 2 R of RIAs ρ 1 R R 1 and R 2 ρ 2 R of Types 2 and 1 in the proof of ρ O R , where R 1 O R 2 , and ρ 1 and ρ 2 are non-empty, we take R 2 such that R 1 ρ 2 O R 2 and ρ 1 R 2 O R , which exists since O is stratified, and replace the sub-proof of
This transformation always terminates. Indeed, after each transformation step, either the number of axioms R 1 • • • R n R 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 (ρ 1 R R 1 , R 2 ρ 2 R ) of RIAs respectively of Types 2 and 1 such that ρ 1 and ρ 2 are non-empty and ρ 1 R R 1 is used in the proof before R 2 ρ 2 R , decreases.
After the transformation terminates, it is easy to see that the proof becomes stratified.
Theorem 1. For every stratified ontology O and role R one can construct an automaton for L O (R) which is at most exponential in the level of R in O.
Proof (Sketch). By Lemma 4 for every ρ ∈ L O (R), the RIA ρ R has a stratified 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 ρ R of Type 0 correspond to finite languages since the level of the roles in ρ is smaller than the level of R , and therefore, only one step rewritings are possible. Now the fact that L O (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 L O (R) is at most exponential in the level of R.
Returning to Example 1, we can show that the set of RIAs (2)-( 4) is stratified. Indeed, it can be shown that RIAs (3)-( 4) can result in the following overlaps:
All of the above RIAs can be stratified using ( 2)-( 4). On the other hand, RIAs ( 12)-( 14) are not stratified. Indeed there are the following overlaps between RIAs ( 12) and ( 13) and between RIAs ( 12) and ( 14):
The problem with (21) is that there is
Intuitively, this property should hold for R = isChildOf − , but RIAs ( 12)-( 14) are not sufficient to derive this property. Fortunately the problem can be fixed by declaring the role isSiblingOf to be symmetric: (14). Now (12) implies that (21) is stratified. The problem with ( 22) is more involved, since isChildOf − •isChildOf O 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:
It is now possible to show that RIAs ( 12)-( 14) and ( 23)-( 27) are stratified.
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 stratified. 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 L O (R) is regular. Then there exists a conservative extension O of O which is stratified for every preorder that is admissible for O.
In this paper we have introduced a notion of stratified role inclusion axioms which provides a syntactically-checkable sufficient condition for regularity of RIAs-a condition that ensures decidability of SROIQ. We have demonstrated that for every stratified 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 stratified 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 stratified RIAs.
Complex RIAs are closely related to interaction axioms in grammar modal 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 sufficient syntactical condition for regularity called ≺-regularity. Another sufficient condition proposed in [14] requires associativity of RIAs, which means that if R 1 R 2 R 1 and R 1 R 3 R then there exists R 2 such that R 2 R 3 R 2 and R 1 R 2 R . It is easy to see that associativity is a partial case of our sufficient 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 stratified 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 stratified RIAs in practice. We made a small experiment to check how many of complex RIAs in release 7 of Galen are stratified. We found that the total of 385 complex role inclusions in Galen produce 3604 non-stratified overlaps, for which additional axioms are required to fix the problems. Clearly, the process of finding the missing axioms can be very time consuming. The conditions of stratified overlaps in such cases could provide valuable hits for finding the missing axioms. Methods for finding stratified axioms could be one of the topics for our future works.
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 R 1 , R 2 , ρ 1 , ρ 2 , and ρ O R we add axioms:
Let O be the extension of O with the above axioms. It is easy to show that O is a conservative extension of O: for every model I of O one can interpret (R ρ ) I := {(ρ ) I | ρ ρ O R} so that the axioms (28) and (29) are satisfied. Moreover, it can be shown that the resulting ontology is stratified. First, the original RIAs follow from (28) and ( 29
Hence by removing the original RIAs, the relation O does not change. The remaining axioms of the form (28) and (29) are stratified, since every overlap of axioms ( 28
The only problem with O is that it requires infinitely 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
. By Myhill-Nerode theorem (see, e.g., [7]), since L O (R) is regular for each R, there are at most finitely many equivalence classes induced by ∼ O . Since ∼ O -equivalent roles have the same interpretations, we can identify those roles, and thus obtain only finitely many axioms of form (28) and (29).