论文标题
Buchi自动机加强了空间约束：模拟与非确定性的交替并确定后者的空虚问题
Buchi automata augmented with spatial constraints: simulating an alternating with a nondeterministic and deciding the emptiness problem for the latter
论文作者
论文摘要
这项工作的目的是彻底研究具有空间约束的Buchi自动机。这种自动机的输入树是无限的k-ary sigma-Trees，节点代表时间点，Sigma（包括其在经典的K- Ary Sigma-Trees中）的用途，以及对N-Object n-Object Spatial感兴趣的空间场景的快照的描述。从类似RCC8的空间关系代数（RA）X的约束来对空间场景的对象施加空间约束，最终在输入树的不同节点上。我们表明，可以使用相同类型的经典buchi非确定自动机模拟带有空间约束的Buchi交替自动机，并使用空间约束增强。然后，我们为后一种自动机的空置问题提供了一个非确定性的双重深度第一多项式空间算法。我们的主要动机来自另一项作品，也提交了这次会议，该作品定义了具有混凝土领域的著名家族alc（d）的时空化：共同的两部作品提供了一个有效的解决方案，以解决方案的概念，即对弱循环循环的Tbox的概念。
The aim of this work is to thoroughly investigate Buchi automata augmented with spatial constraints. The input trees of such an automaton are 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 constraints, from an RCC8-like spatial Relation Algebra (RA) x, are used to impose spatial constraints on objects of the spatial scene, eventually at different nodes of the input trees. We show that a Buchi alternating automaton augmented with spatial constraints can be simulated with a classical Buchi nondeterministic automaton of the same type, augmented with spatial constraints. We then provide a nondeterministic doubly depth-first polynomial space algorithm for the emptiness problem of the latter automaton. Our main motivation came from another work, also submitted to this conference, which defines a spatio-temporalisation of the well-known family ALC(D) of description logics with a concrete domain: together, the two works provide an effective solution to the satisfiability problem of a concept of the spatio-temporalisation with respect to a weakly cyclic TBox.
