The goal of the present work is to enhance the expressiveness of modal temporal logics with qualitative spatial constraints. What we get is a family of qualitative theories for spatial change in general, and for motion of spatial scenes in particular. The family consists of domain-specific spatio-temporal (henceforth s-t) languages, and is obtained by spatio-temporalising a well-known family of description logics (DLs) with a concrete domain, known as ALC(D) (Baader and Hanschke 1991). ALC(D) originated from a pure DL known as ALC (Schmidt-Schauss and Smolka 1991), with roles all of which are general, not necessarily functional relations, and which Schild (Schild 1991) has shown to be expressively equivalent to Halpern and Moses’ Kmodal logic (Halpern and Moses 1985). ALC(D) is obtained by adding to ALC functional roles (better known as abstract features), a concrete domain D, and concrete features (which refer to objects of the concrete domain). The spatio-temporalisation of ALC(D) is obtained, as the name suggests, by performing two specialisations at the same time: (1) temporalisation of the roles, so that they consist of m + n immediate-successor (accessibility) relations , of which the ’s are general, the ’s functional; and (2) spatialisation of the concrete domain D: the concrete domain is now D, and is generated by a spatial RA x, such as the RegionConnection Calculus RCC8 (D A Randell and Cui 1992).

The final spatio-temporalisation of ALC(D) will be referred to as MTALC(MTALC for Modal Temporal ALC). Constraint-based languages candidate for generating a concrete domain for a member of our family of spatio-temporal theories, are spatial RAs for which the atomic relations form a decidable subset —i.e., such that consistency of a CSP expressed as a conjunction of p-ary relations on p-tuples of objects, where p is the arity of the RA relations, is decidable. These include, the RegionConnection Calculus RCC8 in (D A Randell and Cui 1992) (see also (Egenhofer 1991)), the Cardinal Directions Algebra CDA in (Frank 1992), and the rectangle algebra in (Balbiani, Condotta, and del Cerro 1998) (see also (G¨usgen 1989; Mukerjee and Joe 1990)), for the binary case; and the RA CYCof 2D orientations in (Isli and Cohn 1998; Isli and Cohn 2000) for the ternary case. As our illustrating spatial RA, we will be using the ternary RA in (Isli and Cohn 1998; Isli and Cohn 2000).

It is known that, in the general case, satisfiability of an

ALC(D) concept with respect to a cyclic Terminological Box (TBox) is undecidable (see, e.g., (Lutz 2001)). In order to capture the expressiveness of most modal temporal logics encountered in the literature, we introduce in this work weakly cyclic TBoxes of MTALC, whose axioms capture the decreasing property of modal temporal operators. We show the important result that satisfiability of an MTALCconcept with respect to a weakly cyclic TBox can be reduced to the emptiness problem of a B¨uchi weak alternating automaton augmented with spatial constraints. In another work, complementary to this one, also submitted to this conference, we thoroughly investigate B¨uchi automata augmented with spatial constraints, and provide, in particular, a translation of an alternating into a nondeterministic, and an effective decision procedure for the emptiness problem of the latter.

Temporalisations of DLs are known in the literature (see, e.g., (Artale and Franconi 2000; Bettini 1997)); as well as spatialisations of DLs (see, e.g., (Haarslev, Lutz, and M¨oller 1999)). The present work considers a spatio-temporalisation of the well-known family ALC(D) of DLs with a concrete domain (Baader and Hanschke 1991). Specifically, we consider, at the same time, a temporalisation of the roles of the family and a spatialisation of its concrete domain.

Concrete domain Definition 1 (concrete domain (Baader and Hanschke 1991)) A concrete domain D consists of a pair , where D is a set of (concrete) objects, and D is a set of predicates over the objects in D. Each predicate D is associated with an arity n and we have .

Definition 2 (admissibility (Baader and Hanschke 1991)) A concrete domain D is admissible if: (1) the set of its predicates is closed under negation and contains a predicate for D; and (2) the satisfiability problem for finite conjunctions of predicates is decidable.

The concrete domains D, with x spatial RA

