On the Undecidability of Description and Dynamic Logics with Recursion and Counting

1 Introduction

Description logics are popular knowledge representation lan­ guages, with important applications to the semantic web, soft­ ware engineering and heterogeneous databases. Description logics (DLs) are strictly related to propositional dynamic log­ ics (PDLs), that play an important role in software and pro­ tocol verification based on automated reasoning techniques. The analogies between the two frameworks are so tight that DLs and PDLs can be regarded as syntactic variants of the same family of logics.

The simplest DLs and PDLs can be easily embedded into a fragment of L 2 , that is, first-order logic with two variables. Application requirements led researchers to extend these ba­ sic logics with more expressive constructs, such as fixpoints, nominals (that represent individuals in DLs), transitive clo­ sure operators similar to Kleene's star, and equivalents of gen­ eralized quantification called number restrictions (or count­ ing) in DLs and graded modalities in PDLs. At the same time, applications require these logics to be decidable and have ac­ ceptable computational complexity.

The evolution of DLs and PDLs produced-and keeps on extending-a hierarchy of decidable logics with multi­ ple maximal elements. Currently, two of the maximal de­ cidable DLs are pACCIO (featuring fixpoints and nomi­ nals [Sattler and Vardi, 1999; Bonatti, 2002]) and pACCIQ (featuring fixpoints and number restrictions). The corre­ sponding PDLs are the hybrid p-calculus and the p-calculus with graded modalities, respectively [Sattler and Vardi, 1999; Kupferman et al., 2002].

Of course, it would be desirable to combine the features of different maximal logics into one super-logic. A combination of pACCIO and pACCIQ would help-for example-in describing the functional behavior of e-Services (cf. [Bon­ atti, 2002] and related comments on SVC(X) in Section 5). However, in the super-logic inference may turn out to be too complex, and in particular undecidable.

A related, interesting open question pointed out by Sattler and Vardi [Sattler and Vardi, 1999] is whether inference in the union of the hybrid p-calculus and the p-calculus with graded modalities is decidable, and which complexity class it belongs to. More precisely, Sattler and Vardi mention a slightly simpler logic: a hybrid p-calculus with determin­ istic programs. Deterministic programs are a special case of graded modality, whose counterpart in DLs are features, i.e., functional roles. The DL corresponding to the hybrid p-calculus with deterministic programs is called pACCIO 1.

The main contribution of this paper is a negative answer to the above open question. We prove that the hybrid p­ calculus with deterministic programs and the correponding DL pACCIO 1 are undecidable. For this purpose, we use a novel approach based on nested fixpoints.

The second contribution is an undecidability result for log­ ics that support number restrictions together with regular role expressions. These results show that transitive role closure can be more expressive than fixpoints in some contexts.

In the next section we recall the basic notions about DLs and the p-calculi. Section 3 is devoted to the undecidabil­ ity proof for pACCIO 1 and the hybrid p-calculus with de­ terministic programs. Section 4 briefly illustrates the unde­ cidability result for the combination of transitive closure and number restrictions. Finally, Section 5 concludes the paper with a brief discussion of the results and some directions for further research. Some proofs will be omitted because of space limitations.

2 Preliminaries

The vocabulary of the description logics we deal with in this paper is specified by the following disjoint sets of symbols: a set of atomic concepts At, a set of nominals Nom, a set of concept variables Var, and a set of atomic roles AR.

The set of roles is the smallest superset of AR such that if R, R' are roles then R-, R U R', and R* are roles.

Let R be a role, X E Var and n E N. The set of concepts is the smallest superset of At U Nom U Var such that if C C' D are concepts, then -,C, C n D, :l~n R.C, and pX.C' a~e c~n­ cepts, provided that all the free occurrences of X in C' lie within the scope of an even number of operators-, and :l ~n.

