Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees

1 Introduction

Description Logics (DLs) allow one to represent a domain of interest in terms of concepts and roles, where concepts model classes of individuals, and roles model relationships between classes [Woods and Schmolze, 1992; Donini et al., 1996; Borgida and Patei-Schneider, 1994]. A knowledge base ex­ pressed in a DL is constituted by inclusion assertions that state the properties of concepts and roles. Various reason­ ing tasks can be carried out on a k; 1wledge base. The most fundamental one consists in checking whether a certain asser­ tion is logically implied by a knowledge base. A DL is char­ acterized by three aspects: the language used to form com­ plex concepts and roles, the kind of assertions that are used to express properties of concepts and roles, and the inference mechanisms provided for reasoning on the knowledge bases expressible in the system.

In the last years, the investigation on DLs has been driven by the goal of applying them in several areas, such as plan­ ning [Weida and Litman, 1992], action representation [Ar­ tale and Franconi, 1994], software engineering [Devanbu and Jones, 1997], information systems [Catarci and Lenzerini, 1993], databases [Borgida, 1995; Bergamaschi and Sartori, 1992; Sheth et al., 1993], information integration [Calvanese et al., 1998c], and intelligent access to the web [Levy et al., 1996; Blanco et al., 1994]. The modeling requirements aris­ ing in the above areas have stimulated the need for incorpo­ rating increasingly expressive representation mechanisms:

• The goal of capturing the semantics of database mod­ els and reasoning about data schemas has stressed the importance of number restrictions, n-ary relations, and cyclic assertions in the knowledge base [Calvanese et al., 1994].
• Information integration systems require inclusion asser­ tions not only on concepts, but also on relations [Ullman, 1997].
• Semi-structured data, used in applications such as digital libraries, internet information systems, etc., require the ability to represent data whose structure is not rigid and strictly typed as in conventional database systems. Mod­ els for semi-structured data represent data as graphs with labeled edges, and adopt flexible typing schemes in or­ der to classify data [Buneman, 1997]. A special case of such models is XML [Bray et al., 1998], which is be­ coming the standard for exchanging data on the web. In general, correctly modeling such typing schemes calls for the use of fixpoints in the representation formali sm [Cal vanese et al., 1998b].
• UML [Booch et al., 1998] is nowadays the standard lan­ guage for the analysis phase of software and information system development. CASE tools that perform auto­ mated reasoning on UML schemas (for example, to test consistency or redundancy) would be of great interest. Fully capturing UML schemas in DLs requires inverse roles, n-ary relations, number restrictions, and general fixpoints on concepts for modeling recursive structures (both inductive and coinductive), such as lists, trees, streams, etc ..

DLs that capture all requirements above except fixpoints are known (see e.g. [Calvanese et al., 1998c]). However, fully capturing fixpoints in DLs has been an open problem for a long time. Fixpoints incorporated directly in the seman­ tics have been first studied in [Nebel , 1991; Baader, 1996] for simple DLs. DLs with regular expressions, which can be seen as a form of fix points, have been studied in [Baader, 1991 ], and exploiting the correspondence with Propositional Dynamic Logics in [Schild, 1991; De Giacomo and Lenz­ erini, 1994]. In [Calvanese et al., 1995] another form of fixpoints, capturing well-foundedness, has been considered. While such logics got increasingly expressive, they all in­ clude fix point of a limited form only. Fix points on concepts in their full generality have been investigated in [Schild, 1994; De Giacomo and Lenzerini, 1997] developing a correspon­ dence with modal 11-calculus [Kozen, 1983]. However these logics lack inverse roles (and number restrictions on them) which are essential to deal with n-ary relations.

The work presented in this paper closes the gap between the two lines of research, presenting a logic with general fix­ points on concepts that includes all the constructs mentioned above. Specifically, we consider a DL, called DLR~-', that includes:

• a very rich language, comprising all classical concept forming constructs, plus inverse roles, n-ary relations, and the most general form of number restrictions;
• the most general form of inclusion assertions, without any limitations on the presence of cycles;
• the most general form of fixpoint on concepts.

