Terminological Cycles in a Description Logic with Existential Restrictions

1 Introduction

Early description logic (DL) systems allowed the use of value restrictions 0/r.C), but not of existential restrictions (3r.C). Thus, one could express that all children are male using the value restriction Vchild.Male, but not that someone has a son using the existential restriction 3child.Male. The main rea­ son was that when clarifying the logical status of property arcs in sema~tic networks and slots in frames, the decision was taken that arcs/slots should be read as value restrictions (see, e.g., [Nebel, 1990]). Once one con~ider~ more ~xp_res­ sive DLs allowing for full negation, existential restnctlons come in as the dual of value restrictions [Schrnidt-Schau13 and Smolka, 1991]. Thus, for historical reasons, DLs that allow for existential, but not for value restrictions, are largely unexplored. In the present paper, we investigate termino­ logical cycles in the DL £ C, which allows for conjunction, existential restrictions, and the top-concept. In contrast to (even very inexpressive) DLs with value restrictions, sub­ sumption in ££ remains polynomial in the presence of t~r­ minological cycles. It should be noted that there are m­ deed applications where the small DL ££appears to be suffi­ cient. In fact, SNOMED, the Systematized Nomenclature of Medicine [Cote eta!., 1993] employs££ [Spackman, 2001; Spackman eta!., 1997]. Even though SNOMED does not appear to use cyclic definitions, this may be due to a lack of technology rather than need. In fact, the Galen medical knowledge base contains many cyclic dependencies [Rector and Horrocks, 1997]. Also, even in the case of acyclic ter­ minologies, our polynomial subsumption algorithm improves on the usual approach that first unfolds the TBox (a poten­ tially exponential step) and then applies the polynomial sub­ sumption algorithm for ££-concept descriptions [Baader et a!., 1999].

*Partially supported by the DFG under grant BA 1122/4-3.

The first thorough investigation of cyclic terminologies in description logics (DL) is due to Nebel [1991], who intro­ duced three different semantics for such terminologies: least fix point (lfp) semantics, which considers only th~ models that interpret the defined concepts as small as possible; greatest fix point (gfp) semantics, which considers only th~ models that interpret the defined concepts as large as possible; and descriptive semantics, which considers all models.

In [Baader, 1990; 1996], subsumption w.r.t. cyclic termi­ nologies in the small DL F £ 0 , which allows for conjunction and value restrictions only, was characterized with the help of finite automata. This characterization provided PSPACE de­ cision procedures for subsumption in F Co with cyclic termi­ nologies for the three types of semantics introduced by Nebel. In addition, it was shown that subsumption is PSPACE-hard. The results for cyclic F £ 0-terminologies were extended by Kiisters [ 1998] to ACN, which extends F Co by atomic nega­ tion and number restrictions.

The fact that the DL ACC (which extends :F Co by full negation) is a syntactic variant of the multi-modal logic K opens a way for treating cyclic terminolo~ies and more g~n­ eral recursive definitions in more expressive languages hke ACC and extensions thereof by a reduction to the modal mu­ calculus [Schild, 1994; De Giacomo and Lenzerini, 1994]. In this setting, one can use a mix of the three types of semantics introduced by Nebel. However, the complexity of the sub­ sumption problem is EXPTIME-complete.

In spite of these very general results for cyclic definitions in expressive languages, there are still good reasons to look at cyclic terminologies in less expressive (in particular sub­ Boolean) description logics. One reason is, of course, that one can hope for a lower complexity of the subsumption prob­ lem. For DLs with value restrictions, this hope is not fulfilled, though. Even in the inexpressive DL F Co, sub_sumpti?~ be­ comes PSPACE-complete if one allows for cychc defimtwns. This is still better than the EXPTIME-completeness that one has in A.CC with cyclic definitions, but from the practical point of view it still means that the subsumption algorithm may need exponential time.

In contrast, the subsumption problem in££ can be decided in polynomial time w.r.t. the three types of semantics intro­ duced by Nebel. The main tool used to show these results is a characterization of subsumption through the existence of so-called simulation relations.