Any spatial RA x for which the atoms are Jointly Exhaustive and Pairwise Disjoint (henceforth JEPD), and such that the atomic relations form a decidable subclass, can be used to generate a concrete domain Dfor members of the family MTALCof qualitative theories for spatial change. Such a concrete domain is used for representing knowledge on p-tuples of objects of the spatial domain at hand, p being the arity of the x relations; stated otherwise, the x relations will be used as the predicates of D.

Admissibility of the concrete domains D, with

RCC8, CDA, CYC

Let RCC8, CDA, CYC. The concrete domain generated by x, D, can be written as D, with: DRCC8 = (RTS, 2RCC8-at), DCDA = (2DP, 2CDA-at) and DCYC2DO, 2CYC-at), where RTS is the set of regions of a topological space TS; 2DP is the set of 2D points; 2DO is the set of 2D orientations; and x-at, as we have seen, is the set of x atoms —2x-at is thus the set of all x relations.

Admissibility of the concrete domains Dis an immediate consequence of (decidability and) tractability of the subset x-at} of x atomic relations, for each RCC8, CDA, CYC. The reader is referred to (Renz and Nebel 1999) for x = RCC8, to (Ligozat 1998) for x = CDA, and to (Isli and Cohn 1998; Isli and Cohn 2000) for x = CYC:

Theorem 1 Let RCC8, CDA, CYC. The concrete domain Dis admissible.

Syntax of MTALCconcepts

Definition 3 (MTALCconcepts) Let x be an RCC8-like p-ary spatial RA. Let and be mutually disjoint and countably infinite sets of concept names, role names, and concrete features, respectively; and a countably infinite subset of whose elements are abstract features. A (concrete) feature chain is any finite composition of abstract features and one concrete feature g. The set of MTALCconcepts is the smallest set such that:

1. and are MTALCconcepts 2. an MTALCconcept name is an MTALC(atomic) concept 3. if C and D are MTALCconcepts; R is a role (in general, and an abstract feature in particular); are feature chains; and P is an MTALCpredicate, then the following expressions are also MTALCconcepts: (a) ; and (b) .

We denote by MTALC the sublanguage of MTALCgiven by rules 1, 2 and 3a in Definition 3, which is the temporal component of MTALC. It is worth noting that MTALC does not consist of a mere temporalisation of ALC (Schmidt-Schauss and Smolka 1991). Indeed, ALC contains only general roles, whereas MTALC contains abstract features as well. A mere temporalisation of ALC (i.e., MTALC without abstract features) cannot capture the expressiveness of well-known modal temporal logics, including Propositional Linear Temporal Logic PLTL, the computation tree logic CTL, and the subsuming full branching modal temporal logic CTL(Emerson 1990). Given two integers and , the sublanguage of MTALC(resp. MTALC) whose concepts involve at most p general roles, and q abstract features will be referred to as MTALC(resp. MTALC). The particuler case (p, q) = (0, q) with is discussed in Section ??, where we provide a translation of CTLto MTALC.

Definition 4 (subconcept) The set Subc(C) of subconcepts of an MTALCconcept C is defined inductively as follows:

1. Subc, Subc

2. Subc(A) = {A}, Subc, for all atomic concepts A 3. SubcSubcSubc(D), 4. SubcSubcSubc(D), 5. SubcSubcSubc, 6. SubcSubcSubc, 7. SubcSubc(C), 8. SubcSubc(C), 9. SubcSubc, 10. Subc, 11. Subc. 12. Subc.

We now define weakly cyclic TBoxes.

Weakly cyclic TBoxes An (MTALCterminological) axiom is an expression of the form A .= C, A being a concept name and C a concept. A TBox is a finite set of axioms, with the condition that no concept name appears more than once as the left hand side of an axiom.

Let T be a TBox. T contains two kinds of concept names: concept names appearing as the left hand side of an axiom of T are defined concepts; the others are primitive concepts. A defined concept A “directly uses” a defined concept B iff B appears in the right hand side of the axiom defining A. If “uses” is the transitive closure of “directly uses” then T contains a cycle iff there is a defined concept A that “uses” itself. T is cyclic if it contains a cycle; it is acyclic otherwise. T is weakly cyclic if it satisfies the following two conditions:

