具有记忆与约束的显式树自动机
计算机科学中的逻辑
2015-07-01 v2
摘要
具有单一记忆的树自动机于 2001 年被引入。它们推广了下推（字）自动机以及 Bogaert 和 Tison 提出的具有兄弟节点相等约束的树自动机。尽管该模型具有可判定的空性问题，但其主要弱点是缺乏良好的封闭性质。我们提出将 Alur 和 Madhusudan 的显式下推自动机推广为一类树识别器，这类识别器在其（自底向上）计算过程中携带一个具有树结构（而非符号栈）的辅助无界记忆。换言之，这些被称为具有记忆的显式树自动机 (VTAM) 的识别器定义了一个具有布尔封闭性质的单记忆树自动机子类。我们特别证明了它们可以被确定化，并且对于 VTAM，空性、成员资格、包含性和通用性等问题都是可判定的。此外，我们提出了 VTAM 的几种扩展，其转换可能受到记忆之间不同类型的测试约束，以及类似于 Bogaert 和 Tison 的约束，用于比较输入树中的兄弟子树。我们证明了某些这类受约束的 VTAM 类保持了良好的封闭性和可判定性性质，并通过相关的树语言示例展示了它们的表达能力。
引用
@article{arxiv.0804.3065,
title = {Visibly Tree Automata with Memory and Constraints},
author = {Hubert Comon-Lundh and Florent Jacquemard and Nicolas Perrin},
journal= {arXiv preprint arXiv:0804.3065},
year = {2015}
}
备注
36 pages including an appendix