Semantics is based on interpretations of the form I = (6J, · 7 ) where 1:1 7 is a set of individuals and .I is an inter­ pretation function mapping each A E At U Nom onto some A 7 ~ 1:1 7 , and each R E AR onto some R 7 C 1:1 7 x 1:1 7 . Furthermore, nominals must be mapped onto ;ingletons. A valuation on I is a function p : Var -+ p(t1 7 ). As usual, p[X/ S] denotes the valuation such that p[X/ S](X) =Sand for all Y f:. X, p[ X/ S](Y) = p(Y). The meaning of inverse roles is

while (RUR'f = R 7 UR' 7 , and (R*f denotes the reflexive transitive closure of R 7 .

The meaning of compound concepts is determined by pairs (I , p). By US we denote the cardinality of a setS.

Subscript p will be sometimes omitted when it applies to a closed concept (i.e., such that all variables are bound by Jt).

Other standard constructs can be derived from the above concepts. We use the symbol ~ to define abbreviations.

Here C[X/-,X] is the concept obtained from C by replacing all free occurrences of X with -,X.

The syntactic restrictions on concept variables make ev­ ery concept C monotonic with respect to its free variables. Then JtX.C(X) and vX.C(X) denote exactly the least and the greatest fixpoints of C(X), that can be characterized with the standard iterative constructions.

An assertion has the form C C D where C and D are closed concepts. It is satisfied by i(equivalently, I is a model of the assertion) iff C 7 ~ D 7 . A TBox is a finite set of assertions. A TBox is satisfiable iff it has a model, that is, an I that satisfies all the assertions in the TBox. Symmetric pairs of assertions such as C C D and D C C will be abbreviated by C = D. A TBox T~ntails C ~ -D if every model ofT satisfies C ~ D.

The description logic ACC is a fragment of the logic de­ scribed so far, supporting only atomic roles, -,, n and :JR.C

(plus all the constructs definable from these). In ACC, Nom= 0.

By convention, the name of a description logic contains ACC if the logic extends ACC. Moreover, the name contains an I if inverse roles (R-) are supported, an 0 if Nom f:. 0, a Q if number restrictions (:l~n R.C) are supported, and a 11- if fixpoints are supported. For example, ACCIO denotes the extension of ACC with inverse roles and nominals. A subscript f indicates that roles may be declared to be func­ tions. Note that such assertions are a special case of number restriction, as they can be expressed with axioms of the form T ~ :l~ 1 R.T. If the logic supports role operators besides inversion, we list those operators as superscripts. For exam­ ple ACCIU,· denotes the extension of ACCI with role union and reflexive transitive closure.

Description logics can be regarded as variants of the propo­ sitional Jt-calculi. Individuals correspond to possible worlds and roles correspond to accessibility relations. Atomic con­ cepts play the role of propositional symbols. In particular, 11-ACCIO 1 can be embedded into the hybrid Jt-calculus with deterministic programs and graded modalities ((n, P)F and [n, P]F) via the following satisfiability-preserving transla­ tion. For all propositions p, and for all n > 0,

Moreover, functional roles are mapped onto deterministic programs (whose accessibility relation is the graph of a function), and nominals are mapped onto their equivalents (called nominals, too), that in PDL terms are propositional symbols that are true in exactly one world. Program o denotes the universal program whose accessibility relation consists of all pairs of possible worlds. The reader is re­ ferred to [Sattler and Vardi, 1999; Kupferman et al., 2002; De Giacomo, 1995] for further details.

3 Undecidability of J.LA£C'IO 1

This section is devoted to the proof of the following theorem.

Theorem 3.1 In 11-ACCIO I· concept satisfiability, TBox sat­ isfiability and entailment are all undecidable.

We find it convenient to prove this theorem by first reduc­ ing domino problems to TBox satisfiability, and then extend­ ing this result to the other decision problems.

Recall that domino problems consist in placing tiles on an infinite grid, satisfying a given set of constraints on ad­ jacent tiles. Formally, a domino problem is a structure V = (T, H, V), where Tis a set of tile types and H, V ~ T 2 spec­ ify which tiles can be adjacent horizontally and vertically, respectively. A solution to V is a tiling, that is, a function T : N2 -+ T, such that

The existence of a solution for a given domino problem is known to be undecidable (cf. [Gradel et al., 1999]).

Domino problems are reduced to reasoning problems by characterizing (i) the grid and (ii) correct tilings. Formally, the grid is a structure 9 = (f'P, hg , v9 ), where hg (x , y) = (x + 1, y), and v9 (x, y) = (x, y + 1), for all x , yE N.

In description logics, hg and v9 can be denoted by two roles, h and v. If the two roles characterize the grid cor­ rectly (see Figure 1 (a)), then characterizing the solutions of a domino problem is easy, even within simple (and decidable) description logics such as A.CC, by means of the following assertion:

Here for each tile type t, a distinct concept name Ct is in­ troduced. Assertion (1) basically states that each individual is a tile (first term), that distinct tile types contain different tiles (rest of the first line), and that the tiling preserves the constraints specified by H and V (second line).

The real problem is characterizing the grid, because there is no direct way to force h and v to commute. Here we shall provide a projective characterization of 9, that is, we shall capture exactly the class of interpretations isomorphic to the expansion 9* = (f'P' hg ' v9 ' og·) of 9, where 0 is a unary relation and o 9 · = { (0, 0)} .

We proceed in three steps. First, h and v must be forced to be injective functions . For this purpose, we declare all roles and their converse to be functional, which is equivalent to adopting the following assertion, for all roles R.

Second, all nodes are classified with respect to their incom­ ing and outcoming edges. Note that the domain and the range of a role R can be defined as follows.

Now we can define the vertical and the horizontal borders of the grid (Bv and Bh, respectively), and the internal nodes (C). 0 is a nominal that represents the origin of the grid.

The following assertions state the properties of 0 and force the above concepts to cover all the domain .

Third, we characterize the global structure of the grid. The next assertions ensure that the vertical border Bv and the hor­ izontal border Bh have the desired structure (i.e., they should be isomorphic to N).

Note that Bv and Bh contain no cycles, because of (2) and (3), so the two fixpoints induce infinite linear sequences of nodes.

Finally, we introduce an assertion that forces h and v to commute everywhere.

Informally speaking, the constructive characterization of the fixpoint in (7) corresponds to a visit of the grid along diag­ onals directed north-west (Figure l(b)). At each iteration, a new node x0 is considered. Subformula cp0 (X) ensures that x0 is connected to the last visited element XI in such a way that h and v commute. Actually, h and v are not explicitly re­ quired to commute. They actually do (equation (9)) because each visited node x but the last one (i .e., XI) must be con­ nected by v o h- and h- o v to another visited node (Proposi­ tion 3.3.e), therefore, by (2), there exist no further links v o h­ and h- o v connecting x to (the not yet visited node) x0 . It follows that only XI can be connected to x0 as specified by cp0 (X) . This makes hand v commute and ensures that x0 is unique. Every time the vertical border Bv is reached, subfor­ mula Cf?I (X) adds the first element of the next diagonal. For this purpose, subformula pY.cp2 (X, Y) looks for diagonals entirely contained in X (the set of nodes visited so far) so that a new diagonal is not entered before the previous one has been completely visited. Figure l(c) illustrates this phase. Let Xi be the current set of visited nodes. The black circles are the elements of Cf?I (Xi). In this example, pY.cp2 (Xi , Y) equals xi. because the latter contains precisely the first 3 diagonals. In the following we formalize all the above intuitions.

Let T consist of the assertions (2), the local constraints (3) and (4), and the fixpoint assertions (5), (6) and (7). In the rest of this section, let I be a model of T.

First we introduce some notation related to the domain el­ ements of I . Let o E OI . For all d, j E N, let

Note that ed,j is not necessarily defined, because h-I is par­ tial. Informally speaking, d counts diagonals and j is the dis­ placement within a diagonal (cf. Figure l(b)). Indexes are ordered lexicographically. Define

For all sets S ~ D. I, let max( S) be the element ed,j E S with ~-maximal index (if any). The restriction of~ to ~ = { (x, y) E I"P I x ~ y} admits a successor relation, namely:

With a slight abuse of notation, succ~ ( ed,j) will denote Csucc-< (d,j) ·

Next we need a constructive characterization of the fixpoint in assertion (7). To improve readability, in the following we abbreviate ~(x);(X/SJ to e(s), where s ~ ~I . Formulae cp; (i = 0, 1, 2) will be treated in a similar way. Then the fix point can be characterized as follows.

To ensure that the fixpoint is actually reached within w steps, as implicitly claimed by the above construction, it suffices to show that a is continuous.

Proposition 3.2 a is continuous, that is, for all non­ decreasing sequences {X;};:::;,., where a is an ordinal, e (U;<,. x;) = ui<<> e (X;).

The following technical result formalizes the intuitive ex­ planation of the nested fixpoint construction.

Proposition 3.3 For all integers i ~ 0 such that X; c Xi+1, there exists ed,j E X;+l such that:

1. For all x E X;+l \ {ed,j}, if h-I(x) is defined then vi(h-I(x)) E X;+l and h-I(vi(x)) E Xi+1 .

f For all ek,l E Xi+ I> if ek,l E Bt then k = l.

Proof. We prove a-f simultaneously, by induction on i. For i = 0, X; = or = {o} = {eo,o} and X;+l = cpf(Xo) = X; U {e1,o} C B~. Then a-fare trivially satisfied with (d,j) = (1 ,0).

Now assume i > 0. Let x0 E X;+l \X;. Then there are two possibilities: either xo E cpif(X;) or x0 E cpf(X;).

Note that these two cases are mutually exclusive, because the elements of cpif (X;) are in the range of vi, while the elements of cpf (X;) are not, because they belong to B~ .

Case 1: xo E cpif(X;). By definition of cp0 , there must be x1,x2 E X; such that hi(v-I(xo)) = x1 and v-I(hi(xo)) = x2. Since hi and v-I are inJective func­ tions(bytheassertions(2)),vi(h-I(x1)) = h- (vi(x2)) = x0 f_ X;, and hence, by induction hypothesis e (I.H.e for short), x1 = x2 = max(X;). Now, by choosing d and j such that max(X; ) = ed,j-1· we have x0 = h-I(vi(x2)) = h-I(vi(ed,j-1 )) = ed,j· The above equations can be rewrit­ ten as

Since (9) holds for arbitrary Xo E xi+1 \X;, we have that Xo is the unique member of X;+l \X;, and hence point a holds.

Now, since max(X;) = ed,j-1 and succ~(d,j - 1) ( d, j), we immediately get point b.

To prove c, note that

To prove d, note that

Point e follows from the corresponding I.H.e and (9).

We are only left to show that f holds. The induction hypothesis I.H.f covers all cases but (k, l) = (d, l). If ed,l E Bt, then v-I ( ed,j ) E Bt, by assertion (5). Moreover, v-I(ed,j ) = ed- 1,j-I. by (10). Then ed-1,j-1 E Bt. and hence, by I.H.f, d- 1 = j -1. Point f follows immediately.

This concludes the proof for Case 1.

Case 2:. x? E cpf(X¥. ~y definiti~n of cp1 , the following facts hold. (1) Xo E B h, (11) there exist { x1, ... , Xn} E X; (n > 0) such that

(cf. Figure 1(c)). By I.H.f and (11), x1 = ed-1,d-1 for some d E N. Then, by (13), { x1 , ... , Xn} must equal {ed-1,d-1, ed-1,d-2, ... , ed-1,o}.

Now, if ed-1,d-1 ::f max(X;), then the set {ed-1,d-1, ed-1,d-2, ... , ed-1,o} would be entirely contained in X;-1 and hence x0 E cpf (X;_ I) C X;, a contradiction. Consequently,

Note also that

Now we are ready to prove a-f. Let j = 0.

Since x0 = ed,o for an arbitrary xo E X;+l \ X;, point a holds.

Moreover, succ~ (d-1, d-1) = (d, 0) so point b is entailed by (14). -

Point c holds vacuously as j = 0.

Point d holds, as h-I(ed,o) = ed-1,o by definition of ed,O· Point e is covered by I.H.e with the exception of max(X;) = ed-1,d_1, that satisfies e vacuously because it is a member of B?j and hence h-I(ed-1,d-d is undefined.

Finally, to prove point f, note that ed,o f/. B?j (because ed,o E B~ \ QI), so f is satisfied vacuously when (k, l) = (d, 0) . All the other cases are implied by I.H.f. This com­ pletes the proof. I

We are now ready to prove the two propositions that con­ firm that T characterizes the grid.

Proposition 3.4 Every model ofT is isomorphic to Q*.

Proof. Suppose I. is a model ofT Then (5) and (6) cause 6. 7 to be infinite. On the contrary, each X; (i < w) is finite, by Proposition 3.3.a. It follows by assertion (7) that no X; can be a fixpoint of e fori < W, and hence the hypothesis of Proposition 3.3-that is, X; c Xi+1 -is satisfied for all i < w.

As a first consequence of Propositions 3.3.a, b, we have that for all ( d, j) E ~, ed,j is defined and 6. I = { ed,j I (d,j) E ~ }. Since X; C Xi+1 , Propositions 3.3.a,b imply also that e;,i and ek,t are always distinct when (d, j) ::f (k, l).

Then the function f : 6. I -7 ~ specified by

is well defined and total. Moreover, the total function g : N2 -7 6.I definedbyg(i,j) = ei+j,j satisfiesgof =fog= id, so f is a bijection.

We are left to show that f is a morphism. By Proposi­ tion 3.3.c,d, we have that for all (d,j) E ~· hi(ed,j) ed+ 1 ,j and v 7 ( ed,j) = ed+l ,i+ 1· Then

Moreover, j(QI) = {f(eo,o)} = {(0,0)} = Og·. We con­ clude that f is an isomorphism. I

Proposition 3.5 Q* is a model ofT

Since the J.LA.CCI.O 1 TBox Tis a projective characteriza­ tion of Q (by Propositions 3.4 and 3.5) and the J.LA£CI.O 1 assertion (1) is satisfied only by correct tilings, we derive the following lemma.

Lemma 3.6 Satisfiability of J.LA£CI.O 1 TBoxes is undecid­ able.

We are left to extend this lemma to concept satisfiability and entailment. This is done through the following reduc­ tions.

Lemma 3.7 In all extensions of J.LA£CI.,

1. TBox satisfiability can be reduced to concept satisfiabil­ ity in polynomial time.
2. Concept unsatisfiability can be reduced to entailment in polynomial time.

By Lemma 3.6 and Lemma 3.7, we conclude that the main result of this section, Theorem 3.1, holds.

Finally, with Theorem 3.1 and the standard embedding of description logics into propositional dynamic logics, we im­ mediately obtain the following result.

Corollary 3.8 Formula satisfiability in the hybrid J.L-calculus with deterministic programs is undecidable.

4 Regular roles and counting

Description logics with regular role expressions introduce a form of recursion (Kleene's star, or reflexive transitive clo­ sure) different from fixpoints. It is interesting to investigate the interplay of this form of recursion and counting.

Consider A£CIQu·* (the extension of A£CI.Q with role union and reflexive transitive closure). We prove its undecid­ ability by characterizing domino problems with unbounded grids (i.e., grids without borders) in A£CI.Qu·*. The grid is modelled by splitting the injective functional role h (resp. v) into the disjoint union of two roles ho and h1 (resp. v0 and v1), alternated as shown in Figure 2(a). Nodes are then par­ tioned into four classes 'f/i,j, 0 ~ i, j ~ 1, according to their incoming and outcoming edges ((3R) abbreviates 3R. T):

All nodes are forced to belong to one of these four classes by an assertion T ~ 'f/o,o U 'f/o,1 U 'f/1,0 U 'f/1,1·

Furthermore, the four assertions

(where 0 ~ i,j ~ 1) force the desired alternation of h0 , h1 , vo and v1 (cf. Figure 2(a)).

Now the compound role ( h; U Vj) * applied to a node eo can reach at most five different nodes eo-c4 (cf. Figure 2(b)), because the alternation of edges with index 0 and 1 (more precisely, assertions ( 16)) guarantees that c1 , c3, c4 have no outcoming Vj edges, and that c2, c3, c4 have no outcoming hi edges.

Then the following assertions (where 0 :::; i, j :::; 1) imply that for each node in 'f/i,j, hi and Vj commute.

In fact-with reference to Figure 2(b )-for all co in 'f/i ,j, as­ sertion (16) forces nodes c0-c4 to belong to different (mutu­ ally disjoint) concepts 'f/x,y. with the exception of c3 and C4, both of which belong to 'f/I-i,I-j. Now if c3 =/= c4 then (17) would be violated (there would be 5 nodes reachable with (hi U Vj)*), so hi and Vj commute (i .e., ho, hi, vo, VI char­ acterize the unbounded grid).

We are only left to model correct tilings. It suffices to adapt assertion (1) by replacing h and v with ho U hi and vo U VI, respectively. From the above discussion we derive the following theorem.

Theorem 4.1 A.CCIQU,· is undecidable.

On the contrary, 11A.CCIQu is decidable. In fact, every expression in J..LA.CCIQu is equivalent to an expression in the decidable logic 11A.CCIQ thanks to the equivalence

Then Theorem 4.1 suggests that transitive closure is more powerful than fixpoints in this context (the extension of A.CCIQu with fixpoints is decidable, while the extension with * is not).

5 Discussion and conclusions

Description logics evolved into a hierarchy of decidable log­ ics with multiple maximal elements. Some support fixpoints, inverse roles, and either nominals or number restrictions (but not both) [Sattler and Vardi, 1999; Kupferman et al., 2002]. Others support rich sets of role operators, including union and transitive closure.

The results of this paper show that the above features can­ not be easily combined into one decidable logic. In particular, no decidable extension of A.CCI can simultaneously support fixpoints, nominals and number restrictions, even in the very special case where number restrictions are confined into the functionality assertions (2). 1 As a corollary, the hybrid t-L­ calculus with deterministic programs is proved to be unde­ cidable. Moreover, Theorem 4.1 shows that role union and transitive closure cannot occur together within number re­ strictions (it provides also evidence that * is more expressive than fixpoints) .

These results have immediate implications on V.CR [Cal­ vanese et al., 1999], a rich DL with n-ary relations. Recall that 11A.CCIQ can be embedded into V.CR~-' [Calvanese et al., 1999]. Similarly, A.CCIQ can be embedded into V.CR (the fragment of V.CRJ.L without fixpoints) . Then Theo­ rem 3.1 and Theorem 4.1 imply that decidability is preserved neither by extending V.CRJ.L with nominals, 2 nor by extending v.cn with role operators u and*· .

An interesting question arising from these results concerns the family of service description logics SV.C(X) [Bonatti, 2002] . These logics are analogous to D.CRJ.L, in the sense that they model mappings (that can be regarded as n-ary re­ lations). SV.C(X) differs from V.CR~-' because the former features set abstraction and composition, while V.CRJ.L sup­ ports number restrictions. Service descriptions in SV.C(X) are supposed to extend an underlying ontology written in a standard description logic X (modelling concepts and roles only). The main reasoning tasks for SD.C(X) are proved to be decidable by embedding SV.C(X) into decidable ex­ tensions of both 11A.CCIO and X. By the undecidability of 11A.CCIO 1, it follows that this technique cannot be applied when X supports number restrictions, or simply functional roles. Then the (un)decidability of SV.C(X), when X sup­ ports number restrictions of some sort, remains an interesting open issue.