1. Whenever A uses B and B uses A, we have B = A — the only possibility for a defined concept to get involved in a cycle is to appear in the right hand side of the axiom defining it.

2. All possible occurrences of a defined concept B in the right hand side of the axiom B .= C defining B itself, are within the scope of exactly one quantifier (in other words, there is no free ocurrence of B in C, and no occurrence of B in C is within the scope of more than one quantifier).

Definition 5 (depths of a defined concept) Let B be a de-fined concept, and C a concept. The set of depths of B in C, depths(B, C), is the set of all integers d such that B has an occurrence in C whithin the scope of d quantifiers. depths(B, C) is defined inductively as follows:

Remark 1 In Definition 5:

1. Item (1) includes the following particular case: depths; and

2. Item (5) includes the particular case: if depthsthen depthsdepths.

A weakly cyclic TBox can now be defined formally as follows:

Definition 6 (weakly cyclic TBox) A TBox T is weakly cyclic if and only if it satisfies what follows:

1. whenever two defined concepts A and B are such that A uses B and B uses A, we have B = A; and

2. all axioms B .= C of T verify the following: depthsor depths(B, C) = {1}.

Definition 7 Let T be a weakly cyclic TBox. 1. An axiom B .= C of T is cyclic if depths(B, C) = {1}; it is acyclic otherwise 2. A defined concept B of T is cyclic if the axiom B .= C defining it is cyclic; it is acyclic otherwise 3. A cyclic axiom of T is said to be a necessity axiom if it is

4. A cyclic axiom of T is said to be an eventuality axiom if it

5. A defined concept of T is a necessity defined concept if the axiom defining it is a necessity axiom 6. A defined concept of T is an eventuality defined concept if the axiom defining it is an eventuality axiom 7. The necessity defined concept and the eventuality

8. The necessity defined concept and the eventuality

From now on, we restrict ourselves, exclusively, to weakly cyclic TBoxes T such that

1. for all necessity or eventuality defined concepts B of T , T also has the defined concept consisting of the dual of B; and

2. all defined concepts B verify the following:

In the rest of the paper, unless explicitly stated otherwise, we denote concepts reducing to concept names by the letters A and B, possibly complex concepts by the letters C, D, E, general roles by the letter R, abstract features by the letter f, concrete features by the letters g and h, feature chains by the letter u, (possibly complex) predicates by the letter P.

Example 1 Due to lack of space, an example supposed to come here is added as additional material, as a separate file including a brief background on the ternary spatial RA CYC(Isli and Cohn 1998; Isli and Cohn 2000) and an illustration of the use of MTALCDCYCin robot navigation.

Let Dbe an admissible spatial concrete domain generated by a p-ary spatial RA x. MTALCconcepts will be interpreted over k-ary -trees.

Definition 8 (k-ary -tree) Let and , , be two disjoint alphabets: is a labelling alphabet and K an alphabet of directions. A (full) k-ary tree is an infinite tree whose nodes have exactly k immediate successors each, . A -tree is a tree whose nodes are labelled with elements of . A (full) k-ary -tree is a k-ary tree t which is also a -tree, which we consider as a mapping associating with each node an element . The empty word, , denotes the root of t. Given a node and a direction , the concatenation of and , denotes the d-successor of . The level of a node is the length of as a word. We can thus think of the edges of t as being labelled with directions from K, and of the nodes of t as being labelled with letters from . A partial k-ary -tree (over the set K of directions) is a -tree with the property that a node may not have a d-successor for each direction d; in other terms, a partial k-ary -tree is a -tree which is a prefix-closed2 partial function .

MTALCis equipped with a Tarski-style possible worlds semantics. MTALCinterpretations are spatio-temporal structures consisting of k-ary trees t, representing k-immediate-successor branching time, together with an interpretation function associating with each primitive concept A the nodes of t at which A is true, and, additionally, associating with each concrete feature g and each node u of t, the value at u (seen as a time instant) of the spatial concrete object referred to by g. Formally:

Definition 9 (interpretation) Let x be an RCC8-like p-ary spatial RA and a set of k directions. An interpretation I of MTALCconsists of a pair I = (tI, .I), where tI is a k-ary tree and .I is an interpretation function mapping each primitive concept A to a subset AI of ; each role R to a subset RI of , so that RI is functional if R is an abstract feature; and each concrete feature g to a total function gI from