We characterize reasoning in such a DL as EXPTIME­ complete1, by presenting a decision procedure based on re­ ducing inference to nonemptiness of two-way alternating au­ tomata on infinite trees [Vardi, 1998]. We observe that this is the first decidability result for a logic combining inverse roles, number restrictions, and general fix points.

2 The Description Logic 1J .CRJ.L

Traditionally, description logics (DLs) allow one to represent a domain of interest in terms of concepts and roles, which model classes of individuals and binary relationships between classes, respectively. More recently DLs comprising relations of arbitrary arity have been introduced, e.g., DLR [Calvanese et al., 1998c]. We present the DL DLR~-' which extends D LR by least and greatest fix point constructs.

We make use of the standard first-order notions of scope, bound and free occurrences of variables closed formulae etc., treating 11 and vas quantifiers. ' '

Concepts and relations (of arity between 2 and nmax) are built according to the following syntax:

where P and A denote atomic relations and atomic concepts respectively, Rand C denote arbitrary relations and concepts, i denotes components of relations, i.e., an integer between 1 and nmax. n denotes the arity of a relation, i.e., an integer between 2 and nmax, k denotes a nonnegative integer, T 1 de­ notes the top concept, T n. for n = 2, ... , nmax. denotes the top relation of arity n, X denotes a concept variable, and the restriction is made that every free occurrence of X in 11X .C is in the scope of an even number of negations ((:S k [$i]R) counts as one negation).

Concepts and relations must be well-typed, which means that (i) only relations of the same arity n can be combined to

1 The same computational complexity of reasoning with inclu­ sion assertions in the basic DL ACC.

Figure 1: Semantic rules for DLR~-'

form expressions of type R1 n Rz (which inherit the arity n), and (ii) i :S n whenever i denotes a component of a relation of arity n.

We make use of the standard abbreviations, including vX.C for ·11X.·G[X/·X], where C[X/C 1 ] denotes the concept obtained from C by substituting all free occurrences of X with C 1 · We use >. to denote either 11 or v.

An interpretation I = (~I, .I) consists of an interpre­ tation domain ~I, and an interpretation function .I, which maps every atomic concept to a subset of !:!J.I, and every atomic relation of arity n to a subset of (~I)n. The presence of free variables does not allow us to extend .I directly to ev­ ery concept and relation. For this reason we introduce valua­ tions. A valuation p on I is a mapping from concept variables to subsets of ~I. Given a valuation p, we denote by p[X/£] the valuation identical top except for p[X/E](X) = £.

Let I be an interpretation and p a valuation on I. We as­ sign meaning to concepts and relations of the logic by associ­ ating to I and p an extension function ·7i, mapping concepts to subsets of~ I and relations of arity n to subsets of ( ~ I)n, as shown in Figure 1. Observe that the semantics assigned to vX.Cis

The expression CJrx;t:] can be seen as an operator from sub­ sets £ of ~I to subsets of ~I, and, by the syntactic restric­ tion enforced on variables, such an operator is guaranteed to be monotonic wrt ~- The constructs 11X.C and vX.C de­ note respectively the least fixpoint and the greatest fixpoint of the operator (see [De Giacomo and Lenzerini, 1997] for a discussion on the use of fixpoints in DLs). The extension of closed concepts and relations is independent of the valu­ ation, and therefore for closed concepts and relations we do not consider the valuation explicitly. A closed concept or re­ lation L is satisfiable if there exists an interpretation I such that LI =J. 0.

A DLRI-' knowledge base is a finite set of assertions of the form L1 ~ Lz where L1 and L2 are either two closed concepts of DLR 11 or two closed relations of the same arity. We use L1 = Lz as an abbreviation for the assertions L1 ~ Lz and Lz ~ L1. An interpretation I satisfies an assertion L1 ~ Lz, if Lf ~ Lf. I is a model of a knowledge base K, if it satisfies all assertions in K. An assertion L1 C L2 is logically implied by a knowledge base K if Lf ~ L1 for every model I of K.

