ALC(D) 的时空化及其向带空间约束的交替自动机的翻译
人工智能
2020-03-02 v1 形式语言与自动机理论
摘要
本工作的目标是提供一类关于空间变化（特别是空间场景运动）的定性理论。为此，我们考虑对著名的带具体域的描述逻辑（DLs）族 ALC(D) 进行时空化 MTALC(Dx)：MTALC(Dx) 概念在无限的 k 元 Sigma-树上进行解释，其中节点表示时间点，且 Sigma 除在经典 k 元 Sigma-树中的用途外，还包含对所关注 n 对象空间场景快照的描述；角色拆分为 m+n 个直接后继（可达）关系，它们是序列的、非自反的和反对称的，其中 m 个是一般的、未必是函数的，其余 n 个是函数的；具体域 Dx 由类 RCC8 的空间关系代数（RA）x 生成，并通过对“后续”空间场景中的对象施加空间约束（最终在输入树的不同时间点）来引导变化。为捕捉文献中遇到的大多数模态时序逻辑的表达能力，我们引入 MTALC(Dx) 的弱循环术语盒（TBoxes），其公理捕捉模态时序算子的递减性质。我们展示了重要结果：MTALC(Dx) 概念相对于弱循环 TBox 的可满足性可归约为带空间约束的 Büchi 弱交替自动机的空性问题。在另一项与本工作互补且也提交至本次会议的工作中，我们深入研究了带空间约束的 Büchi 自动机，并特别给出了交替自动机到非确定自动机的翻译，以及针对后者空性问题的有效判定过程。
引用
@article{arxiv.2002.12760,
title = {A spatio-temporalisation of ALC(D) and its translation into alternating automata augmented with spatial constraints},
author = {Amar Isli},
journal= {arXiv preprint arXiv:2002.12760},
year = {2020}
}
备注
See footnote 1 on the first page of the paper. arXiv admin note: substantial text overlap with arXiv:cs/0307040 and text overlap with arXiv:2002.11510