作用域 MSO、寄存器自动机与表达式：数据词上的等价性
计算机科学中的逻辑
2026-02-16 v1
摘要
本文在无限字母域上建立了基于 MSO 逻辑和表达式的 nondeterministic register automata with guessing（NRA）语言的描述理论。我们引入 Scoped MSO，这是一种包含新型段落模态且对数据比较具有语法限制的逻辑。我们证明了该逻辑在可消除“强 guessing”的数据域上与 NRA 等价。进一步，我们定义 Data-Regular Expressions，这是一种基于量词-free 区域并具备 -contracting 连接的极简正则表达式计算器，证明其在任意关系结构上与 NRA 等价。这些形式化方法共同提供了一种强大的描述性理论，用于解释寄存器自动机，弥合了自动机、逻辑和表达式之间的鸿沟。
引用
@article{arxiv.2602.13120,
title = {Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words},
author = {Radosław Piórkowski},
journal= {arXiv preprint arXiv:2602.13120},
year = {2026}
}