一句话：提出带极值约束的无限树寄存器自动机，证明其空性问题可判定，并用于二变量逻辑。
本文引入一种在无限树上运行的寄存器自动机，并为其增加极值约束。该自动机可将线性序域中的元素存入寄存器，并能将寄存器值与子树中寄存器值的上确界和下确界进行比较。作者研究该模型的关键判定问题——空性问题，并证明它是可判定的。标题还表明该模型可应用于二变量逻辑，为相关逻辑结果提供自动机工具。由于摘要未给出具体证明构造与复杂度，本文的核心贡献是模型定义与空性可判定性定理。
We introduce a model of register automata over infinite trees with extrema constraints. Such an automaton can store elements of a linearly ordered domain in its registers, and can compare those values to the suprema and infima of register values in subtrees. We show that the emptiness problem for these automata is decidable.
DOI 原文 ·
@inproceedings{paperbot5507,
title = {Register Automata with Extrema Constraints, and an Application to Two-Variable Logic},
author = {Szymon Toruńczyk and Thomas Zeume},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394748}
}