onto the set of (concrete) objects of the concrete domain D.

Given an MTALCinterpretation I = (tI, .I), a feature chain , and a node , we denote by the value , where is the -successor of ; i.e., is so that there exists a sequence verifying , for all (in other words, ).

Definition 10 (satisfiability w.r.t. a TBox) Let x be an RCC8-like p-ary spatial RA, a set of k directions, C an MTALCconcept, T an MTALCweakly cyclic TBox, and I = (tI, .I) an MTALCinterpretation. The satisfiability, by a node s of tI, of C w.r.t. to T, denoted I, is defined inductively as follows:

4. Iiff I, Iiff I, for all defined concepts B defined by the axiom B .= C of T, such that B does not occur in C, the right hand side of the axiom (in other words, such that depths).

5. for all eventuality defined concepts B defined by the axiom , Iiff there exists , with , such that:

13. Iiff Iand I, s |=

14. Iiff I, for some such that I

15. Iiff I, for all such that I

A concept C is satisfiable w.r.t. a TBox T iff I, for some MTALCinterpretation I, and some state I, in which case the pair (I, s) is a model of C w.r.t. T; C is insatisfiable (has no models) w.r.t. T, otherwise. C is valid w.r.t. T iff the negation, , of C is insatisfiable w.r.t. T.

Let C be an MTALCconcept and T an MTALCweakly cyclic TBox. We define T as the TBox T augmented with the axiom being a fresh de-fined concept (not occurring in T):

In the sequel, we refer to T as the TBox T augmented with C. The idea now is that, satisfiability of C w.r.t. T has (almost) been reduced to the emptiness problem of T , seen as a weak alternating automaton on k-ary -trees, for some labelling alphabet to be defined later, with the de-fined concepts as the states of the automaton, as the initial state of the automaton, the axioms as defining the transition function, with the accepting condition derived from those defined concepts that are not eventuality concepts, and with k standing for the number of concepts of the form in a certain closure, to be defined later, of T .

The Disjunctive Normal Form The notion of Disjunctive Normal Form (DNF) of a concept C w.r.t. to a TBox T, dnf1(C, T), is crucial for the rest of the paper. Such a form results, among other things, from the use of De Morgan’s Laws to decompose a concept so that, in the final form, the negation symbol outside the scope of a (existential or universal) quantifier occurs only in front of primitive concepts.

Given a (concrete) feature chain u, we define Exists(u) as follows:

Definition 11 (first DNF) The first Disjunctive Normal Form (dnf1) of an MTALCconcept C w.r.t. an MTALCweakly cyclic TBox T, dnf1(C, T), is defined inductively as follows:

1. for all primitive concepts A: dnf1(A, T) = {{A}}, dnf1

Note that the dnf1 function checks satisfiability at the propositional level, in the sense that, given a concept C, dnf1(C, T) is either empty, or is such that for all dnf1(C, T), S does not contain both A and being a primitive concept. Furthermore, given a set dnf1(C, T), all elements of S are concepts of either of the following forms: A or , where A is a primitive concept; ; or .

Definition 12 (the pcpartition) Let C be an MTALCconcept, T an MTALCTBox, dnf1(C, T) and the language of all finite words over the alphabet . The pcpartition of S, pc, is defined as pc, where:

and is computed as follows :

1. Initialise to the empty set :

2. For all in S with R general role:

3. For all abstract features f such that S contains ele-

The second dnf of a concept C w.r.t. a TBox T, dnf2(C, T), is now introduced. This consists of the dnf1 of C w.r.t. T, dnf1(C, T), as given by Definition 11, in which each element S is replaced with . Formally:

Definition 13 (second DNF) Let {RCC8, CDA, CYCbe an MTALCconcept, and T an MTALCweakly cyclic TBox. The second Disjunctive Normal Form (dnf2) of C w.r.t. T, dnf2(C, T), is defined as dnf2dnf1(C, T)}.

Given an MTALCconcept C and an MTALCTBox T, we can now use the second DNF, dnf2, to define the closure of , the TBox T augmented with C.

