Bisimulation-Based Comparisons for Interpretations in Description Logics

Abstract

We study comparisons between interpretations in description logics with respect to \logical consequences" of the form of semipositive concepts (like semi-positive concept assertions). Such comparisons are characterized by conditions similar to the ones of bisimulations. The simplest among the considered logics is a variant of PDL (propositional dynamic logic). The others extend that logic with inverse roles, nominals, quanti ed number restrictions, the universal role, and/or the concept constructor for expressing the local re exivity of a role. The studied problems are: preservation of semi-positive concepts with respect to comparisons, the Hennessy-Milner property for comparisons, and minimization of interpretations that preserves semi-positive concepts.

Introduction

Bisimulation is a natural notion of equivalence arose in modal logic [23{25] and

state transition systems [20, 11]. It can be viewed as a binary relation associating state transition systems which behave in the same way in the sense that one system simulates the other and vice versa. Kripke models in modal logic are a special case of labeled state transition systems.

Bisimulations have widely been studied for various variants of modal logic like

dynamic logic, temporal logic, hybrid logic and, in particular, also for description logics (DLs) [13, 6, 14, 21]. They have been used for analyzing the expressivity of a wide range of modal logics (see, e.g., [2] for details), for minimizing state transition systems, as well as for concept learning in DLs (e.g., [19, 22, 10, 5]).

Bisimilarity between two states is usually de ned by three conditions (the states have the same label, each transition from one of the states can be simulated by a similar transition from the other, and vice versa). For bisimulation between two pointed-models, the initial states of the models are also required to be bisimilar. When converse is allowed, two additional conditions are required for bisimulation [2]. Bisimulation conditions for dealing with graded modalities were studied in [4, 3, 12]. In the eld of hybrid logic, the bisimulation condition for dealing with nominals is well known (see, e.g., [1]). In DLs, such conditions are used for dealing with inverse roles, (quanti ed) number restrictions and nominals, respectively. There are also bisimulation conditions for dealing with individuals, the universal role and the Self constructor in DLs [7, 22].

In modal logic, bisimulation invariance has the form: if two states are bisimi

lar then they satisfy the same set of formulas (i.e., all modal formulas are invariant w.r.t. bisimulation). For the converse, the Hennessy-Milner property states that, in nitely branching Kripke models, two states are bisimilar i they satisfy the same set of formulas. This property can be generalized for non- nitely branching Kripke models (see, e.g., [14]).

Simulation is a notion with weaker conditions than bisimulation. It is only

\one way", while bisimulation is \two way". In the most common understanding, the \ways" are related with the \transitions" but not w.r.t. comparison between the sets of atomic formulas satis ed at the considered states. Such simulation preserves positive existential formulas (see, e.g., [2]).

What variant of bisimulation can be used to talk about preservation of pos

itive formulas, which may use both existential and universal modal operators?

De ning positive formulas to be the ones without ? (falsity), : (negation) and

! (implication), in [15] Nguyen gave a bisimulation-based comparison between

Kripke models that preserves positive formulas in basic serial monomodal logics.

In [17] he extended the preservation result also for serial regular grammar logics and proved the corresponding Hennessy-Milner property. Such bisimulationbased comparison uses the conditions of bisimulation for \transitions" and compares the sets of atomic formulas satis ed at the considered states. Bisimulationbased comparison between Kripke models is worth studying, because it can be used for minimizing a Kripke model w.r.t. the set of logical consequences being positive formulas. For example, after constructing a least Kripke model of a positive modal logic program in a serial modal logic [15, 17, 8], one can minimize it w.r.t. positive formulas to obtain a minimal Kripke model that characterizes the program w.r.t. positive consequences. Such minimization is also applicable to (non-serial) DLs [16, 18].

In this paper, we study bisimulation-based comparisons between interpretations in DLs. The simplest among the considered logics is ALCreg, a variant of PDL (propositional dynamic logic). The others extend that logic with inverse roles, nominals, quanti ed number restrictions, the universal role, and/or the concept constructor for expressing the local re exivity of a role. The studied problems are: preservation of semi-positive concepts with respect to comparisons, the Hennessy-Milner property for comparisons, and minimization of interpretations that preserves semi-positive concepts. The class of semi-positive concepts di ers from the class of positive concepts in that, in the recursive de nition, it allows also ?. This is involved with non-seriality.

Apart from [15, 17, 8], bisimulation-based comparisons for modal logics were studied also in [9] (and possibly other works). In [9] the notion is studied at an abstract level for coalgebraic modal logics under the name -simulation, and the term \positive formula" is used instead of \semi-positive formula". As mentioned before, the term \simulation" traditionally has another meaning, and in our opinion ? should not be referred to as \positive". At an abstract level, the work [9] does not have a result like a Hennessy-Milner property. In the current work, to guarantee a Hennessy-Milner property, roles in semi-positive concepts have a speci c syntax due to the presence of the test operator. The de nition of semi-positive concepts itself in the current work is not trivial (e.g., we have that if C is a semi-positive concept then n r::C is also a semi-positive concept).

Our results on preservation of semi-positive concepts and the Hennessy

Milner property w.r.t. comparisons may overlap to a certain degree with the known ones. However, our results on \characterizing bisimulation by semipositive concepts" and \minimization preserving semi-positive concepts" are completely novel.

2

Notation and Semantics of Description Logics

L Our languages use a nite set C of concept names (atomic concepts), a nite set R of role names (atomic roles), and a nite set I of individual names. Let = C [ R [ I . We denote concept names by letters like A and B, denote role names by letters like r and s, and denote individual names by letters like a and b.

We consider some (additional) DL-features denoted by I (inverse), O (nom

inal), Q (quanti ed number restriction), U (universal role), Self. A set of DLfeatures is a set consisting of some or zero of these names.

Let be any set of DL-features and let L stand for ALCreg. The DL language allows roles and concepts de ned inductively as follows: { if r 2 R then r is a role of L { if A 2 C then A is a concept of L { if R and S are roles of L and C is a concept of L then ", R S , R t S, R and C? are roles of L >, ?, :C, C t D, C u D, 9R:C and 8R:C are concepts of L if I 2 then R is a role of L if O 2 and a 2 I then fag is a concept of L if Q 2 , r 2 R and n is a natural number then n r:C and n r:C are concepts of L if fQ; Ig , r 2 R and n is a natural number then n r :C and n r :C are concepts of L if U 2 then U is a role of L if Self 2 and r 2 R then 9r:Self is a concept of L .

We use letters like R and S to denote arbitrary roles, and use letters like C

and D to denote arbitrary concepts. We refer to elements of R also as atomic roles. Let R = R [ fr j r 2 Rg. From now on, by basic roles we refer to elements of R if the considered language allows inverse roles, and refer to elements of R otherwise. In general, the language decides whether inverse roles are allowed in the considered context.

An interpretation I = h I ; I i consists of a non-empty set I , called the domain of I, and a function I , called the interpretation function of I, which maps every concept name A to a subset AI of I , maps every role name r to a binary relation rI on I , and maps every individual name a to an element aI (R S)I = RI SI (R t S)I = RI [ SI (R )I = (RI ) (C?)I = fhx; xi j CI (x)g

I g "I = fhx; xi j x 2

U I = I I (R )I = (RI ) 1 >I = I ?I = ; (:C)I = I n CI (C t D)I = CI [ DI (C u D)I = CI \ DI

fagI = faI g (9r:Self)I = fx 2

I j rI (x; x)g (9R:C)I = fx 2 (8R:C)I = fx 2 ( n R:C)I = fx 2 ( n R:C)I = fx 2

I j 9y [RI (x; y) and CI (y)] I j 8y [RI (x; y) implies CI (y)]g I j #fy j RI (x; y) and CI (y)g I j #fy j RI (x; y) and CI (y)g ng ng of I . The interpretation function I is extended to complex roles and complex concepts as shown in Figure 1, where # stands for the cardinality of the set . We write CI (x) to denote x 2 CI , and write RI (x; y) to denote hx; yi 2 RI .

An interpretation I is said to be serial in L if, for every basic role R of L

and every x 2 I , there exists y 2 I such that hx; yi 2 RI .

We say that a role R is in the converse normal form (CNF) if the inverse

constructor is applied in R only to role names and the role U is not under the scope of any other role constructor. Since every role can be translated to an equivalent role in CNF,1 in this paper we assume that roles are presented in the CNF. 3

Positive and Semi-Positive Concepts

Let Lpos be the smallest set of concepts and Lpo;9s, Lpo;8s be the smallest sets of roles de ned recursively as follows: { if r 2 R then r is a role of Lpo;9s and Lpo;s , {{ iiff IR2andaSndarre2roleRs othfeLnpo;rs ainsdaCroilse aofcLo8npco;9sepatnodf LLppoo;8ss,

9 then ", R S , R t S, R and C? are roles of Lpo;s , 9 pos { if R and S are roles of Lpo;s and C is a concept of L

8 { itfhAen2", RC thSen,RAtisSa, Rconcaenpdt (o:fCL)p?osa,re roles of Lpo;8s, { if O 2 and a 2 I then fag is a concept of Lpos , 1 For example, ((r t s ) r ) = (r )

(r t s). { if Self 2 and r 2 R then 9r:Self is a concept of Lpos , { if C>is, aCctonDce,pCt uofDL,po9sR, :RC iasnadr8oSle:Cof aLrepo;c9soanncdepStsiosfaLrpoolse, of Lpo;8s then itfhQen2 n, rr:C2 anRd andn nr:(i:sCa )naatruercaolnncuemptbseorf Lpos , itfhfenQ; Ign r : C,ra2nd R nanrd :n(:iCsa) anraetucroanlcneputmsboefrLpos , if U 2 then 8U:C and 9U:C are concepts of Lpos .

A concept of Lpos is called a positive concept of L . We introduce both Lpo;8s and Lpo;9s due to the test constructor of roles. The concepts 9(A?):B and

8((:A)?):B are positive concepts; they are equivalent to A u B and A t B,

respectively. That the concept n R:(:A) is positive should not be a surprise, as 8R:A is equivalent to 0 R:(:A). sp of rLoleets Ldesp nbeed tahneaslomgaolulesslyt tsoetthofe ccoanseceopftLspaons d, LLpso;p;s9,,LLpo;8s;8ebxecetphtetshmatal?lesits aselstos allowed as a concept of Lsp . We call concepts of Lsp 9semi-positive concepts of L . 4

Bisimulation-Based Comparisons for Interpretations

Let I and I0 be interpretations. A binary relation Z I I0 is called an L comparison between I and I0 if the following conditions hold for every a 2 I , A 2 C , r 2 R, x; y 2 I , x0; y0 2 I0 :

Z(aI ; aI0 ) Z(x; x0) ) [AI (x) ) AI0 (x0)] [Z(x; x0) ^ rI (x; y)] ) 9y0 2 [Z(x; x0) ^ rI0 (x0; y0)] ) 9y 2

I0 [Z(y; y0) ^ rI0 (x0; y0)]

I [Z(y; y0) ^ rI (x; y)]; if I 2

then if O 2 if Q 2 then then [Z(x; x0) ^ rI (y; x)] ) 9y0 2 [Z(x; x0) ^ rI0 (y0; x0)] ) 9y 2

I0 [Z(y; y0) ^ rI0 (y0; x0)]

I [Z(y; y0) ^ rI (y; x)];

Z(x; x0) ) [x = aI ) x0 = aI0 ]; if fQ; Ig

then (additionally) if Z(x; x0) holds then, for every role name r, there exists a bijection h : fy j rI (x; y)g ! fy0 j rI0 (x0; y0)g such that h Z, if Z(x; x0) holds then, for every role name r, there exists a bijection h : fy j rI (y; x)g ! fy0 j rI0 (y0; x0)g such that h Z, ( 1 ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) ( 6 ) ( 7 ) ( 8 ) 1. The relation fhx; xi j x 2 I g is an L -comparison between I and I. 2. If Z1 is an L -comparison between I0 and I1, and Z2 is an L -comparison between I1 and I2, then Z1 Z2 is an L -comparison between I0 and I2. 3. If Z is a set of L -comparison between I and I0 then S Z is also an L comparison between I and I0. if U 2

then then

Lemma 4.2. Let I and I0 be interpretations and Z be an L -comparison between I and I0. Then the following properties hold for every concept C of Lsp , every role R of Lsp;9, every role S of Lsp;8, every x; y 2 I , every x0; y0 2 I0 , and every a 2 I:

Z(x; x0) ) [CI (x) ) CI0 (x0)] [Z(x; x0) ^ RI (x; y)] ) 9y0 2 [Z(x; x0) ^ SI0 (x0; y0)] ) 9y 2

I0 [Z(y; y0) ^ RI0 (x0; y0)]

I [Z(y; y0) ^ SI (x; y)]:

See the appendix for a proof of this lemma.

A concept C of L is said to be preserved by L -comparisons if, for any

interpretations I, I0 and any L -comparison Z between I and I0, if Z(x; x0) holds and x 2 CI then x0 2 CI0 . The following theorem follows immediately from the assertion ( 13 ) of Lemma 4.2.

Theorem 4.3. All concepts of Lsp are preserved by L -comparisons. Corollary 4.4. All concepts of Lpos are preserved by L -comparisons.

Let I and I0 be interpretations, x 2 I and x0 2

I0 . De ne that: { x is equivalent to x0 w.r.t. (concepts of) L , denoted by x concept C of L , x 2 CI i x0 2 CI0 ; x0, if, for every { x is less than or equal to x0 w.r.t. concepts of Lsp (resp. Lpos ), denoted by x sp x0 (resp. x pos x0), if, for every concept C of Lsp (resp. Lpos ), x 2 CI implies x0 2 CI0 ; { x is equivalent to x0 w.r.t. concepts of Lsp , denoted by x sp x0, if x sp x0 and x0 sp x.

We say that an interpretation I is nitely branching (or image- nite) w.r.t.

L if, for every x 2 I and every basic role R of L , the set fy 2 I j RI (x; y)g

is nite. We say that I is unreachable-objects-free (w.r.t. L ) if every element of

I is reachable from some aI (with a 2 I ) via a path consisting of edges being instances of basic roles (of L ). The following theorem comes from our work [7].

Theorem 4.5 (The Hennessy-Milner Property). Let I and I0 be nitely branching interpretations (w.r.t. L ) such that, for every a 2 I , aI aI0 . Suppose that if U 2 then either I 6= ; and both I, I0 are nite, or both I, I0 are unreachable-objects-free. Then, for every x 2 I and x0 2 I0 , x x0 i there exists an L -bisimulation Z between I and I0 such that Z(x; x0) holds. In particular, the relation fhx; x0i 2 I I0 j x x0g is an L -bisimulation between I and I0.

In the rest of this section we present theorems similar to the Hennessy-Milner

property that are related to L -comparisons and/or semi-positive concepts. Theorem 4.6. Let I and I0 be nitely branching interpretations (w.r.t. L ) such that, for every a 2 I , aI sp aI0 . Suppose that if U 2 then either I 6= ; and both I, I0 are nite, or botshp Ix0 i , I0 are unreachable-objects-free. Then, for every x 2 I and x0 2 I0 , x there exists an L -comparison Z between I and I0 such that Z(x; x0) holds. In particular, the relation fhx; x0i 2 I I0 j x sp x0g is an L -comparison between I and I0.

See the appendix for a proof of this theorem.

Analyzing the proof of Theorem 4.6, it can be seen that, in the case Q 2= , ? is only used for showing that there exists y 2 I such that rI (x; y) holds when proving the condition ( 4 ). If I is a serial interpretation then that property is guaranteed. Therefore, we also have the following theorem, whose proof is very similar to the proof of Theorem 4.6.

Theorem 4.7. Let I and I0 be nitely branching interpretations (w.r.t. L ) such that I is serial and, for every a 2 I , aI pos aI0 . Suppose Q 2= and if U 2 then either I 6= ; and both I, I0 are nite, or both I, I0 are unreachableobjects-free. Then, for every x 2 I and x0 2 I0 , x pos x0 i there exists an L -comparison Z between I and I0 such that Z(x; x0) holds. In particular, the relation fhx; x0i 2 I I0 j x pos x0g is an L -comparison between I and I0. 5

Characterizing Bisimulation by Semi-Positive Concepts

In the case Q 2 , there is a closer relationship between semi-positive concepts and L -bisimulation from the semantic point of view.

Theorem 5.1. Let I and I0 be nitely branching interpretations (w.r.t. L ) such that, for every a 2 I , aI sp aI0 . Suppose Q 2 and if U 2 then both I and I0 are unreachable-objects-free. Then, for every x 2 I and x0 2 I0 , x sp x0 i there exists an L -bisimulation Z between I and I0 such that Z(x; x0) holds. In particular, the relation fhx; x0i 2 I I0 j x sp x0g is an L bisimulation between I and I0.

See the appendix for a proof of this theorem.

Corollary 5.2. Let I and I0 be nitely branching interpretations (w.r.t. L ) such that, for every a 2 I , aI sp aI0 . Suppose Q 2 and if U 2 then both I and I0 are unreachable-objects-free. Then, for every x 2 I and x0 2 I0 , x sp x0 i x x0.

This corollary follows from Theorems 5.1 and 4.5.

Example 5.3. We show that the assumption Q 2 of Theorem 5.1 is neces

sary. Let = ;, I = fag, C = fA; Bg, R = frg and let I, I0 be the interpretations speci ed as follows.

{ {

I = fu; v0; v1; v2g, aI = u, rI = fhu; v0i; hu; v1i; hu; v2ig, AI = fv1; v2g, BI = fv2g,

I0 = fu; v0; v2g, aI0 = u, rI0 = fhu; v0i; hu; v2ig and AI0 = BI0 = fv2g.

Notice that I0 is obtained from I by deleting v1. Observe that there are L

comparisons between I and I0 as well as between I sp aI0 , but aI 6 0 and I, but there is no L -bisimulations between I and I0. In particular, aI aI0 . C

The point of the above example is that, when Q 2= , if v0, v1, v2 are pairwise di erent r-successors of u, v0 sp v1 and v1 sp v2 then the edge hu; v1i 2 rI is not essential for the semantics of semi-positive concepts. Also note that, when Q 2= , if v and v0 are di erent r-successors of u such that v sp v0 then the edge hu; v0i 2 rI is not essential for the semantics of semi-positive concepts.

Suppose Q 2= and let I be a nitely branching interpretation. We say that I is Lsp -tidy if it is unreachable-objects-free and, for every x; y; y0; y00 2 I and every basic role R of L , { if fhx; yi; hx; y0ig RI and y sp y0 then y = y0, { if fhx; yi; hx; y0i; hx; y00ig RI , y sp y0 and y0 sp y00 then y = y0 or y0 = y00 or (Self 2 and y0 = x).

Theorem 5.4. Suppose Q 2= . Let I and I0 be nitely branching and Lsp -tidy interpretations such that, for every a 2 I , aI sp aI0 . Then, for every x 2 I sauncdhxt0ha2t ZI(0x,; xx0) hspolxds0.i Inthpearreticeuxliastrs, athne Lrel-abtiisoinmfuhlaxt;ixon0i Z2 beItweenII0 jaxnd Isp0 x0g is an L -bisimulation between I and I0.

See the appendix for a proof of this theorem.

Auto-Bisimulation and Minimization

In this section, we recall some results of our manuscript [7], not published in [6].

An L -bisimulation between I and itself is called an L -auto-bisimulation of I.

An L -auto-bisimulation of I is said to be the largest if it is larger than or equal to ( ) any other L -auto-bisimulation of I.

Proposition 6.1. For every interpretation I, the largest L -auto-bisimulation of I exists and is an equivalence relation. C

Given an interpretation I, by ;I we denote the largest L -autobisimulation of I, and by ;I we denote the binary relation on I with the property that x ;I x0 i x is L -equivalent to x0.

Theorem 6.2. For every nitely branching interpretation I, ;I is the largest L -auto-bisimulation of I (i.e. the relations ;I and ;I coincide).

An interpretation I is said to be minimal among a class of interpretations

if I belongs to that class and, for every other interpretation I0 of that class, # I # I0 (the cardinality of I is less than or equal to the cardinality of I0 ).

A concept assertion of L (resp. Lsp ) is an expression of the form C(a), where C is a concept of L (resp. Lsp ). We say that an interpretation I satis es a concept assertion C(a) if a 2 CI . We say that I satis es the same concept assertions of L sp ) as an interpretation I0 if, for every concept assertion C(a) of L (resp(.reLsspp.)L,I satis es C(a) i I0 satis es C(a).

Theorem 6.3. Suppose fI; O; U g and let I be an unreachable-objects-free interpretation. If I= ;I is nitely branching then it is a minimal interpretation that satis es the same concept assertions of L as I.

For the case when Q 2 or Self 2 , in order to obtain a result similar to

Theorem 6.3, we introduce QS-interpretations as follows.

A QS-interpretation is a tuple I = h I ; I ; QI ; SI i, where { h I ; I i is an interpretation, { QI is a function that maps every basic role to a function I I ! N such that QI (R)(x; y) > 0 i hx; yi 2 RI , where N is the set of natural numbers, { SI is a function that maps every role name to a subset of I . ng ng: ;I #fy0 2 [y] ;I j hx0; y0i 2 RI g

If I is a QS-interpretation then we rede ne

(9r:Self)I = fx 2 (

n R:C)I = fx 2 ( n R:C)I = fx 2 I j I j x 2 SI (r)g I j fQI (R)(x; y) j CI (y)g fQI (R)(x; y) j CI (y)g

Other notions for interpretations remain unchanged for QS-interpretations.

For I being an interpretation, the quotient QS-interpretation of I w.r.t. ;I ,

denoted by I=QS , is the QS-interpretation I0 = h I0 ; I0 ; QI0 ; SI0 i such that: ;I { h I0 ; I0 i is the quotient interpretation of I w.r.t. { for every basic role R and every x; y 2 I ,

QI0 (R)([x] Theorem 6.4. Let I be an unreachable-objects-free interpretation. If I=QS ;I is nitely branching then it is a minimal QS-interpretation that satis es the same concept assertions of L as I. 7

Minimization Preserving Semi-Positive Concepts

Suppose fO; U; Selfg and let I be a nitely branching interpretation such that it is also unreachable-objects-free when U 2 . By Tidysp(I) we denote the maximal Lsp -tidy sub-interpretation of I obtained by modifying I as follows: { For each r 2 R, if fhx; yi; hx; y0ig rI , y

delete the pair hx; y0i from rI . { For each r 2 R, if fhx; yi; hx; y0i; hx; y00ig rI , y sp y0, y0 sp y00, y 6 sp y0, y0 6 sp y00 and (Self 2= or y0 6= x) then delete the pair hx; y0i from rI . { Delete from the domain of I all elements not reachable from any aI (with a 2 I ) via a path consisting of edges being instances of basic roles of L . sp y0, y 6= y0 and y0 6= x then Lemma 7.1. Suppose fO; U; Selfg and let I be a nitely branching interpretation such that it is also unreachable-objects-free when U 2 . Then Tidysp(I) satis es the same concept assertions of Lsp as I. Proof. Let I0 = Tidysp(I) and let Z, Z0 be the smallest binary relations such that the following conditions hold for every a 2 I , r 2 R, x; y 2 I , x0; y0 2 I0 : { Z(aI ; aI ) and Z0(aI ; aI ), { Z(x; x0) ^ rI (x; y) ^ rI0 (x0; y0) ^ y { Z0(x0; x) ^ rI (x; y) ^ rI0 (x0; y0) ^ y0 sp y0 ) Z(y; y0),

sp y ) Z0(y0; y).

It is easy to see that Z is an L -comparison between I and I0, and Z0 is an

L -comparison between I0 and I. Therefore, by Theorem 4.3, I0 and I satisfy

the same concept assertions of Lsp . C Theorem 7.2. Suppose fO; U; Selfg. Let I0 and I00 be nitely branching interpretations such that they are also unreachable-objects-free when U 2 and they satisfy the same concept assertions of Lsp . Let I = Tidysp(I0), I2 = I= ;I if Self 2= , and I2 = I=QS ;I if Self 2 . Then I2 satis es the same concept assertions of Lsp as I00 and # I2 # I00 .

I0=QS ;I0 . By Theorems 6.3 and 6.4, # follows that # I2 # I00 .

Proof. Let I0 =sp .TCidoynsspe(qIu00e)n.tBlyy, bLyemThmeaor7e.m1, 5I.4a,nthderIe0 esxaitsitssfyanthLe s-abmiseimcuolnacteiopnt assertions of L between I and I0. By Theorem 4.5, it follows that I and I0 satisfy the same concept assertions of L . If Self 2= then let I20 = I0= ;I0 , else let I20 = I2 = # I20 . Since # I20 # I00 , it

C Theorem 7.3. Suppose Q 2 . Let I and I0 be nitely branching interpretations such that they are also unreachable-objects-free when U 2 and they satisfy tthheatssaamties ceosntcheeptsaamsseerctoionncsepotfaLsssepr.tiTonhesnofIL2s=p aIs=QIS0 ;aIndis #a QIS2 -int#erprIe0t.ation Proof. Let I20 = I0=QS ;I0 . By Theorem 5.1, there exists an L -bisimulation between I and I0. By Theorem 4.5, it follows that I and I0 satisfy the same concept assertions of L . Hence, by Theorem 6.4, # I2 = # I20 . Since # I20 # I0 , it follows that # I2 # I0 . C

Notice that minimization of interpretations that preserves semi-positive con

cepts for the case when Q 2= and I 2 is not investigated in this section. 8

Conclusions

We have studied bisimulation-based comparisons between interpretations in a reasonably systematic way for a large class of useful description logics and obtained novel results on \characterizing bisimulation by semi-positive concepts" and \minimization preserving semi-positive concepts".

Acknowledgments. This work was supported by the Polish National Science Centre (NCN) under Grant No. 2011/01/B/ST6/02759.

Proofs

Proof of Lemma 4.2

We prove this lemma by induction on the structures of C, R and S.

Consider the assertion (14). Suppose Z(x; x0) and RI (x; y) hold. By induction

on the structure of R we prove that there exists y0 2 I0 such that Z(y; y0) and RI0 (x0; y0) hold. The base case occurs when R is a role name and the assertion for it follows from ( 3 ). The induction steps are given below.

{ Case R = " is trivial. { Case R = R1 R2, where R1 and R2 are roles of Lsp;9: We have that (R1

R2)I (x; y) holds. Hence, there exists z 2 I such that R1I (x; z) and R2I (z; y)

hold. By the inductive assumption of ( 14 ), there exists z0 2 I0 such that Z(z; z0) and R1I0 (x0; z0) hold, and there exists y0 2 I0 such that Z(y; y0) and R2I0 (z0; y0) hold. Since R1I0 (x0; z0) and R2I0 (z0; y0) hold, we have that (R1 R2)I0 (x0; y0) holds, i.e. RI0 (x0; y0) holds. { Case R = R1 t R2, where R1 and R2 are roles of Lsp;9, is trivial. { Case R = R1, where R1 is a role of Lsp;9: Since RI (x; y) holds, there exists x0; : : : ; xk 2 I such that x0 = x, xk = y and, for 1 i k, R1I (xi 1; xi) holds. Let x00 = x0. For each 1 i k, since Z(xi 1; x0i 1) and R1I (xi 1; xi) hold, by the inductive assumption of ( 14 ), there exists x0i 2 I such that Z(xi; x0i) and R1I0 (x0i 1; x0i) hold. Hence, Z(xk; x0k) and (R1)I0 (x00; x0k) hold. Let y0 = x0 . Thus, Z(y; y0) and RI0 (x0; y0) hold.

k { Case R = (D?), where D is a concept of Lsp : By the de nition of (D?)I , we have that DI (x) holds and x = y. By the inductive assumption of ( 13 ), DI0 (x0) holds, and therefore RI0 (x0; x0) holds. By choosing y0 = x0, we have that Z(y; y0) and RI0 (x0; y0) hold. { Case I 2 and R = r : The assertion for this case follows from ( 5 ).

The assertion (15) can be proved analogously as for (14) except for the case

S = (:C)?, where C is a concept of Lsp . The proof for this case is as follows. Suppose Z(x; x0) and SI0 (x0; y0) hold. Thus, (:C)I0 (x0) holds and x0 = y0. By the contrapositive of the inductive assumption of ( 13 ), it follows that (:C)I (x) holds. By choosing y = x, Z(y; y0) and SI (x; y) hold.

Consider the assertion (13). Suppose Z(x; x0) and CI (x) hold, where C is a

concept of Lsp . We show that CI0 (x0) holds. The cases when C is of the form >, ?, A, D t D0 or D u D0 are trivial.

{ Case C = 9R:D, where R is a role of L ;9 and D is a concept of Lsp : Since sp (9R:D)I (x) holds, there exists y 2 I such that RI (x; y) and DI (y) hold. By the inductive assumption of ( 14 ) (proved earlier), there exists y0 2 I0 such that Z(y; y0) and RI0 (x0; y0) hold. By the inductive assumption of ( 13 ), DI0 (y0) holds. Therefore, CI0 (x0) holds. { Case C = 8S:D, where S is a role of L ;8 and D is a concept of Lsp : Let sp y0 be an arbitrary element of I0 such that SI0 (x0; y0) holds. We show that DI0 (y0) holds. By the inductive assumption of ( 15 ) (proved earlier), there exists y 2 I such that Z(y; y0) and SI (x; y) hold. Since (8S:D)I (y) holds, it follows that DI (y) holds. Therefore, by the inductive assumption of ( 13 ), it follows that DI0 (y0) holds. { Case O 2 and C = fag: Since fagI (x) holds, we have that x = aI . By the condition ( 7 ), it follows that x0 = aI0 . Hence CI0 (x0) holds. { Case Self 2 and C = 9r:Self: Since (9r:Self)I (x) holds, we have that rI (x; x) holds. By the condition ( 12 ), it follows that rI0 (x0; x0) holds. Hence CI0 (x0) holds. { Case Q 2 and C = ( n r:D), where D is a concept of Lsp : By the condition ( 8 ), there exists a bijection h : fy j rI (x; y)g ! fy0 j rI0 (x0; y0)g such that h Z. Since ( n r:D)I (x) holds, there exist pairwise di erent y1, . . . , yn 2 I such that rI (x; yi) and DI (yi) hold for every 1 i n. For each 1 i n, let yi0 = h(yi). Thus, Z(yi; yi0) holds. By the inductive assumption of ( 13 ), it follows that DI0 (yi0) holds. Since rI0 (x0; y0) and DI0 (yi0) hold for 1 i n, and yi 6= yj for 1 i 6= j n, it follows that ( n r:D)I0 (x0) holds, which means CI0 (x0) holds. { Case fQ; Ig and C = ( n r 1:D), where D is a concept of Lsp , can be proved analogously to the above case. { Case Q 2 and C = ( n r:(:D)), where D is a concept of Lsp : For the sake of contradiction, suppose CI0 (x0) does not hold. Thus, (:C)I0 (x0) holds, which means ( (n + 1) r:(:D))I0 (x0) holds. By the condition ( 8 ), there exists a bijection h : fy j rI (x; y)g ! fy0 j rI0 (x0; y0)g such that h Z. Since ( (n + 1) r:(:D))I0 (x0) holds, there exist pairwise di erent y10, . . . , yn0+1 2 I0 such that rI0 (x0; yi0) and (:D)I0 (yi0) hold for all 1 i n + 1. For each 1 i n + 1, let yi = h 1(yi0). Since h is a bijection, y1; : : : ; yn+1 are pairwise di erent, and by the de nition of h, rI (x; yi) holds for every 1 i n + 1. For 1 i n + 1, since (:D)I0 (yi0) holds, by the contrapositive of the inductive assumption of ( 13 ), it follows that (:D)I (yi) holds. Thus, (:C)I (x) holds, which contradicts the assumption that CI (x) holds. Therefore, CI0 (x0) holds. { Case fQ; Ig and C = ( n r 1:(:D)), where D is a concept of Lsp , can be proved analogously to the above case. { Case U 2 and C = 8U:D, where D is a concept of Lsp : Let y0 2 I0 . By the condition ( 11 ), there exists y 2 I such that Z(y; y0) holds. Since CI (x) holds, it follows that DI (y) holds. By the inductive assumption of ( 13 ), it follows that DI0 (y0) holds. Hence CI0 (x0) holds. { Case U 2 and C = 9U:D, where D is a concept of Lsp : Since CI (x) holds, there exists Iy0 s2uch that Z(y; y0) holds. By the inductive assumption

I such that DI (y) holds. By the condition (10),

there exists y0 2 of ( 13 ), it follows that DI0 (y0) holds. Hence CI0 (x0) holds. Proof of Theorem 4.6

First, suppose Z is an L -comparison between I and I0 such that Z(x; x0) holds.

We show that x sp x0. Let C be an arbitrary concept of Lsp such that CI (x) holds. Thus, by the assertion ( 13 ) of Lemma 4.2, CI0 (x0) holds. Therefore, x x0. sp

Conversely, we show that Z = fhx; x0i 2 comparison between I and I0.

I

I0 j x sp x0g is an L { The condition ( 1 ) immediately follows from the assumption of the theorem. { Consider the condition ( 2 ). If Z(x; x0) and AI (x) hold, then by the de nition of Z, AI0 (x0) holds. { Consider the condition ( 3 ). Suppose Z(x; x0) and rI (x; y) hold. Let S = fy0 2 I0 j rI0 (x0; y0)g. We show that there exists y0 2 S such that Z(y; y0) holds. Since (9r:>)I (x) holds and x sp x0, it follows that (9r:>)I0 (x0) holds. Consequently, S 6= ;. Since I0 is nitely branching, S must be nite. Let the elements of S be y10, . . . , y0 . For the sake of contradiction, suppose that for n every 1 i n, Z(y; yi0) does not hold, which means that y 6 sp yi0. Thus, for every 1 i n, there exists a concept Ci of Lsp such that CiI (y) holds, but CiI0 (y0) does not. Let C = 9r:(C1 u : : : u Cn). Thus, CI (x) holds, but CI0 (x0) does not. This contradicts x sp x0. Hence, there exists yi0 2 S such that Z(y; yi0) holds. { Consider the condition ( 4 ). Suppose Z(x; x0) and rI0 (x0; y0) hold. Let S = fy 2 I j rI (x; y)g. We show that there exists y 2 S such that Z(y; y0) holds. For the sake of contradiction, suppose S = ;. Thus, (8r:?)I (x) holds. Since x sp x0, it follows that CI0 (x0) holds, and hence ?I0 (y0) holds, which is a contradiction. Therefore, S 6= ;. Since I is nitely branching, S must be nite. Let y1; : : : ; yn be all the elements of S. For the sake of contradiction, suppose that for every 1 i n, Zi(yi; y0) does not hold, i.e. yi 6 sp y0. Thus, for every 1 i n, there exists a concept Ci of Lsp such that CiI (yi) holds, but CiI0 (y0) does not. Let C = 8r:(C1 t: : : tCn). Clearly, CI (x) holds, but CI0 (x0) does not. This contradicts x sp x0. Hence, there exists yi 2 S such that Z(yi; y0) holds. { The conditions ( 5 ) and ( 6 ) can be proved analogously as for the conditions ( 3 ) and ( 4 ), respectively. { Consider the condition ( 7 ) and the case O 2 . Suppose Z(x; x0) holds and x = aI . Since fagI (x) holds and x sp x0, it follows that fagI0 (x0) holds.

Therefore, x0 = aI0 . { Consider the condition ( 8 ) and the case Q 2 . Suppose Z(x; x0) holds, i.e., x sp x0. Let S = fy 2 I j rI (x; y)g and S0 = fy0 2 I0 j rI0 (x0; y0)g. Since I and I0 are nitely branching, S and S0 must be nite. Let m = #S and n = #S0. We rst show that m = n. If m > n then x 2 ( m r:>)I and x0 2= ( m r:>)I0 , which contradicts x sp x0. If m < n then x 2 ( m r::?)I and x0 2= ( m r::?)I0 , which contradicts x sp x0. Therefore m = n. Let S = fy1; : : : ; ymg. We can try to construct a bijection h : S ! S0 such that h Z as follows. For each i from 1 to m :

If there exists y0 2 S0 nfh(y1); : : : ; h(yi 1)g such that Z(yi; y0) holds then

set h(yi) := y0 and continue with the next i.

Consider the other case. By the assertion (3), there exists y0 2 S0 such

that Z(yi; y0) holds. Nondeterministically choose 1 j < i such that h(yj ) = y0, exchange yi and yj , and go back to the previous step.

For the sake of contradiction, suppose that for some 1 i m, ev

ery possible run of the above loop does not terminate. There must exist S0 fy1; : : : ; yi 1g such that, for every y 2 S0 [ fyig and every y0 2 S0, if Z(y; y0) holds then y0 2 h(S0). Let S0 [ fyig = fu1; : : : ; uhg and S0 n h(S0) = fv1; : : : ; vkg. We have h + k = m + 1, hence h > m k. For each 1 i h and 1 j k, since Z(ui; vj ) does not hold, there exists a concept Ci;j of Lsp such that CiI;j (ui) holds, but CiI;j0 (vj ) does not. For 1 i h, let Ci = Ci;1 u : : : u Ci;k. Then let C = C1 t : : : t Ch. Observe that fu1; : : : ; uhg CI and fv1; : : : ; vkg \ CI0 = ;. Thus, x 2sp( x0h. Tr:hCe)rIefoarned, x0 2= ( h r:C)I0 , which contradicts the assumption that x there exists a bijection h : S ! S0 such that h Z. { The condition ( 9 ) can be proved analogously as for the condition ( 8 ). { Consider the condition ( 10 ) and the case U 2 . By the assumption of this case, either I 6= ; and both I, I0 are nite, or both I, I0 are unreachableobjects-free.

Case I 6= ; and both I, I0 are nite: Let x 2 I and let x01; : : : ; x0n be all the elements of I0 . For the sake of contradiction, suppose that for every 1 i n, x 6 sp x0i. Thus, for every 1 i n, there exists a concept Ci of Lsp such that CiI (x) holds, but CiI0 (x0i) does not. Let C = C1 u : : : u Cn and a 2 I . Since CI (x) holds, (9U:C)I (aI ) also holds, but (9U:C)I0 (aI0 ) does not, which contradicts the assumption aI sp aI0 .

Case both I, I0 are unreachable-objects-free: The condition ( 10 ) follows from the conditions ( 1 ), ( 3 ) and ( 4 ). { The condition ( 11 ) can be proved analogously as for the condition ( 10 ). { Consider the condition ( 12 ) and the case Self 2 sp x0, it follows that . Suppose Z(x; x0) and rI (x; x) hold. Since (9r:Self)I (x) holds and x (9r:Self)I0 (x0) holds. Hence, rI0 (x0; x0) holds.

Proof of Theorem 5.1 If Z is an L -bisimulation between I ansdp Ix00.suFcohr tthhaet rZe m(xa;ixn0i)nghoalsdssertthioenn,s boyf

Theorem 4.5, x x0, and hence x

the current theorem, we show that Z = fhx; x0i 2 I I0 j x sp x0g is an

L -bisimulation between I and I0.

{ The condition ( 1 ) immediately follows from the assumption of the theorem. { Consider the condition (2'). Suppose Z(x; x0) holds. By the de nition of Z,

AI (x) holds i AI0 (x0) holds. { Consider the condition (7') and the case O 2 . Suppose Z(x; x0) holds.

Thus, fagI (x) holds i fagI0 (x0) holds. That is, x = aI i x0 = aI0 . Proof of Theorem 5.4 Let Z = fhx; x0i 2 I I0 j x sp x0g. Analyzing the proof of Theorem 5.1, it su ces to show that the condition ( 3 ) holds (the conditions ( 4 ), ( 5 ) and ( 6 ) can be proved in a similar way). Suppose Z(x; x0) ^ rI (x; y) holds. We show that there exists y0 such that Z(y; y0) ^ rI0 (x0; y0) holds. This is trivial for the case when Self 2 and y = x. So, suppose Self 2= or y 6= x. Analogously to the proof of Theorem 4.6, it can be shown that there exists y20 2 I0 such that rI0 (x0; y20) holds and y sp y20. Dually, there exists y10 2 I0 such that rI0 (x0; y10) rhLIos(pldx-ts;iyda2yn),dehiyot10lhde,r syyp1 =y.ysSp1i moyr10ilyaarn=lyd,yyt2h.20eSrienscpeexyiys21t. yH1se;pnyyc21e02y1spIysspauncydh ythspatspyr2yI.20(Sxi;nsycp1e)yI2a,niidst follows that y sp y10 or y sp y20, which completes the proof.

References

1. C. Areces , P. Blackburn , and M. Marx . Hybrid logics: Characterization, interpolation and complexity . J. Symb. Log. , 66 ( 3 ): 977 { 1010 , 2001 .

2. P. Blackburn , M. de Rijke, and Y. Venema. Modal Logic . Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001 .

3. W. Conradie . De nability and changing perspectives: The Beth property for three extensions of modal logic . Master's thesis , ILLC, University of Amsterdam, 2002 .

4. M. de Rijke . A note on graded modal logic . Studia Logica , 64 ( 2 ): 271 { 283 , 2000 .

5. A.R. Divroodi , Q.-T. Ha , L.A. Nguyen , and H.S. Nguyen . On C-learnability in description logics . In Proceedings of ICCCI'2012 (1) , volume 7653 of LNCS , pages 230 { 238 . Springer, 2012 .

6. A.R. Divroodi and L.A. Nguyen . On bisimulations for description logics . In Proceedings of CS&P' 2011 , pages 99 { 110 , 2011 .

7. A.R. Divroodi and L.A. Nguyen . On bisimulations for description logics . http: //arxiv.org/abs/1104. 1964 , 2011 .

8. B. Dunin-Keplicz , L.A. Nguyen , and A. Szalas . Tractable approximate knowledge fusion using the Horn fragment of serial propositional dynamic logic . Int. J. Approx. Reasoning , 51 ( 3 ): 346 { 362 , 2010 .

9. Daniel Gor n and Lutz Schroder. Simulations and bisimulations for coalgebraic modal logics . CoRR, abs/1303.2467 , 2013 .

10. Q .-T. Ha, T.-L.-G. Hoang , L.A. Nguyen , H.S. Nguyen , A. Szalas , and T.-L. Tran . A bisimulation-based method of concept learning for knowledge bases in description logics . In Proceedings of SoICT'2012 , pages 241 { 249 . ACM, 2012 .

11. M. Hennessy and R. Milner . Algebraic laws for nondeterminism and concurrency . Journal of the ACM , 32 ( 1 ): 137 { 161 , 1985 .

12. D. Janin and G. Lenzi . On the relationship between monadic and weak monadic second order logic on arbitrary trees, with applications to the mu-calculus . Fundam . Inform., 61 ( 3-4 ): 247 { 265 , 2004 .

13. N. Kurtonina and M. de Rijke. Expressiveness of concept expressions in rst-order description logics . Artif . Intell., 107 ( 2 ): 303 { 333 , 1999 .

14. C. Lutz , R. Piro , and F. Wolter . Description logic TBoxes: Model-theoretic characterizations and rewritability . In T. Walsh, editor, Proceedings of IJCAI'2011 , pages 983 { 988 , 2011 .

15. L.A. Nguyen . Constructing the least models for positive modal logic programs . Fundamenta Informaticae , 42 ( 1 ): 29 { 60 , 2000 .

16. L.A. Nguyen . A bottom-up method for the deterministic Horn fragment of the description logic ALC . In Proceedings of JELIA 2006 , LNAI 4160 , pages 346 { 358 . Springer, 2006 .

17. L.A. Nguyen . Constructing nite least Kripke models for positive logic programs in serial regular grammar logics . Logic Journal of the IGPL , 16 ( 2 ): 175 { 193 , 2008 .

18. L.A. Nguyen . Horn knowledge bases in regular description logics with PTime data complexity . Fundamenta Informaticae , 104 ( 4 ): 349 { 384 , 2010 .

19. L.A. Nguyen and A. Szalas . Logic-based roughi cation . In A. Skowron and Z . Suraj, editors, Rough Sets and Intelligent Systems (To the Memory of Professor Zdzislaw Pawlak) , Vol. 1 , pages 529 { 556 . Springer, 2012 .

20. D.M.R. Park . Concurrency and automata on in nite sequences . In Peter Deussen, editor, Proceedings of the 5th GI-Conference , volume 104 of LNCS , pages 167 { 183 . Springer, 1981 .

21. R. Piro . Model Theoretic Characterisations of Description Logics . PhD thesis , University of Liverpool, 2012 .

22. T.-L. Tran , Q.-T. Ha, T.-L.-G. Hoang , L.A. Nguyen , H.S. Nguyen , and A. Szalas . Concept learning for description logic-based information systems . In Proceedings of KSE'2012 , pages 65 { 73 . IEEE Computer Society, 2012 .

23. J. van Benthem. Modal Correspondence Theory . PhD thesis , Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam, 1976 .

24. J. van Benthem. Modal Logic and Classical Logic . Bibliopolis, Naples, 1983 .

25. J. van Benthem. Correspondence theory . In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic , Volume II , pages 167 { 247 . Reidel , Dordrecht, 1984 .

{ Consider the condition (12') and the case Self 2 . Suppose Z(x; x0) holds. Thus, (9r:Self)I (x) holds i (9r:Self)I0 (x0) holds. That is, rI (x; x) holds i rI0 (x0; x0) holds .

{ Consider the condition (8) and the case Q 2 . Suppose Z(x; x0) holds, i .e., x sp x0 . Let S = fy 2 I j rI (x; y)g and S0 = fy0 2 I0 j rI0 (x0; y0)g. Since I and I0 are nitely branching, S and S0 must be nite. As shown in the proof of Theorem 4.6, there exists a bijection h : S ! S0 such that, if h(y) = y0 then y sp y0 . Analogously, there exists a bijection h0 : S0 ! S such that, if h0(y0) = y then y0 sp y. Therefore, there must exist a bijection h2 : S ! S0 such that, if h2(y) = y0 then y sp y0 .

{ The condition (9) can be proved analogously as for the condition (8).

{ The conditions (3) and (4) follow from the condition (8).

{ The conditions (5) and (6) follow from the condition (9).

{ Consider the conditions (10) and (11) and the case U 2 . By assumption, both I and I0 are unreachable-objects-free. The condition (10) follows from the conditions (1), (3) and (4). Analogously, the condition (11) also holds .