Eve位置语言：为Büchi自动机引入秩序
Eve-positional languages: putting order into Büchi automata
AI总结：
本研究提出一种基于受限非确定性Büchi自动机的新形式体系，刻画Eve位置ω-正则语言，补全既有研究的缺失结论，给出阶乘级规模膨胀的确定化方法，并证明其状态最优性。
摘要：
若一个ω-正则语言是Eve位置的，则在所有以该语言为目标的博弈中，存在玩家无需保留之前任何走步的信息即可实现最优策略。这一概念在验证、自动机理论与综合中发挥着关键作用。\n Casares与Ohlmann近期给出了ω-正则语言Eve位置性的若干刻画。为此，他们引入了ε-完全奇偶自动机的概念，并（在诸多结果中）证明：一个ω-正则语言是Eve位置的，当且仅当它可被某个确定性奇偶自动机的ε-完全化所识别。Colcombet与Idir在其工作基础上，得到了Eve位置性的一种更直接的代数刻画。\n 我们提出一种刻画Eve位置语言的新形式体系，它由非确定性Büchi自动机的一类限制构成。这一成果补全了Casares与Ohlmann工作中缺失的一个蕴含关系。随后我们利用该形式体系，给出了识别这类语言的非确定性Büchi自动机的确定化过程，其规模膨胀至多为阶乘级。我们还证明，对于字母表足够完全的语言，该构造在状态维度上是最优的。
英文摘要：
An $ω$-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis. Casares and Ohlmann recently gave several characterisations of Eve-positionality of $ω$-regular languages. For this, they introduce the notion of $\varepsilon$-complete parity automaton and show (among other results) that an $ω$-regular language is Eve-positional if and only if it can be recognised by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir built on their work, and obtained a more direct algebraic characterisation of Eve-positionality. We introduce a new formalism that characterises the Eve-positional languages, consisting of a restriction of non-deterministic Büchi automata. This allows us to complete a missing implication in Casares and Ohlmann's work. We then use this formalism to describe a determinization procedure for non-deterministic Büchi automata recognising such languages, with size blow-up at most factorial. We also show that this construction is state-wise optimal for languages over sufficiently complete alphabets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
