一句话：提出一种数据树自底向上交替自动机，证明其刻画垂直 XPath，并给出可满足性判定。
数据树是每个节点带有限字母表标签和无限域数据值的有限树。论文引入一种非排序数据树上的新自动机模型，其本质是带有一个寄存器的自底向上交替自动机；该寄存器可保存一个数据值，并能与当前节点子树中出现的数据值进行相等测试。该模型具有可判定的空性问题。作者进一步证明，该自动机恰好刻画 XPath 的垂直片段——包含 child、descendant、parent 和 ancestor 轴——的表达力，从而得到该片段可满足性问题的判定过程。关键结果是自动机与查询逻辑片段之间的精确对应，以及由此导出的可判定性。
A data tree is a finite tree whose every node carries a label from a finite alphabet and a datum from some infinite domain. We introduce a new model of automata over unranked data trees with a decidable emptiness problem. It is essentially a bottom-up alternating automaton with one register that can store one data value and can be used to perform equality tests with the data values occurring within the subtree of the current node. We show that it captures the expressive power of the vertical fragment of XPath - containing the child, descendant, parent and ancestor axes - obtaining thus a decision procedure for its satisfiability problem.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FigueiraS11,
title = {Bottom-up automata on data trees and vertical XPath},
author = {Diego Figueira and Luc Segoufin},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:5)2017}
}