Example 2.1 Figure 2 shows an UML diagram which is part of a Telecom Italia application monitoring departments. De­ partments other than Main Departments are controlled by other departments, in a purely hierarchical fashion (see the use of the concept Tree). Moreover, Departments can be sold to companies for a certain amount of money. There are further constraints in the application (not shown in the diagram): First, if a Main Department is sold, then all De­ partments directly or indirectly controlled by it are also sold. Second, if a Department is sold, then its controlling Main De­ partment is also sold.

We provide the formalization in D £RI-I of the UML dia­ gram in Figure 2. Tree[N, L] represents a concept param­ eterized on N and L, to be used as a template, according to the following inductive definition of tree: (i) an empty tree is a tree; (ii) a node with at most one predecessor, at least one successor, and such that all successors are trees, is a tree; (iii) nothing else is a tree. Tree[Dept, CONTROLS] repre­ sents the concept obtained by syntactically substituting Dept and CONTROLS for the parameters Nand Lin Tree[N, L].

[ def TreeN, L] = JLX.(EmptyTree U (N n (:S 1 ($2]£) n 3($1]£ n ·3($1](£ n ($2/2: ·X)))) Dept Tree = Tree(Dept, CONTROLS] SOLD ~ ($1: Dept) n ($2: Company) n ($3: Money) CONTROLS ~ ($1: Dept) n ($2: Dept) MDept ~ Dept n ·3($2]COl\'mROLS

The additional constraints mentioned above are formalized as follows:

MDept n 3($1]SOLD ~ vX.(3($1]SOLD n ·3($1] (CONTROLS n ($2: ·X))) Dept n 3($1]SOLD ~ JLX.((MDept n 3($1]SOLD) U 3($2](CONTROLS n ($1: X)))

3 The DLs J.LA.CCQ;I and J.LA.CCI1

Below we also consider the DL ~-£A£C QI, which extends ~-£A£C Q, studied in [De Giacomo and Lenzerini, 1997], by the inverse operator on roles. Concepts in f.1-A£C QI are built as follows (R is an atomic or inverse atomic role):

c ::=A 1 x I·C 1 C1 nC2I ::JR.c 1 (::; kR.C) 1 f-£x.c

f-£A£C QI can be viewed as a syntactic variant of modal !-£­ calculus [Kozen, 1983] extended both with graded modalities (see e.g., [Vander Hoek and De Rijke, 1995]) and with back­ ward modalities [Vardi, 1985].

We observe that f-£A£C QI can also be considered as a sub­ language of D£RI-I by restricting relations to be binary and allowing their use only according to the following abbrevia­ tions:

3P.C for 3($1](P n ($2/2: C)) 3P- .C for 3($2](P n ($1/2: C)) (:S k P.C) for (:S k [$1](P n ($2/2: C))) (:S k p- .C) for (:S k [$2](P n ($1/2: C)))

Finally, we call ~-£A£CI 1 the restriction of ~-£A£CQI ob­ tained by forcing all atomic and inverse roles to be functional.

4 Encoding V .CRJ..L into J.LA.CCI1

Next we tum to reasoning in D£Rw In particular, we present a technique to decide logical implication in D£Rw In this section we show how to encode D £RI-I into ~-£A£C QI and then into f.1-A£CIJ. In Section 5 we study reasoning in ~-£A£CI! by adopting automata theoretic techniques.

Since we can define an atomic relation to be equivalent to any complex relation, we assume wlog that all qualified num­ ber restrictions are of the form (::; k [$i]P), where P is an atomic relation. We also use the standard abbreviations.

To reduce logical implication in D£RI-I to logical impli­ cation in f.1-A£CQI we extend the technique in [Calvanese et al., 1998a]. We make use of the mapping a{) defined in Figure 3, and define the f.1-A£CQI knowledge base a:(K) by applying a: to all assertions in K and adding:

