论文标题
ALC（D）的时空化及其转换为交替的自动机，并具有空间约束
A spatio-temporalisation of ALC(D) and its translation into alternating automata augmented with spatial constraints
论文作者
论文摘要
这项工作的目的是为一般的空间变化提供一个定性理论，特别是为空间场景的运动提供。 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 N-Objignt空间感兴趣的空间场景的快照；分为串行，反射性和反对称性的M+n立即成果（可访问性）关系，其中m是一般的，不一定是功能性的，是其他n个功能。混凝土域DX是由RCC8样的空间关系代数（RA）X生成的，并用于通过对“遵循”空间场景的对象施加空间约束来指导变化，最终在输入树的不同时间点处。为了捕获文献中遇到的大多模态时间逻辑的表现力，我们引入了MTALC（DX）（DX）的弱环状术语盒（Tboxes），其公理捕获了模态暂时算子的降低特性。我们表明的重要结果是，MTALC（DX）概念相对于弱环状Tbox的满意度可以降低为Buchi弱交替自动机的空虚问题，并具有空间约束。在这项会议上也提交给这项会议的另一项工作中，我们彻底调查了布奇自动机，并以空间约束的形式增加了，尤其是将交替转换为非确定性的翻译，以及解决后者空虚问题的有效决策程序。
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.