In the next section we will introduce the DL ££ as well as cyclic terminologies and the three types of semantics for these terminologies. Then we will show in Section 3 how such terminologies can be translated into description graphs. In this section, we will also define the notion of a simulation between nodes of a description graph, and mention some use­ ful properties of simulations. The next three sections are then devoted to the characterization of subsumption in ££ w.r.t. gfp, lfp, and descriptive semantics, respectively.

2 Cyclic terminologies in the DL £ .C

Concept descriptions are inductively defined with the help of a set of constructors, starting with a set Nc of concept names and a set N R of role names. The constructors determine the expressive power of the DL. We restrict the attention to the DL ££,whose concept descriptions are formed using the con­ structors top-concept (T), conjunction (C n D), and existen­ t!al re~triction (3.r.C). The semantics of ££-concept descrJR­ twns IS defined m terms of an interpretation I = ( ll I, · ) . The domain ll I of I is a non-empty set of individuals and the interpretation function .I maps each concept name A E Nc to a subset AI of fli and each role r E NR to a binary re­ lation ri on fli. The extension of .I to arbitrary concept descriptions is inductively defined, as shown in the third col­ umn of Table 1.

A terminology (or TBox for short) is a finite set of con­ cept definitions of the form A = D, where A is a concept name and D a concept description. In addition, we require that TBoxes do not contain multiple definitions, i.e., there cannot be two distinct concept descriptions D1 and D2 such that both A = D1 and A = D2 belongs to the TBox. Con­ cept names occurring on the left-hand side of a definition are called defined concepts. All other concept names occurring in the TBox are called primitive concepts. Note that we al­ low for cyclic dependencies between the defined concepts, i.e., the definition of A may refer (directly or indirectly) to A itself. An interpretation I is a model of the TBox T iff it satisfies all its concept definitions, i.e., AI = DI for all definitions A = D in T.

The semantics of (possibly cyclic) ££-TBoxes we have just defined is called descriptive semantic by Nebel [ 1991].

For some applications, it is more appropriate to interpret cyclic concept definitions with the help of an appropriate fix­ point semantics. Before defining least and greatest fixpoint semantics formally, let us illustrate their effect on an exam­ ple.

Example 1 Assume that our interpretations are graphs where we have nodes (elements of the concept name Node) and edges (represented by the role edge), and we want to define the concept I node of all nodes lying on an infinite (possibly cyclic) path of the graph. The following is a possible defini­ tion of I node: I node =: Node n 3edge.lnode.

Now consider the following interpretation of the primitive concepts and roles:

Where M := {mo,ml,m2, ... } and N := {no}, there are four possible ways of extending this interpretation of the primitive concepts and roles to a model of the TBox consist­ ing of the above concept definition: I node can be interpreted by M UN, M, N, or 0. All these models are admissible w.r.t. descriptive semantics, whereas the first is the gfp-model and the last is the lfp-model of the TBox. Obviously, only the gfp-model captures the intuition underlying the definition (namely, nodes lying on an infinite path) correctly.

It should be noted, however, that in other cases descrip­ tive semantics appears to be more appropriate. For example, consider the definitions

With respect to gfp-semantics, the defined concepts Tiger and Lion must always be interpreted as the same set whereas this is not the case for descriptive semantics. 1

