一句话：引入正则交替名义自动机，证明无界寄存器下非空与包含仍为初等复杂度，并几乎完全去交替化。
无限字母表上的形式语言可抽象带数据结构和进程。经典寄存器自动机或等价的名义轨道有限自动机在推理上常难解甚至不可判定，除非限制控制能力或寄存器数；带名字分配的正则非确定性名义自动机可在无界寄存器下以初等复杂度判定包含。本文把控制能力扩展到交替，引入正则交替名义自动机（RANAs），研究其非空性与包含问题。结果表明：即使寄存器数无界，这两类问题仍具初等复杂度；RANAs 可几乎完全去交替化，即仅余一个死锁的全称状态。作为推论，有限数据字上的 Bar-µTL 某类模型的模型检测复杂度提升一个指数层级。
Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-µTL, a fixed-point logic with name allocation over finite data words, by one exponential level.
DOI 原文 ·
@inproceedings{paperbot8672,
title = {Alternating Nominal Automata with Name Allocation},
author = {Florian Frank and Daniel Hausmann and Stefan Milius and Lutz Schröder and Henning Urbat},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00012}
}