Definition 14 (closure of ) Let C be an MTALCconcept and T an MTALCweakly cyclic TBox. The closure of is defined by the procedure of Figure 1, which also outputs a partial order PO on the defined concepts of .

Remark 2 The axioms of are of the form B = ; for all , all elements of S are of either of the following forms:

1. A or , where A is a primitive concept;

2. being a general role or an abstract feature, and a defined concept, for all ; or

3. . . . .P.

We also need the closure of a concept C w.r.t. a TBox T, cl(C, T), which is defined as the union of the right hand sides of the axioms in . Formally:

Definition 15 (closure of a concept w.r.t. a TBox) The closure of an MTALCconcept C w.r.t. an MTALCTBox T, cl(C, T), is defined as follows:

Definition 16 Let C be an MTALCconcept and T an MTALCTBox. We denote by:

1. cFeatures(S), where cl(C, T), the set of concrete features of S: in other words, cFeatures(S) is the set of concrete features g for which there exists a feature chain u suf-fixed by g, such that S contains a predicate concept , with .

E. POiv. for all abstract features f such that S contains elements of the form

Figure 1: The closure of a weakly cyclic TBox T augmented with a concept ; and a partial order PO on the defined concepts of .

2. cFeatures

crete features of C w.r.t. T; 3. ncf(C, T) = |cFeatures(C, T)|, the number of concrete features of C w.r.t. T; 4. aFeaturesfor some concept E there exists cl(C, T) s.t. S}, the set of abstract features of C w.r.t. T; 5. naf(C, T) = |aFeatures(C, T)|, the number of abstract features of C w.r.t. T; 6. pConceptscl(C, T) s. t. , the set of primitive concepts of C w.r.t. T; 7. dConcepts(C, T) is the set of defined concepts in ; 8. reConcepts(C, T), the set of relational existential (sub)concepts of C w.r.t. T, is the set of all such that R is a general role and there exists an axiom B .= E in and S in E so that ; 9. fbf(C, T) = naf(C, T), the functional branching factor of C w.r.t. T; 10. rbf(C, T) = |reConcepts(C, T)|, the relational branching factor of C w.r.t. T; 11. bf(C, T) = fbf(C, T) + rbf(C, T), the branching factor of C w.r.t. T. We suppose that the relational existential concepts in reConcepts(C, T) are ordered, and refer to the i-th element of reConcepts(C, T), i = 1 . . . rbf(C, T), as rec. Similarly, we suppose that the abstract features in aFeatures(C, T) are ordered, and refer to the i-th element of aFeatures(C, T), i = 1 . . . fbf(C, T), as af. Together, they constitute the directions of the weak alternating automaton to be associated with the satisfiability of C w.r.t. T. Definition 17 (branching tuple) Let C be an MTALCconcept and T an MTALCweakly cyclic TBox. The branching tuple of C w.r.t. T is given by the ordered bf(C, T)-tuple bt(C, T) = (recrecrbfafaffbfof the rbf(C, T) relational existential concepts in reConcepts(C, T) and the fbf(C, T) abstract features in aFeatures(C, T). Given an MTALCconcept C and an MTALCweakly cyclic TBox T, we will be interested in k-ary -trees (see Definition 8), t, verifying the following: 1. k = bf(C, T); and

2. pConceptscFeatures, where cFeaturesis the set of total functions cFeaturesassociating with each concrete feature g in cFeatures(C, T) a concrete value from the spatial concrete domain .

Such a tree will be seen as representing a class of interpretations of the satisfiability of C w.r.t. T: the label of a node bf, with pConcepts(C, T) and cFeatures, is to be interpreted as follows:

1. X records the information on the primitive concepts that are true at , in all interpretations of the class; and

2. cFeaturesrecords the values, at the abstract object represented by node , of the concrete features ncfin cFeatures(C, T).

The crucial question is when we can say that an interpretation of the class is a model of C w.r.t. T. To answer the question, we consider (weak) alternating automata on k-ary -trees, with k = bf(C, T) and pConceptscFeatures. We then show how to associate such an automaton with the satisfiability of an MTALCconcept C w.r.t. a weakly cyclic TBox T, in such a way that the models of C w.r.t. T coincide with the k-ary -trees accepted by the automaton. The background on alternating automata has been adapted from (Muller, Saoudi, and Schupp 1992).

Definition 18 (free distributive lattice) Let S be a set of generators. L(S) denotes the free distributive lattice generated by S. L(S) can be thought of as the set of logical formulas built from variables taken from S using the disjunction and conjunction operators and (but not the negation operator ). In other words, L(S) is the smallest set such that: 1. for all ; and 2. if and belong to L(S), then so do and .

Each element has, up to isomorphism, a unique representation in DNF (Disjunctive Normal Form), e = (each is a conjunction of generators from S, and no subsumes , with ). We suppose, without loss of generality, that each element of L(S) is written in such a form. If is an element of L(S), the dual of e is the element obtained by interchanging and is not necessarily in DNF).

