Multi-Dimensional Description Logics

1 Introduction

Description logics are often characterized as logic-based formalisms intended for representing knowledge about concept hierarchies and supplied with effective reason­ ing procedures and a Tarski-style declarative semantics. A standard example is the description logic A.CC (see [Schmidt-Schauf3 and Smolka, 1991]) in the syntax of which the "definition" above can be represented as fol­ lows:

Description_logic = KnowledgeJepresentation_language 1\ Logic 1\ :Jis_decided_by.Aigorithm 1\ :Jhas.Tarski...semantics, A.CC : Description_logic

(here Description _logic, K nowledge_representation _Ia ngu­ age, Logic, Algorithm, Tarski...semantics are concept names (unary predicates) , is_decided_by and has are role names

Michael Zakharyaschev

Institute of Applied Mathematics Russian Academy of Sciences Miusskaya Square 4

125047 Moscow, Russia

e-mail: mz@spp.keldysh.ru

(binary predicates) and A.CC is an object name (individ­ ual constant)).

Created in the 1980s as a direct successor of semantic networks and Minsky frames , description logic has found numerous applications and given rise to a rich family of languages (see e.g. [Brachman and Schmolze, 1985; Donini et al., 1996]). But as the application areas are be­ coming more and more sophisticated, new, more expres­ sive description logics are being called for. Sometimes it is possible to comply with the application demands by enriching a "standard" description language with new constructs and retaining basically the same semantical paradigm. E.g., De Giacomo and Lenzerini [1996] ex­ tend A.CC by providing means to form the union, com­ position, inversion, transitive reflexive closure of roles and to use the number restrictions for quantification over roles; Baader and Hanschke [1991] add concrete domains to A.CC. However, some constructs require more drastic changes in the standard semantics. This happens, for instance, when one has to take into account various dy­ namic aspects of knowledge representation, say time- or agent-dependence of knowledge like

Received = Mail 1\ (sometime in the past):Jis_in.Mailbox,

John: :J[always]loves.Woman , [John believes](eventually)(31oves.T = T) ,

i.e., a received mail has been put into the mailbox some time ago, John will always love the same woman, and John believes that sometime in the future everybody will love somebody.

Several approaches to the design of "dynamic" de­ scription logics were developed in the 1990s (see e.g. [Schmiedel, 1990; Schild, 1993; Baader and Ohlbach, 1995; Baader and Laux, 1995; Donini et al., 1992; Wolter and Zakharyaschev, 1998a; 1998b; 1998c]) , and all of them share one important feature: their models become multi-dimensional in the sense that besides the usual "object dimension" they may contain a time axis, possible worlds or states for beliefs or actions, etc.

Perhaps the most general multi-dimensional perspec­ tive was proposed by Baader and Ohlbach [1993; 1995]. Roughly, each dimension (object, time, belief, etc.) is represented by a set D; (of objects, moments of time, possible worlds, etc.), concepts are interpreted as sub­ sets of the Cartesian product f1~=1 Di and roles of di­ mension i as binary relations between n-tuples that may differ only in the ith coordinate. And one can quantify over roles not only concepts, but also roles themselves and concept equations. However, the constructed lan­ guage turned out to be too expressive. At least no sound and complete reasoning procedure for it has appeared (Baader and Ohlbach provide only a sound satisfiability algorithm for a restricted fragment of their language). Moreover, under the natural assumption that some di­ mensions may be "independent" the language becomes undecidable. 1

Trying to simplify this semantics, Baader and Laux [1995] noticed that different dimensions may have a dif­ ferent status. For instance, time should probably be the same for all objects inhabiting the object dimension of our knowledge base. This observation led to a some­ what more transparent semantics: models now consist of worlds (or states) which represent-in terms of some standard description logic-the "current state of affairs"; these worlds may change with time passing by or under certain actions, or they may have a number of alternative worlds reflecting the beliefs of agents, and the connec­ tion between concepts and roles from different worlds is described by means of the corresponding temporal, dy­ namic, epistemic, or some other "modal" operators.