L AT1 U···UATnmaz C (::; 1 Fi.T) for each i E {1 , ... , nmax} C V Fi+l ·j_ for each i E {1, ... , nmax} ::JF1.AT, n · · · n ::JFn.AT, n VFn+l·..l for each n E {2, .. . , nmax} C AT n for each atomic relation P of ari ty n C AT 1 for each atomic concept A

Intuitively, a:(K) makes use of reification of n-ary relations, i.e. a tuple in a model of K is represented in a model of a:(K) by an individual having one functional role Fi for each tuple component $i.

Although atomic roles in a:(K) are functional their inverses are not. Next we further transform a:(K) to get a f.1-A£CIJ

where in the second last equation the number of nested con­ cepts of the form · tJ(A) U \:lg{.C is k, and the following ab­ breviations are used: \:lg;.c for vX.(C n \:lg;.X) , \:lg{ .C for \:lg; .\:lg; .c, :Jg; .c for f1X.(C u :Jg;.X), and :J(gj)*.C for f1X.(C u :Jgj .X).

Figure 4: Mapping {3( ·) from J-LA£CQI to J-LA£Cit

knowledge base {3( a(K)) (in which also all inverse roles are functional). Intuitively, following [De Giacomo and Lenz­ erini , 1995], we represent the role F;-, i = 1, ... , nmax· by the role j ; o gi, where j ;, gi are new functional roles and gi is the reflexive-transitive closure of g; . Now qualified num­ ber restrictions can be encoded as constraints on the chain j; o gi. Formally, we make use of the mapping {3( ·) defined in Figure 4.

We define {J(a(K)) as the J-LA£Cit knowledge base ob­ tained by applying {3 to all assertions in a(K) and adding the assertion T ~ -{3!;- . T n 3gi. T) .

Theorem 4.1 Given a 1J £Rp. knowledge base K and a 1J £Rp. assertion L1 ~ L2,

Since the mappings a and {3 are polynomial we get the (ollowing result.

Theorem 4.2 Logical implication in 1J£Rp. can be polyno­ mially reduced to logical implication in 11A£Cit. 2

Finally we observe, that since J-LA£Cit has the connected­ model property, we can internalize assertions and polyno­ mially reduce logical implication to concept satisfiability. Namely, K F cl ~ c2 iff

is unsatisfiable, where CK = n [Ci;;;C'EK] ( ·C U C') and P1, ... , Pq are the atomic roles inK, C1 and C2. Therefore, in the following we concentrate on concept satisfiability in J-LA£Cit.

5 Automata Techniques for J.LA.CCI!

We now study concept satisfiability in 11A£CI1 following the techniques based on two-way alternating automata on infinite trees (TWAA) introduced in [Vardi, 1998]. Indeed, Vardi used TWAAs to derive a decision procedure for modal J-L-Calculus with backward modalities. Here we exploit them to derive a reasoning procedure for J-LA£Cit, which corre­ sponds to a modal J-L-Ca1culus with backward modalities in which both forward and backward modalities are functional.

2 Under the usual assumption that numbers in number restrictions are coded in unary.

5.1 Automata on Infinite Trees

Infinite trees are represented as prefix closed (infinite) sets of words over N (the set of positive natural numbers). Formally, an infinite tree is a set of words T ~ N*, such that if x·c E T, where x E N* and c E N, then also x E T . The tree is full if also x ·c' E T for all 0 < c' < c. The elements ofT are called nodes, the empty word c: is the root ofT, and for every x E T , the nodes x·c, with c E N, are the successors of x. By convention we take x·O = x, and x·i·-1 = x. The branching degree d(x) denotes the number of successors of x. If d(x) = k for all nodes x, then we say that the tree is k­ ary. An infinite path P ofT is a prefix-closed set P ~ T such that for every i 2 0 there exists a unique node x E P with JxJ = i . A labeled tree over an alphabet~ is a pair (T, V) where T is a tree and V : T -7 ~.

Alternating automata on infinite trees are a generalization of nondetermi!listic automata on infinite trees, introduced in [Muller and Schupp, 1987]. They allow for an elegant re­ duction of decision problems for temporal and program log­ ics [Emerson and Jut1a, 1991; Bernholtz et al., 1994]. Let [3+ (I) be the set of positive boolean formulas over I, includ­ ing also true and false. For a set J ~ I and a formula cp E [3+ (I) , we say that J satisfies cp iff assigning true to the elements in J and false to those in I \ J makes cp true. Let (k] = { -1, 0, 1, ... , k }. A two-way alternating automa­ ton over infinite k-ary trees is a tuple A= (~,Q,o,qo,F), where ~ is the input alphabet, Q is a finite set of states, 8 : Q x ~ -7 f3+( [k] x Q) is the transition function, qo E Q is the initial state, and F specifies the acceptance condition.

The transition function maps a state q E Q and an input letter a E ~to a positive boolean formula over (k] x Q. In­ tuitively, if o(q,a) = cp, then each pair (c,q') appearing in cp corresponds to a new copy of the automaton going to the direction suggested by c and starting in state q'. For example, if k = 2 and o(q1, a)= (1, q2) 1\ (1, q3) V ( -1, q1) 1\ (O, q3), when the automaton is in the state q1 and is reading the node x labeled by the letter a , it proceeds either by sending off two copies, in the states q2 and q3 respectively, to the first succes­ sor of x (i.e., x·1), or by sending off one copy in the state Q1 to the predecessor of x (i.e., x·-1) and one copy in the state q3 to x itself (i.e., x·O) .

A run of a TWAA A over a labeled tree (T, V) is a labeled tree (Tr, r) in which every node is labeled by an element of T x Q. A node in Tr labeled by (x, q) describes a copy of A that is in the state q and reads the node x ofT. The labels of adjacent nodes have to satisfy the transition function of A. Formally, a run (Tr , r) is aT x Q-labeled tree satisfying:

1. Let y E Tr , with r(y) = (x, q) and o(q, V(x)) cp. Then there is a (possibly empty) set S {(cl ,Ql), ... ,(cn,qn)} ~ (k] x Qsuchthat:
2. S satisfies cp and
3. for all 1 < i < n, we have that y ·i E Tr, x·c; is defined, and r(Y·i) = (x·c;, Qi).

A run (Tr. r) is accepting if all its infinite paths satisfy the acceptance condition. Given an infinite path P ~ Tr, let in/ (P) ~ Q be the set of states that appear infinitely often in P (as second components of node labels). We consider here parity acceptance conditions. A parity condition over a state set Q is a finite sequence F = ( G1 , ... , Gm) with G1 . ~ G2 ~ · · · ~ Gm = Q, and a path P satisfies F if there is an even i for which inf(P) n Gi =1- 0 and inf(P) n Gi-l = 0.

5.2 Reasoning in /-lA£Cit

First we observe that J-LA£C'IJ has the tree model property, which states that if a J-LA£C'IJ concept C is satisfiable then it is satisfied in an interpretation which has the structure of an infinite tree of bounded degree. In particular, the degree is bounded by 2 · n, where n is the number of atomic roles appearing in C. The tree model property can be shown fol­ lowing the lines of the proof in [Vardi, 1998] for the modal J-L­ calculus with backward modalities. Next we define a TWAA that accepts exactly the trees that are models of a concept.

The closure cl(C) of a J-LA£C'IJ concept C (which extends the one in [Kozen, 1983] for the modal J-L-calculus) is defined as the smallest set cl (C) of closed concepts that satisfies:

C E cl(C) C' E cl( C) implies -,C' E cl( C) (we identify -,-,C and C) C1 n C2, C1 U C2 E cl(C) implies C1 E cl(C) and C2 E cl(C) 3R.C', 'r/ R.C' E cl (C) implies C' E cl (C) >.X.C' E cl(C) implies C'[X/ >.X.C'] E cl(C)

Note that the cardinality of cl( C) is linear in the length of C.

Let C be the J-LA£CI 1 concept we want to check for satisfi­ ability, which wlog we assume to be in negation normal form. Let A be the set of atomic concepts, and P = { P1 , .. . , Pn} the set of atomic roles appearing in C. We construct from C a TWAA Ac which checks that C is satisfied at the root of the input tree. For technical reasons it is useful to con­ sider trees where all nodes have the same branching degree 2n. To this end we introduce dummy nodes in the tree. We use the symbols A 9 and -,A 9 to distinguish nodes that corre­ spond to elements of the model from those that do not. We also represent in the nodes of the tree the information about the labeling of the edges by introducing for each role Pi four symbols Ai, 'Ai, Ai, and -,Ai. Intuitively, Ai labels x·i if (x, x·i) E Pl and 'Ai labels x·i if not. Similarly Ai labels x·i if ( x·i, x) E Pl and -,Ai labels x·i if not.

Since all roles (both direct and inverse) are deterministic, we can assume that for each node x, each Pi and each pi­ successor appears in a fixed position. In particular, x·i is labeled with Ai and x·(i+n) is labeled with Ai. Let det and ini be two new symbols, and Aaux = { A 9 , -,A 9 } U U7= 1 { Ai, 'Ai, Ai, -,Ai} U { det }.

The automaton Ac = (I:, S, o, ini, F), where I: = 2AuA ·· , , S = cl (C) U Aaux U { ini , det } , the acceptance condition F is as in [Vardi, 1998] and the transition function 0 is defined as follows. For all a E I:: for all A E AU Aaux we have o(A, a) =true if A E a, o(A, a) =false if A rf_ a ,

J(-,A, a)= true if A rf_ a, J(-,A, a) =false if A E a, and 8( C1 n C2 , a )=(0, CI) 1\ (0, C2) 8(C1 u C2 , a)=(O, C1) V (0, C2) 8(>.X.C1 , a)=(O, C[X/ >.X.C!]) 8(3P;.C1 , a)=((-1,C1) 1\ (O,Ai)) V ((i,A 9 ) 1\ (i,C1)) 8(3P;-.C1, a)=((-1,CI) 1\ (O,A;)) v ((i+n,A 9 ) 1\ (i+n,C!)) 8(\1 ?;.C1, a)=( ( -1, CI) v (0, -,Ai)) 1\ ( (i, -,A 9 ) v (i, C!)) 8(\/ P;- .C1, a)=( ( -1, C1) V (0, -,A;)) 1\ ( ( i+n, -,A 9 ) V (i+n, C1) 8(det, a)=/\~2 1 (i, det) 1\ /\~ 1 ((i, -,A 9 ) V (i, A; ) 1\ (i+n, -,A 9 ) V (i+n, Ai)) 1\ /\~= 1 ((0, -,A; ) V (n+i , -,A 9 ) 1\ (0, -,Ai) V (i, -,A 9 )) 8(ini, a)=(O, det) 1\ (0, C)

Intuitively, the automaton starts in the initial state ini and spawns two copies of itself: one verifies that the tree has the right structure wrt functionality, and one checks C on such structure.

Theorem 5.1 A J-LA£C'IJ concept C is satisfiable iff the set of trees accepted by Ac in not empty.

Since nonemptiness of TWAA can be decided in EXP­ TIME [Vardi, 1998] we get the following upper bound.

Corollary 5.2 Concept satis.fiability in J-LA£CI 1 can be de­ cided in EXPTIME.

Since the reduction in the previous section is polynomial, we get a worst case deterministic exponential time decision procedure for logical implication in V£Rw Moreover, since logical implication in V£R~' is EXPTIME-hard (it is so al­ ready for A£C) we get the following tight complexity bound.

Theorem 5.3 Logical implication in V£R~' is EXPTIME­ complete.

6 Conclusions

By addressing general fixpoints on concepts, in addition to more standard constructs, DLs finally meet the modeling re­ quirements of advanced applications. The EXPTIME reason­ ing procedure for V£R~' is the first decidability result for a logic combining inverse roles, number restrictions, and gen­ eral fixpoints. In particular, since modal J-L-calculus extended both with graded and backward modalities corresponds to J-LA£CQI, the result here applies to such logic as well.

We observe that reasoning in the presence of extensional information (ABox) remains an open problem for V £R~' .