INFDok - Dokumentenvolltextserver des Fachbereichs Informatik

Kurzfassung auf Englisch:

The aim of this work is to provide a family of qualitative theories for spatial change in general, and for motion of spatial scenes in particular. Motion of an n-object spatial scene is seen as a change (over time) of the (qualitative) spatial relations between the different objects involved in the scene --if, for instance, the spatial relations are those of the well-known Region-Connection Calculus RCC8, then the objects of the scene are seen as regions of a topological space, and motion of the scene as a change in the RCC8 relations on the different pairs of the objects. To achieve this, we consider a spatio-temporalisation MTALC(D_x), of the well-known ALC(D) family of Description Logics (DLs) with a concrete domain: the MTALC(D_x) concepts are interpreted over infinite k-ary trees, with the nodes standing for time points; the roles split into m+n immediate-successor (accessibility) relations, which are antisymmetric and serial, and of which m are general, not necessarily functional, the other n functional; the concrete domain D_x is generated by an RCC8-like spatial Relation Algebra (RA) x. The (long-term) goal is to design a platform for the implementation of flexible and efficient domain-specific languages for tasks involving spatial change. In order to capture the expressiveness of most modal temporal logics encountered in the literature, we introduce weakly cyclic Terminological Boxes (TBoxes) of MTALC(D_x), whose axioms capture the decreasing property of modal temporal operators. We show the important result that satisfiability of an MTALC(D_x) concept with respect to a weakly cyclic TBox is decidable in nondeterministic exponential time, by reducing it to the emptiness problem of a weak alternating automaton augmented with spatial constraints, which we show to remain decidable, although the accepting condition of a run involves, additionally to the standard case, consistency of a CSP (Constraint Satisfaction Problem) potentially infinite. The result provides a tableaux-like satisfiability procedure which we will discuss. Finally, given the importance and cognitive plausibility of continuous change in the real physical world, we provide a discussion showing that our decidability result extends to the case where the nodes of the k-ary tree-structures are interpreted as (durative) intervals, and each of the m+n roles as the 'meets' relation of Allen's RA of interval relations.