A spatio-temporalisation of ALC and its translation into alternating automata augmented with spatial constraints

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. To achieve this, we consider a spatio-temporalisation MTALC(Dx), of the well-known ALC(D) family of Description Logics (DLs) with a concrete domain: the MTALC(Dx) concepts are interpreted over infinite k-ary Sigma-trees, with the nodes standing for time points, and Sigma including, additionally to its uses in classical k-ary Sigma-trees, the description of the snapshot of an n-object spatial scene of interest; the roles split into m+n immediate-successor (accessibility) relations, which are serial, irreflexive and antisymmetric, and of which m are general, not necessarily functional, the other n functional; the concrete domain Dx is generated by an RCC8-like spatial Relation Algebra (RA) x, and is used to guide the change by imposing spatial constraints on objects of the "followed" spatial scene, eventually at different time points of the input trees. In order to capture the expressiveness of most modal temporal logics encountered in the literature, we introduce weakly cyclic Terminological Boxes (TBoxes) of MTALC(Dx), whose axioms capture the decreasing property of modal temporal operators. We show the important result that satisfiability of an MTALC(Dx) concept with respect to a weakly cyclic TBox can be reduced to the emptiness problem of a Buchi weak alternating automaton augmented with spatial constraints. In another work, complementary to this one, also submitted to this conference, we thoroughly investigate Buchi 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.