There are several "degrees of freedom" within this se­ mantical paradigm.

1. The worlds in models may have arbitrary, or ex­ panding (with respect to the accessibility relation be­ tween worlds), or constant domains. Of course, the choice depends on the application we deal with. How­ ever , from the technical point of view the most impor­ tant is the constant domain assumption: as was shown in [Wolter and Zakharyaschev, 1998b), if the satisfaction problem is decidable in models with constant domains then it is decidable in models with varying or expanding domains as well. This is the reason why in this paper we adopt the constant domain assumption.

2. The concept, role and ·object names of the under­ lying description language may be local or global. Global names have the same extensions in all worlds, while lo­ cal ones may have different extensions. (For example, an agent A may regard the role loves to be local, while the role believes to be global.) In principle, we may need both kinds of names. However technically, local object names present no difficulty as compared with global ones, and global concepts are expressible via local concepts and the modal operators.

3. As we saw above, in general one may need modal operators applicable to concepts, roles and formulas.

And finally, depending on the application domain we may choose between various kinds of modal operators (e.g. temporal, epistemic, action, etc.), the correspond­ ing accessibility relations (say, linear for time, universal for knowledge, arbitrary for actions), and between the underlying pure description logics.

1 Franz Baader has kindly informed us that the language is undecidable without this assumption as well.

The main objective of this paper is to analyze anum­ ber of basic multi-dimensional modal description logics based on A.CC and having the most expressive combina­ tion of the listed parameters. In particular, we show that the satisfaction problem (and so many other reasoning problems as well) for the logics with modal operators applicable to arbitrary concepts, (local and global) roles and formulas is decidable in the class of all (multi-modal) frames, in the class of universal frames (corresponding to the modality "agent A knows") and in the class of tran­ sitive, symmetrical and euclidean frames (corresponding to the modality "agent A believes").

Multi-dimensional modal description logics of such a great expressive power have never been considered in the literature. Languages with modal operators appli­ cable only to axioms were studied by Finger and Gab­ bay [1992] and Laux [1994]; Schild [1993] allows appli­ cations of temporal operators only to concepts. Baader and Laux [1995] prove the decidability of the satisfac­ tion problem for A.CC extended with modal operators applicable to concepts and axioms, but only in the class of arbitrary frames and under the expanding domain assumption. Wolter and Zakharyaschev [1998a; 1998b; 1998c] have obtained a series of decidability results for the most important epistemic, temporal and dynamic description logics (based on the description logic CIQ of [De Giacomo and Lenzerini, 1996]) under the constant domain assumption and with modal operators applicable to both concept and formulas.

However, the computational behaviour of the modal­ ized roles (i.e., binary predicates) has remained unclear. It should be emphasized that this problem is not of only technical interest. Modalized roles are really required for expressing the dynamic features of roles while pass­ ing from one state to another (which is usually much more difficult than to reflect the dynamic behaviour of concepts). For instance, to describe the class of people always voting for the same party we can use the axiom

FaithfuLvoter =Voter 1\ 3[always]votes.Party.

(By swapping 3 and [always] we get the class of people always voting for some party.)

The price we have to pay for this extra expressive power is that only a limited number of logics in this language enjoy decidability. We show, for instance, that the satisfaction problem in linear frames or in universal frames with the common knowledge operator for n 2: 2 agents is undecidable (but it becomes decidable if the language contains neither global nor modalized roles).

To simplify presentation, we will be considering first description logics with only one modal operator and then generalize the obtained results to systems of multi­ modal description logic. A full version of the paper is at http:/ fwww .informatik.uni-leipzig.de/ "'Wolter.

2 The language and its models