Before we can define lfp- and gfp-semantics formally, we must introduce some notation. Let T be an ££-TBox con­ taining the roles Nrote, the primitive concepts Nprim, and the defined concepts Ndef := { A1 , ... , Ak}. A primitive inter­ pretations :J for T is given by a domain fl.:T, an interpreta­ tion of the roles r E Nrote by binary relations r.:T on fl.:T, and an interpretation of the primitive concepts P E Nprim by subsets p.:T of fl.:T. Obviously, a primitive interpretation differs from an interpretation in that it does not interpret the defined concepts in Ndef. We say that the interpretation I is based on the primitive interpretation :J iff it has the same domain as :J and coincides with :Jon Nrote and Nprim· For a fixed primitive interpretation :J, the interpretations I based on i.t are uniq~ely determined by the tuple (Af, .. . , A{) of the mterpretatwns of the defined concepts in Ndef. We define

Interpretations based on :J can be compared by the following ordering, which realizes a pairwise inclusion test between the respective interpretations of the defined concepts: if 1"1, 1"2 E lnt(:T), then

1 This example is similar to the "humans and horses" example used by Nebel [ 1991] to illustrate the difference between descriptive semantics and gfp-semantics in A£N.

It is easy to see that -j.:J induces a complete lattice on lnt(:T), i.e., every subset of Int(:T) has a least upper bound (lub) and a greatest lower bound (glb ). Using Tarski 's fixpoint theorem [Tarski, 1955] for complete lattices, it is not hard to show [Nebel, 1991] that, for a given primitive interpretation :T, there is always a greatest and a least (w.r.t. -j.:J) model of T based on :T. We call these models respectively the greatest fixpoint model (gfp-model) and the least fixpoint model (lfp­ model) of T Greatest (least) fixpoint semantics considers only gfp-models (lfp-models) as admissible models.

Definition 2 LetT be an£ .C-TBox and A, B be defined con­ cepts2 occurring in /. Then,

• A is subsumed by B w.r.t. descriptive semantics (A ~T B) iff AI ~ BI holds for all models I ofT
• A is subsumed by B w.r.t. gfp-semantics (A ~gfp,T B) iff AI ~ BI holds for all gfp-models.I ofT
• A is subsumed by B w.r.t. lfp-semantics (A ~lfp,T B) iff AI ~ BI holds for alllfp-models.I ofT

We will show in the following that all three subsumption problems are decidable in polynomial time. To do this, we represent £ .C-TBoxes as graphs.

3 Description graphs and simulations

£.C-TBoxes as well as primitive interpretations can be rep­ resented as description graphs. Before we can translate £ .C­ TBoxes into description graphs, we must normalize them. In the following, let T be an £ .C-TBox, Ndef the defined con­ cepts ofT, Nprim the primitive concepts ofT, and Nrole the roles ofT

We say that the £ .C-TBox T is normalized iff A = D E T implies that D is of the form

form, e 2: 0, p1, . . . , Pm E Nprim. T1, ... , Tf E Nrole. and B1, ... ,Bt E Ndef· Ifm = e = 0, thenD = T.

Since there is a polynomial translation of general TBoxes into normalized ones [Baader, 2002], one can restrict the at­ tention to normalized TBoxes. Thus, we will assume that all TBoxes are normalized. Normalized £ .C-TBoxes can be viewed as graphs whose nodes are the defined concepts, which are labeled by sets of primitive concepts, and whose edges are given by the existential restrictions. For the rest of this section, we fix a normalized £.C-TBox T with primitive concepts Nprim, defined concepts Ndef · and roles Nrole·

Definition 3 An ££-description graph is a graph 9 = (V, E, L) where

• V is a set of nodes;

2 0bviously, we can restrict the attention to subsumption between defined concepts since subsumption between arbitrary concept de­ scriptions can be reduced to this problem by introducing definitions for the descriptions.

• E ~ V x Nrole x V is a set of edges labeled by role names;
• L: V -+ 2Nprim is a function that labels nodes with sets of primitive concepts.

The normalized TBox T can be translated into the follow­ ing ££-description graph 9T = (Ndef, ET, LT):

• the nodes of 9T are the defined concepts ofT;
• if A is a defined concept and

its definition in T, then

• A is the source of the edges (A,rl,Bl), .. . ,(A,rt,Bt) E E7.

Any primitive interpretation :T = ( ~ .:1, . .:1) can be trans­ lated into the following ££-description graph 9.:1 = (~.:1, E.:1, L.:1 ):

• the nodes of 9.:1 are the elements of~ .:1;
• E.:1 := {(x,r,y) I (x,y) E r.:l};
• L.:J(x) := {P E Nprim I x E p.:J} forallx E ~.:J.

The translation between £ .C-TBoxes (primitive interpreta­ tions) and ££-description graphs works in both directions, i.e., any ££-description graph can also be view as an £.C­ TBox (primitive interpretation).

Simulations are binary relations between nodes of two ££­ description graphs that respect labels and edges in the sense defined below.

Definition 4 Let 9i = (Vi, Ei, Li) (i = 1, 2) be two ££­ description graphs. The binary relation z ~ v1 X v2 is a simulation from 91 to 92 iff

• (Sl) (v1,v2) E ZimpliesL1(vl) ~ L2(v2);and
• (S2) if ( v1, v2) E Z and ( V1, r, vU E E1. then there exists a node v~ E V2 such that (vLv~) E Z and (v2,r,v~) E E2.

We write Z: 91 ;:;:: 92 to express that Z is a simulation from 91 to 92.

It is easy to see that the set of all simulations from 91 to 92 is closed under arbitrary unions. Consequently, there always exists a greatest simulation from 91 to 92. If 91, 92 are finite, then this greatest simulation can be computed in polynomial time [Henzinger eta!., 1995]. The following proposition is an easy consequence of this fact (see [Baader, 2002]).

Proposition 5 Let 91, 92 be two finite ££-description graphs, v1 a node of 91 and v2 a node of 92. Then we can decide in polynomial time whether there is a simulation Z: 91;:;:: 92 such that (v1,v2) E Z .

4 Subsumption w.r.t. gfp-semantics

In the following, letT be a normalized£ .C-TBox with primi­ tive concepts Nprim, defined concepts Ndef, and roles Nrole · Before characterizing subsumption w.r.t. gfp-semantics, we give a characterization of when an individual of a gfp-model belongs to a defined concept in this model.

Proposition 6 Let :1 be a primitive interpretation and I the gfp-model ofT based on :1. Then the following are equiva­ lent for any A E Ndef and x E 6. :J:

2. ThereisasimulationZ:QT ~ 9:Jsuchthat(A,x) E Z .

This proposition (whose proof can be found in [Baader, 2002]), can now be used to prove the following characteriza­ tion of subsumption w.r.t. gfp-semantics in t: C.

Theorem 7 LetT be an£ C-TBox and A, B defined concepts in T Then the following are equivalent:

1. A r;;;_gfp,T B .
2. There is a simulation Z: 9T ~ 9T with (B, A) E Z .

Proof (2::} 1) Assume that the simulation Z: 9T ~ 9T sat­ isfies (B, A) E Z . Let :1 be a primitive interpretation and I the gfp-model of/ based on :1. We must show that x E AI implies x E BI.

By Proposition 6, x E AI implies that there is a simulation Y : 9T ~ 9:J such that (A, x) E Y. It is easy to show that the composition X := Z o Y is a simulation from 9T to g:J such that ( B, x) E X. By Proposition 6, this implies x E BI.

(1::} 2) Assume that A r;;;_gfp,T B. We consider the graph 9T, and view it as an ££-description graph of a primitive interpretation. Thus, let :1 be the primitive interpretation with 9T = Q :1, and let I be the gfp-model ofT based on :1.