Definition 19 (set representation) Let S be a set of generators, L(S) the free distributive lattice generated by S, and e an element of L(S). Write e in DNF as . The set representation of e, set-rep(e), is the subset of defined as , with .

In the following, we denote by K a set of k directions ; by a set of primitive concepts; by x an RCC8-like p-ary spatial RA; by a finite set of concrete features referring to objects in ; by the alphabet being the set of total functions , associating with each concrete feature g a concrete value from the spatial concrete domain ; by Litthe set of literals derived from (viewed as a set of atomic propositions): Lit; by c(2Litthe set of subsets of Litwhich do not contain a primitive concept and its negation: c(2LitLit; by constrthe set

of constraints of the form with P being an x relation, -chains (i.e., , is of the form g or and n finite, the ’s being directions in K, and g a concrete feature). Definition 20 (B¨uchi alternating automaton) Let be an integer and a set of directions. An alternating automaton on k-ary -trees is a tuple A = (L(Litconstr, where Q is a finite set of states; is the input alphabet (labelling the nodes of the input trees); Litconstris the transition function; is the initial state; and F is the set of accepting states. A is said to be a weak alternating automaton if there exists a partial order on Q, so that the transition function has the property that, given two states , if occurs in then . Let A be an alternating automaton on k-ary -trees, as defined in Definition 20, and t a k-ary -tree. Given two alphabets and , we denote by the concatenation of and , consisting of all words ab, with and . In a run r(A, t) of A on t (see below), which can be seen as an unfolding of a branch of the computation tree T (A, t) of A on t, as defined in (Muller and Schupp 1987; Muller, Saoudi, and Schupp 1992; Muller and Schupp 1995), the nodes of level n will represent one possibility for choices of A up to level n in t. For each , we define the set of n-histories to be the set of all 2n + 1-length words consisting of as the first letter, followed by a 2n-length word , with and , for all j = 1 . . . n. If and then hg, the concatenation of h and g, belongs to . More generally, if and , the concatenation he of h and e will denote the element of Lobtained by prefixing h to each generator in KQ which occurs in e. Additionally, given an n-history , with , we denote: 1. by Last(h) the initial state if h consists of the 0-history

), and the state if ; 2. by K-proj(h) (the K-projection of h) the empty word if

n = 0, and the n-length word otherwise; and 3. by Q-proj(h) (the Q-projection of h) the state if n = 0,

and the n+1-length word otherwise. The union of all , with n finite, will be referred to as the set of finite histories of A, and denoted by . We denote by the alphabet c(2Litconstr, by the alphabet Litconstr, and, in general, by the alphabet c(2Litconstr.

A run of the alternating automaton A on t is now introduced. Definition 21 (Run) Let A be an alternating automaton on k-ary -trees, as defined in Definition

20, and t a k-ary -tree. A run, r(A, t), of A on t is a partial k-ary -tree defined inductively as follows. For all directions , and for all nodes of r(A, t), u has at most one outgoing edge labelled with d, and leading to the d-successor ud of u. The label of the root belongs to Litconstr—in other words, . If u is a node of r(A, t) of level , with label , then calculate distLast(h))), where dist is a function associating with each pair of Litconstran element of L(Litconstrdefined inductively in the following way:

dist

4. the label of

A partial k-ary -tree is a run of A if there exists a k-ary -tree t such that is a run of A on t.

2. the CSP of , CSP, is the CSP whose set of variables,

An n-branch of a run is a path of length (number of edges) n beginning at the root of . A branch is an infinite path. If u is the terminal node of an n-branch , then the argument of the label of u is a set of n-histories. Following (Muller, Saoudi, and Schupp 1992), we say that each n-history in lies along . An n-history h lies along if there exists an n-branch of such that h lies along . An (infinite) history is a sequence h = . Given such a history, :

1. h lies along a branch if, for every , the prefix of h consisting of the n-history lies along the n-branch consisting of the first n edges of ;

2. h lies along if there exists a branch of such that h lies along ;

3. Q-proj(h) (the Q-projection of h) is the infinite word such that, for all , the n + 1-length prefix is the Q-projection of , the n-history which is the 2n + 1-prefix of h.

4. we denote by Inf(h) the set of states appearing infinitely often in Q-proj(h)

The acceptance condition is now defined as follows. A history h is accepting if Inf. A branch of r(A, t) is accepting if every history lying along is accepting.

The condition for a run to be accepting splits into two subconditions. The first subcondition is the standard one, and is related to (the histories lying along) the branches of , all of which should be accepting. The second subcondition is new: the CSP of , CSP, should be consistent. A accepts a k-ary -tree t if there exists an accepting run of A on t. The language L(A) accepted by A is the set of all k-ary -trees accepted by A.

Summarising the previous steps, especially the work of the procedure of Figure 1, we get the following corollary.

Corollary 1 Let x be a spatial RA of arity p, C an MTALCconcept, T an MTALCweakly cyclic TBox, the TBox T augmented with C, and the initial defined concept of is satisfiable w.r.t. T iff the language Laccepted by weak alternating automaton ALitconstron k-ary -trees is nonempty. The parameters of the automaton are as follows:

1. pConceptscFeatures(C, T), Q =

2. K is the set of relational existential concepts and abstract

3. is obtained from the axiom B .= E in

4. The set F of accepting states is the set of defined concepts in dConcepts(C, T) that are not evenuality defined concepts

5. Finally, the partial order on the states in Q is as computed by the procedure of of Figure 1.

We have investigated a spatio-temporalisation MTALCof the ALC(D) family of description logics with a concrete domain (Baader and Hanschke 1991), obtained by temporalising the roles, so that they consist of m + n immediate-successor (accessibility) relations, the first m being general, the other n functional; and spatialising the concrete domain, which is generated by an RCC8-like qualitative spatial language (D A Randell and Cui 1992; Egenhofer 1991). We have shown the important result that satisfiability of an MTALCconcept with respect to a weakly cyclic TBox can be reduced to the emptiness problem of a B¨uchi weak alternating automaton augmented with spatial constraints. In another work, complementary to this one, also submitted to this conference, we thoroughly investigate B¨uchi automata augmented with spatial constraints, and provide, in particular, a translation of an alternating into a nondeterministic, and a nondeterministic doubly depth-first polynomial space algorithm for the emptiness problem of the latter. Together, the two works provide an effective solution to the satisfiability problem of an MTALCconcept with respect to a weakly cyclic TBox. A future work worth mentioning is whether one can keep the same spatio-temporalisation and define a form of TBox cyclicity stronger than the one considered in this work, and

expressive enough to subsume the semantics of the well-

known mu-calculus.

[Artale and Franconi 2000] Artale, A., and Franconi, E. 2000. A Survey of Temporal Extensions of Description Logics. Annals of Mathematics and Artificial Intelligence 30(1-4):171–210.

[Baader and Hanschke 1991] Baader, F., and Hanschke, P. 1991. A scheme for integrating concrete domains into concept languages. In Proceedings of the 12th International Joint Conference on Artificial Intelligence, 452–457. Sydney: Morgan Kaufmann.

[Balbiani, Condotta, and del Cerro 1998] Balbiani, P.; Con- dotta, J.-F.; and del Cerro, L. F. 1998. A model for reasoning about bidimensional temporal relations. In Proceedings of Principles of Knowledge Representation and Reasoning (KR), 124–130. Trento, Italy: Morgan Kaufmann.

[Bettini 1997] Bettini, C. 1997. Time-dependent concepts: representation and reasoning using temporal description logics. Data & Knowledge Engineering 22:1–38.

[D A Randell and Cui 1992] D A Randell, A. G. C., and Cui, Z. 1992. Computing transitivity tables: A challenge for automated theorem provers. In Proceedings CADE 11. Berlin: Springer Verlag.

[Egenhofer 1991] Egenhofer, M. 1991. Reasoning about bi- nary topological relations. In in Computer Science, L. N., ed., SSD, volume 525, 143–160. Z¨urich, Switzerland: Springer.

[Emerson 1990] Emerson, E. A. 1990. Temporal and modal logic. In van Leeuwen, J., ed., Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, 995–1072. Elsevier and MIT Press.

[Frank 1992] Frank, A. U. 1992. Qualitative spatial reasoning about distances and directions in geographic space. Journal of Visual Languages and Computing 3:343–371.

[G¨usgen 1989] G¨usgen, H. 1989. Spatial reasoning based on Allen’s temporal logic. Technical report, ICSI, Berkley, CA.

[Haarslev, Lutz, and M¨oller 1999] Haarslev, V.; Lutz, C.; and M¨oller, R. 1999. A description logic with concrete domains and a role-forming predicate operator. Journal of Logic and Computation 9(3):351–384.

[Halpern and Moses 1985] Halpern, J. Y., and Moses, Y. 1985. A guide to the modal logics of knowledge and belief. In International Joint Conference on Artificial Intelligence, 480–490. Los Angeles, CA: Morgan Kaufmann.

[Isli and Cohn 1998] Isli, A., and Cohn, A. G. 1998. An Al- gebra for Cyclic Ordering of 2D Orientations. In Proceedings of the 15th American Conference on Artificial Intelligence (AAAI), 643–649. Madison, WI: AAAI/MIT Press.

[Isli and Cohn 2000] Isli, A., and Cohn, A. G. 2000. A new approach to cyclic ordering of 2D orientations using ternary relation algebras. Artificial Intelligence 122(1–2):137–187.

[Isli 2003] Isli, A. 2003. Bridging the gap between modal temporal logics and constraint-based QSR as an ALC(D) spatio-temporalisation with weakly cyclic tboxes. CoRR cs.AI/0307040.

[Ligozat 1998] Ligozat, G. 1998. Reasoning about cardi- nal directions. Journal of Visual Languages and Computing 9(1):23–44.

[Lutz 2001] Lutz, C. 2001. The Complexity of Description Logics with Concrete Domains. PhD thesis, LuFG Theoretical Computer Science, RWTH, Aachen.

[Mukerjee and Joe 1990] Mukerjee, A., and Joe, G. 1990. A qualitative Model for Space. In Proceedings of the American Conference on Artificial Intelligence (AAAI), 721–727. Los Altos: Morgan Kaufmann.

[Muller and Schupp 1987] Muller, D. E., and Schupp, P. E. 1987. Alternating automata on infinite trees. Theoretical Computer Science 54:267–276.

[Muller and Schupp 1995] Muller, D. E., and Schupp, P. E. 1995. Simulating alternating Tree Automata by nondeterministic Automata: New Results and new Proofs of the Theorems of Rabin, McNaughton and Safra. Theoretical Computer Science 141:69–107.

[Muller, Saoudi, and Schupp 1992] Muller, D. E.; Saoudi, A.; and Schupp, P. E. 1992. Alternating automata, the weak monadic theory of trees and its complexity. Theoretical Computer Science 97:233–244.

[Renz and Nebel 1999] Renz, J., and Nebel, B. 1999. On the complexity of qualitative spatial reasoning: a maximal tractable fragment of the region connection calculus. Artifi-cial Intelligence 108:69–123.

[Schild 1991] Schild, K. 1991. A correspondence theory for terminological logics: Preliminary report. In 12th International Joint Conference on Artificial Intelligence, 466–471. Sydney: Morgan Kaufmann.

[Schmidt-Schauss and Smolka 1991] Schmidt-Schauss, M., and Smolka, G. 1991. Attributive concept descriptions with complements. Artificial Intelligence 48(1):1–26.