The primitive symbols of the modal description language A£C M we deal with in this paper are: concept names Co, C1 , ... , role names Ro, R1, ... , and object names ao, a1, . . . . Starting from these we construct compound concepts and roles in the following way. Let R be a role, C, D concepts, and let D and<> be the (dual) modal "ne­ cessity" and "possibility" operators, respectively. Then <>R, DR are roles, and T, C 1\ D, ·C, <>C, 3R.C are concepts. Atomic formulas are expressions of the form T, C = D, aRb, a: C, where a, bare object names. If cp and '1/J are formulas then so are Ocp, ·cp, and cp 1\ '1/J.

The intended semantics of A£C M is a natural com­ bination of the standard Tarski-type semantics for the description part of A£C M and the Kripke-type (possi­ ble world) semantics for the modal part.

Definition 1 (model). An A£CM-model based on a frame IB = (W, <1) 2 is a pair 911 = (IB, I) in which I is a function associating with each wE W an A£C-model

where 6. is a non-empty set, the domain of 911, R{'w are binary relations on 6., c{'w ~ 6., and a{'w are objects in 6. such that a{'" = a{'v, for any u,v E W. The values ci,w, RI ,w of a concept C and a role R in a world w E W, and the truth-relation (911, w) f= cp (or simply w f= cp) are defined inductively as follows:

A formula cp is satisfiable if there is a model 911 and a world w in 911 such that w f= cp.

Since many reasoning tasks are reducible to the sat­ isfaction problem for formulas (see e.g. [Donini et al., 1996] and [Wolter and Zakharyaschev, 1998b]), in this paper we focus attention only on the latter. Our first aim is to show that the satisfaction problem is decidable in the class of all A£CM-models.

By the modal depth md( cp) of a formula cp we inean the length of the longest chain of nested modal operators in cp (including those in the concepts and roles occurring in cp). It is well known from modal logic (see e.g. [Chagrov and Zakharyaschev, 1997]) that every satisfiable purely modal formula cp can be satisfied in a finite intransitive tree of depth :::; md( cp). We remind the reader that a frame IB = (W, <l) is called a tree if (i) IB is rooted, i.e. , there is wo E W (a root of IB) such that w0 <J · w for every w E W, where <l* is the transitive and reflexive closure of <l, and (ii) for every w E W, the set { v E W : v <l* w} is finite and linearly ordered by <l*. The depth of a tree is the length of its longest branch. And by the co­ depth of w we mean the number of worlds in the chain { v E W : v <l* w}. A tree IB is intransitive if every world v in IB, save its root, has precisely one predecessor, i.e., I { u E W : u <l v} I = 1, and the root wo is irreflexive, i.e. , ·Wo <l w0 . Using the standard technique of modal logic one can prove the following lemma.

2 W is a non-empty set of worlds and <J a binary accessi­ bility relation on W .

Lemma 2. Every satisfiable formula is satisfied in a model based on an intransitive tree of depth :::; md( cp) (but possibly with infinitely many branches).

3 Quasimodels

Fix an A£CM-formula cp . Let obcp be the set of all object names in cp, and by concp, rolcp and subcp we denote the sets of all concepts, roles, and subformulas occurring in cp, respectively.

In general, A£CM-models are rather complex struc­ tures with rich interactions between worlds, concepts and roles. That is why standard methods of establishing de­ cidability (say, filtration) do not go through for them. Our idea is to factorize the models modulo cp in such a way that the resulting structures- we will call them quasimodels-can be constructed from a finite number of relatively small finite pieces called blocks.

Definition 3 (types). A concept type for cp is a subset t of concp such that

• C 1\ D E t iff C, D E t, for every C 1\ D E concp;
• ·C E tiff C ¢ t, for every ·C E concp.

A named concept type is the pair ta = (t, a), where tis a concept type and a E obcp. A formula type and a named formula type for cp are defined analogously as saturated subsets of subcp. Finally, by a type for cp we mean the pair 7 = ( t, 3), where t is a concept type and 3 a formula type for cp; 7a = (ta, 2a) is a named type for cp.

To simplify notation we write C E 7 and '1/J E 7 when­ ever 7 = (t, 3), C E t and '1/J E 3. Two types 71 = (t1 , 31) and 72 = (t2, 32) are formula-equivalent if 3 1 = 22 .

Let 911 = (IB, I) be a model over 6. and IB = (W, <!) an intransitive tree of depth :::; md( cp). Without loss of generality we may assume also that obcp ~ 6. (and a{'w = ai). For every pair x E 6., wE W, let 7(x,w) = (t(x, w), 3(w)), where

Clearly, T(x , w) is a type for cp. The set of (labelled) types T(x ,w), wE W, with the relation <x defined by T(x, u) <x T(x, v) iff u <I v is a tree isomorphic to <B. But modulo cp only a finite part of this tree is enough to represent all the essential information it contains.

Definition 4 (type tree). By a type tree for cp we mean a structure of the form 'I" = (T, <), where T is a finite set of labelled types for cp (so that one type may have many occurrences in T) and < an intransitive tree order on T such that

• (a) for all T E T and OC .E cancp, we have OC E T iff 3T 1 > T c E T 1 j
• (b) for all T E T and 0'1/J E subcp, we have 0'1/J E T iff 3T 1 > T '1/J E T 1 j
• (c) 'I" is of depth ~ md(cp);
• (d) if T < T 1 , T < T 11 and T 1 -=f. T 11 then the subtrees of 'I" generated by T 1 and T 11 are not isomorphic.

It should be clear that there exist at most N d ( cp) pair­ wise non-isomorphic type trees of depth d, where

So the number of types in each type tree for cp does not exceed U(cp) = (Nmd('P)(cp))md(<p).

Definition 5 (type forest). A type forest of depth d over ~ is a set 3' = {'I"x : x E ~}, where all 'rx = (Tx, <x) are type trees for cp of the same depth d and 'I" a, for every a E ~ n obcp, consists of only named types of the form Ta ·

To represent worlds in models with their inner com­ plex structure we require the following definition.

Definition 6 (run). A run of co-depth d through a type forest 3' over ~ is a pair of the form

in which ~r contains precisely one type r(x) E Tx of co­ depth d for every x E ~(so that ~r = {r(x) : x E ~}) and Rr s;; ~r X ~r such that:

• (e) all types in ~rare formula-equivalent to each other;
• (f) 3R.C E r(x) iff 3y E ~ (r(x)Rrr(y) & C E r(y)), for every 3R.C E cancp;
• (g) C = D E r(x) iff Vy E ~ (C E r(y) ¢:> D E r(y)), for every C = D E subcp;
• (h) a : C E r(x) iff C E r(a), for every a : C E subcp provided that a E ~;
• (i) aRb E r(x) iff r(a)Rrr(b) , for every aRb E subcp provided that a, b E ~.

If only the (¢=)-part of (f) holds, we call r a weak run of co-depth d. And if a weak run r satisfies (f) for some particular x in ~' then r is called a weak x-saturated run of co-depth d. Instead of 'ljJ E r(x) we will writer f= '1/J.

Models as a whole are represented in the form of quasi­ models.

Definition 7 ( quasimodel). A triple m = (3', !R, <1) is called a quasimodel for cp if 3' is a type forest of depth m ~ md(cp) for cp over some ~ 2 obcp, !R a set of runs through 3' and <1 is an intransitive tree order on !R such that the following conditions hold:

• (j) for every d ~ m, the set rytd of runs of co-depth din !R is non-empty;
• (k) for any r,r' E !R, if r <I r' then r(x) <x r'(x) for all X E ~;
• for all r E rytd, x E ~'and T E Tx, if r(x) <x T then there is r' E rytd+l such that r' ( x) = T and r <1 r';
• (m) for all x,y E ~' d ~ m, ORE rolcp, andrE !Jtd , we have r(x)(OR)rr(y) iff 3r' t> r r'(x)Rr'r'(y);
• (n) for all x, y E ~' d ~ m, DR E rolcp, andrE rytd, we have r(x)(DR)rr(y) iff Vr' [> r r'(x)Rr'r'(y).

We say m satisfies cp if r f= cp for some r E !R.

To reconstruct the model 9J1 = (<B, I) factorized in a quasimodel m = (3', !R, <1) over domain ~' one can take <B = (W, <1), W = U !.R, and put xR{'r y iff r(x)(Ri)rr(y), C I,r ·ff C E ( ) I,r _ x E i 1 i r x , ai - ai,

Thus we obtain:

Theorem 8. A formula cp is satisfiable iff cp is satisfied in some quasimodel for cp.

Let m = (3', !R, <1) be a quasimodel over ~' x E ~' R E rolcp and let R = MRi for some (possibly empty) string M of 0 and D, Ri a role name. Consider 'I"x = (Tx, <x) as a usual Kripke frame. If ('rx, r(x)) f= M..l., r E !R, then we say that R is r-universal. This name is explained by the fact that if R is r-universal then we have Rr = D.r x D.r, which can be easily established by induction on the length of M. Using the standard unravelling technique of modal logic (see e.g. [Chagrov and Zakharyaschev, 1997]) one can prove

Lemma 9. Every satisfiable cp is satisfied in a quasi­ model (3', !R, <1) for cp in which the set of pairs (x, y) such that x,y ~ obcp and r(x)Rrr(y) for some R that is not r-universal, r E !R, is an intransitive forest order on the set of objects involved in this relation.

4 Satisfiability checking

We are in a position now to show that a formula cp is sat­ isfiable iff one can construct a (possibly infinite) quasi­ model satisfying cp out of a finite set of finite pattern blocks.

Definition 10 (block). Let 3' be a type forest for cp of depth m ~ md( cp) over a finite D. which is disjoint from obcp, x an object in D., !R a set of weak x-saturated runs through 3' such that the set of pairs (x, y) with r(x)Rrr(y) for some R that is not r-universal , r E !R, is an intransitive tree order on ~ with root x , and let <I be an intransitive tree order on !R. We say (3', !R, <1) is a 'I"x-block for cp if it satisfies conditions (j)- (n) .

Definition 11 (kernel block). A kernel block over ob<p =f. 0 is a structure of the form (J, 91, <J) in which J is a type forest over ob<p of depth m :::; md( <p) (it con­ tains only type trees named by the elements of ob<p), 91 a set of weak runs through J and <J an intransitive tree order on 91 satisfying (j)-(n).

Definition 12 (satisfying set). A set of blocks S for <p is called a satisfying set for <p if

• ( o) S contains one kernel block for <p whenever ob<p =f. 0;
• (p) in every block (J, 91, <J) E S there is r E 91 such that r I= <p;
• (q) for every (J,91, <J) inS and every 'I., E J, there is precisely one 'I.,-block in S.

Theorem 13. A formula <p is satisfiable iff there is a satisfying set for <p the domain of each (non-kernel) block in which contains at most U(<p) ·lcon<pl· (md(<p) + 1) + 1 objects.

As an immediate consequence we obtain:

Theorem 14. The satisfaction problem for A.CCM­ formulas is decidable.

So far we were considering satisfiability in arbitrary A.CCM-models. However, various specializations of the modal operators may impose different restrictions on the structure of underlying frames in our models. For in­ stance, if we understand 0 as "it is known", we may need frames that are transitive, reflexive and symmetri­ cal, i.e., S5-frames in the modal logic terminology, and if 0 is intended to stand for "it is believed", then we may need KD45-frames which have the form of an S5-frame possibly with one irreflexive predecessor.

It is not hard to adopt the developed technique to prove the following:

Theorem 15. There is an algorithm which is capable of deciding, given an arbitrary A.CCM-formula <p, whether <p is satisfiable in an A.CC M -model based upon (i) an S5-frame or (ii) a KD45-frame.

In some applications we may need A.CCM-models with global roles, i.e., roles R which are interpreted by the same binary relation in every world of a model. In quasi­ models, we can reflect this by requiring that r(x)Rrr(y) implies r' ( x) Rr' r' (y) for all x, y E .6., r, r' E 91; in other words, global roles correspond to binary relations be­ tween type trees. By a straightforward modification of the proof of Theorem 14 one can show the following:

Theorem 16. There is an algorithm which is capable of deciding, given an arbitrary A.CC M -formula <p with global roles, whether <p is satisfiable in an A.CC M -model based upon (i) an arbitrary frame, (ii) an S5-frame or (iii) a KD45-frame.

When dealing with intensional knowledge, one usually needs one modal operator Oi for each agent ~ (mean­ ing that "agent i knows" or "agent i believes"); see e.g. [Fagin et al., 1995] for a discussion of propositional mul­ timodal epistemic logics. Let A.CC Mn denote the modal description language with n modal operators, so that A.CC Mn -models are based on Kripke frames with n ac­ cessibility relations <J 1 , ... , <ln. These frames are called n-frames. S5n-frames and KD45n-frames are those n­ frames all monomodal fragments of which are S5-frames and KD45-frames, respectively. The developed tech­ nique provides a satisfiability checking algorithm for this multimodal case as well.

Theorem 17. For every n 2: 1, there is an algorithm which is capable of deciding, for an arbitrary A.CCMn­ formula <p with global roles, whether <p is satisfiable in an A.CCMn -model based upon (i) an arbitrary n-frame, (ii) an S5n -frame or (iii) a KD45n -frame.

It would also be of interest to extend the constructed epistemic description language A.CC Mn with the com­ mon knowledge operator C which is interpreted by the transitive and reflexive closure of the union <J 1 U . .. U <ln. (For various applications of C in the analysis of multi­ agent systems see [Fagin et al., 1995].) Another im­ portant kind of modality often used in applications is the temporal operator "always in the future" (or the operators "Since" and "Until") interpreted in lin­ early ordered sets of worlds (see e.g. [Gabbay et al., 1994]). The satisfaction problem for these languages without global and modalized roles is known to be de­ cidable (see [Wolter and Zakharyaschev, 1998a; 1998b; 1998c]). However, this is not the case for the language constructed in this paper:

Theorem 18. (i) The satisfaction problem for A.CCM­ formulas in linearly ordered transitive frames is undecid­ able; it is undecidable in (N, <) as well.

(ii) The satisfaction problem for the epistemic descrip­ tion formulas with n 2: 2 agents and the common knowl­ edge operator is undecidable in the class of S5n -frames.

5 Discussion and open problems

This paper makes one more step in the study of con­ cept description languages of high expressive power that are located near the boarder between decidable and un­ decidable. We have designed a "full" multidimensional modal description language which imposes no restric­ tions whatsoever on the use of modal operators (they can be applied to all types of syntactic terms: concepts, roles and formulas) and contains both local and global object, concept and role names. Using the mosaic tech­ nique we have proved that the satisfaction problem for the formulas of this language (and so many other reason­ ing tasks as well) is decidable in some important classes of models. On the other hand, it was shown that the lan­ guage becomes undecidable when interpreted on tempo­ ral structures or augmented with the common knowledge operator.

The obtained results demonstrate a principle possi­ bility of using this highly expressive language in knowl­ edge representation systems. Further investigations are required to make it really applicable. In particular, it would be of interest to answer the following questions:

1. Do the logics considered above have the finite model property?

Our conjecture is that they do have this property, and so the finite model reasoning in those logics is effective.

1. What is the complexity of satisfiability checking in these logics?

We only know that the satisfaction problem in all of them is NEXPTIME-hard.

To increase the language's capacity of expressing the dynamics of relations between individual objects in ap­ plication domains it would be desirable also

1. to extend A.CCMn with (some of) the booleans op­ erating on roles,
2. to extend the underlying description logic with new constructs

and, of course, retain decidability.

Acknowledgements

The work of the second author was supported by U.K. EPSRC grant no. GR/M36748.