Since the identity is a simulation !d: 9T ~ 9T = Q:J that satisfies (A, A) E !d, Proposition 6 yields A E AI. But then A r;;;_gfp,T B implies A E BI, and thus Proposition 6 yields the existence of a simulation Z: 9T ~ Q :1 = 9T such that (B,A) E Z. D

The theorem together with Proposition 5 shows that sub­ sumption w.r.t. gfp-semantics in t:C is tractable.

Corollary 8 Subsumption w.r.t. gfp-semantics in t:C can be decided in polynomial time.

Example 9 Consider the TBox T consisting of the following concept definitions:

The t: £-description graph 9T corresponding to this TBox can be found in Figure 1. Let VT = {A, A', B , C, D} denote the set of nodes of this graph. Then Z := VT x VT is a simulation from 9T to 9T. Consequently, all the defined concepts in T subsume each other w.r.t. gfp-semantics.

5 Subsumption w.r.t. lfp-semantics

For the sake of completeness, we also treat lfp-semantics. It should be noted, however, that the results of this section demonstrate that lfp-semantics is not interesting in t:C.

Let T be an £ C-TBox and QT the corresponding ££­ description graph. Where A, B are nodes of 9T, we write A ~T B to denote that there is a path in 9T from A to B, and A .itT B to denote that there is a non-empty path in 9T from A to B. We define the set CycT as

{A I there exists a node B such that A ~T B .itT B}, i.e., CycT consists of the nodes in 9T that can reach a cyclic path in 9T· The following proposition is an easy consequence of the definition of lfp-semantics and of CycT (see [Baader, 2002]).

Proposition 10 LetT be an t:C-TBox and A a defined con­ cept in T If A E CycT, then A is unsatisfiable w.r.t. @­ semantics, i.e., AI= 0 holds for allljjJ-models I ofT

In Example 9, all the defined concepts belong to CycT, and thus they are all unsatisfiable w.r.t. lfp-semantics.

Since all the defined concepts in CycT are unsatisfiable, their definitions can be removed from the TBox without chan~ing th~ J?eaning of the concepts not belonging to CycT. (The1r defimt10n cannot refer to an element of CycT.) This leaves us with an acyclic terminology, on which gfp- and lfp­ semantics coincide [Nebel, 1991]. Thus, subsumption w.r.t. lfp-semantics in££ can be reduced to subsumption w.r.t. gfp­ semantics.

Corollary 11 Subsumption w.r.t. lfp-semantics in££ can be decided in polynomial time.

6 Subsumption w.r.t. descriptive semantics

Let T be an t: £-TBox and 9T the corresponding t: £­ description graph. Since every gfp-model of T is a model ofT, A r;;;_T B implies A r;;;_gfp,T B. Consequently, A r;;;_T B implies that there is a simulation Z : 9T ~ 9T with (B, A) E Z. In the following we will show what additional properties the simulation Z must satisfy for the implication in the other direction to hold.

To get an intuition on the difference between gfp- and de­ scriptive semantics, let us consider Example 9. With respect to gfp-semantics, all the defined concepts of/ are equivalent (i.e., subsume each other). With respect to descriptive seman­ tics, A, B, D are still equivalent, C is equivalent to A', but A' is not equivalent to B, and C and D are also not equivalent (in both cases, the concepts are not even comparable w.r.t. subsumption).

To see that C and A' are equivalent w.r.t. descriptive se­ mantics, it is enough to note that the following identities hold in every model I ofT: A'I = (3r.D)I = cr. A similar argument shows that B and D are equivalent. In addition, equivalence of C and A' also implies equivalence of A and B. The following model ofT is a counterexample to the other subsumption relationships:

Figure 2: A (E, A)-simulation chain.

We will see below that the reason for A' and E not being equivalent is that in the infinite path in 9r starting with A', one reaches D with an odd number of edges, whereas e is reached with an even number; for the path starting with B, it is just the opposite. In contrast, the infinite paths starting respectively with A and E "synchronize" after a finite number of steps. To formalize this intuition, we must introduce some notation.

Definition 12 The pathp1: E =Eo~ E1 ~ E2 ~ E3 ~ · · · in 9r is Z-simulated by the path P2: A = Ao ~ A1 ~ A2 ~ A3 ~ · · · in 9r iff (Ei, Ai) E Z for all i 2:: 0. In this case we say that the pair (p1, p2) is a (E, A)-simulation chain w.r.t. Z (see Figure 2).

Consider the TBox T and the simulation Z introduced in Example 9. Then

A -!+ A' -!+ D -!+ e -!+ is a (E, A)-simulation chain w.r.t. Z, and E -!+ Z.j. A' -!+ e -!+ Z.j. D -!+ D -!+ Z.j. e -!+ e -!+ Z.j. D -!+ D -!+ D -!+ Z.j. e -!+

is a (E, A')-simulation chain w.r.t. Z. Note that the first chain synchronizes after a finite number of steps in the sense that there is a Z-link between the same defined concept. In con­ trast, the second chain does not synchronize in this sense.

If (E, A) E Z, then (S2) of Definition 4 implies that, for every infinite path p1 starting with Eo := E, there is an infi­ nite path P2 starting with A0 : = A such that p1 is Z -simulated by p2. In the following we construct such a simulating path step by step. The main point is, however, that the decision which concept An to take in step n should depend only on the partial (E, A)-simulation chain already constructed, and not on the parts of the path p1 not yet considered.

Definition 13 A partial (E, A)-simulation chain is of the form depicted in Figure 3. A selection function S for A, E and Z assigns to each partial (E, A)-simulation chain of this form a defined concept An such that (An-1, Tn, An) is an edge in 9r and (En, An) E Z.

Given a path E = Eo ~ E1 ~ E2 ~ E3 ~ · · · and a defined concept A such that ( E, A) E Z, one can use a selec­ tion function S for A, E and Z to construct a Z -simulating path. In this case we say that the resulting (E, A)-simulation chain is S -selected.

Figure 3: A partial (E, A)-simulation chain.

Definition 14 The simulation Z: 9r ~ 9r is called (E, A)­ synchronized iff there exists a selection function S for A, E and Z such that the following holds: for every infinite S­ selected (E, A)-simulation chain of the form depicted in Fig­ ure 2 there exists an i 2:: 0 such that Ai = Ei.

We are now ready to state our characterization of subsump­ tion w.r.t. descriptive semantics (see [Baader, 2002] for the proof).

Theorem 15 LetT be an £.C-TBox, and A, E defined con­ cepts in T Then the following are equivalent:

1. A!;;;yE.
2. There is a (E, A)-synchronized simulation Z: 9r ~ 9r such that (B, A) E Z.

It remains to be shown that property (2) of the theorem can be decided in polynomial time. To this purpose, we construct a simulation Y such that (2) of Theorem 15 is equivalent to (E, A) E Y (see [Baader, 2002] for the proof that this is indeed the case):

We define Y := Un>O Yn, where the relations Yn are defined by induction on n: Y0 is the identity on the nodes of 9r. If Yn is already defined, then

Yn+l :=YnU{(e,e') I (e,e')satisfies(1),(2),(3)below}.

1. Lr(e) ~ Lr(e'),
2. (e, r1, el), ... , (e, re, ee) are all the edges in 9r with source e,
3. there are edges (e', r1, en, ... , (e', re, q) in 9r such that (e1, en E Yn, ... , (ee, q) E Yn.

The relation Y can obviously be computed in time polyno­ mial in the size of Qy. By using the techniques employed to decided Hom-SAT in linear time [Dowling and Gallier, 1984], it is not hard to show that Y can actually be computed in time quadratic in the size of 9r.

Corollary 16 Subsumption w. r. t. descriptive semantics in £ .C can be decided in polynomial time.

An alternative way for showing the polynomiality result would be to reduce the existence of a (E, A)-synchronized simulation Z satisfying (E, A) E Z to the strategy problem for a certain two-player game with a positional winning con­ dition. The existence of a winning strategy is in this case a polynomial time problem [Gradel, 2002].

7 Future and related work

We have seen that subsumption in £ .C with cyclic terminolo­ gies is polynomial for the three types of semantics introduced by Nebel [ 1991). In some applications, it would be interest­ ing to have a mix of all three semantics, and it remains to be seen whether the polynomiality results also hold in such a setting (which would correspond to a restriction of the modal p,-calculus [Kozen, 1983]).

Sub-Boolean DLs (like ££) have attracted renewed at­ tention in the context of so-called non-standard inferences [Kiisters, 200 I] like computing the least common subsumer and the most specific concept. In [Baader, 2003] we have shown that the characterization of subsumption in ££ w.r.t. gfp-semantics also yields an approach for computing the least common subsumer in ££ w.r.t. gfp-semantics. In addition, we have extended the characterization of subsumption in ££ w.r.t. gfp-semantics to the instance problem, and have shown how this can be used to compute the most specific concept.

Simulations and bisimulations play an important role in modal logics (and thus also in description logics). How­ ever, until now they have mostly been considered for modal logics that are closed under all the Boolean operators, and they have usually not been employed for reasoning in the logic. A notable exception are [Kurtonina and de Rijke, 1997; 1999 ], where bisimulation characterizations are given for sub-Boolean Modal Logics and DLs. However, these charac­ terizations are used to give a formal account of the expressive power of these logics. They are not employed for reasoning purposes.

In [Baader eta!., 1999 ], subsumption between ££-concept descriptions was characterized through the existence of ho­ momorphisms between the description trees (basically the syntax trees) associated with the descriptions. If one looks at the polynomial time algorithm for deciding the existence of such a homomorphism, then it is easy to see that it actually computes the greatest simulation between the trees. For trees, the existence of a homomorphism mapping the root to the root coincides with the existence of a simulation containing the tuple of the roots. For graphs, a similar connection does not hold. In fact, for graphs the existence of a homomorphism is an NP-complete problem. For simple conceptual graphs (or equivalently, conjunctive queries) the implication (con­ tainment) problem can be characterized via the existence of certain homomorphisms between graphs [Chein eta!., 1998], and is thus NP-complete.