一句话：引入带极值约束的无限树寄存器自动机，证明其空问题可判定，并用于二变量逻辑可满足性。
论文研究无限树上的寄存器自动机：自动机可将线性序域中元素存入寄存器，并能把寄存器值与子树中寄存器值的上确界和下确界比较。作者提出带极值约束的寄存器自动机模型，并证明其空问题可判定。作为应用，论文证明在同时存在树序、线性序以及可由树序 MSO 定义的任意原子时，二变量逻辑的可数可满足性问题可判定；由此推出，带任意谓词且其中两个谓词解释为线性序的二变量逻辑，其可满足性问题可判定。
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. As an application, we prove decidability of the countable satisfiability problem for two-variable logic in the presence of a tree order, a linear order, and arbitrary atoms that are MSO definable from the tree order. As a consequence, the satisfiability problem for two-variable logic with arbitrary predicates, two of them interpreted by linear orders, is decidable.
@article{paperbot1712,
title = {Register Automata with Extrema Constraints, and an Application to Two-Variable Logic},
author = {Szymon Toruńczyk and Thomas Zeume},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:42)2022}
}