Extensions of ω-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are ill-suited to act on this information, and register automata have intricate formal semantics and issues with tractability. We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions. Whenever a transition with an obligation is taken, the obligation is evaluated against the current symbol and yields a constraint on the next symbol that the automaton will read. We formalize obligation automata with existential and universal branching and Emerson-Lei acceptance conditions, which subsume classic families such as Büchi, Rabin, Strett, and parity automata. We show that these automata recognise a strict superset of ω-regular languages. To illustrate the practicality of our proposal, we also introduce a machine-readable format to express obligation automata and describe a tool implementing several operations over them, including automata product and emptiness checking.

翻译：将ω-自动机扩展至无限字母表时，通常依赖符号守卫来保持转移关系的有限性，并利用寄存器或存储单元来保存过往符号的信息。仅凭符号转移难以有效处理这些信息，而寄存器自动机则具有复杂的形式语义及可处理性问题。我们提出一种基于义务的略有不同的方法，义务即附加于转移的类赋值构造。每当执行带有义务的转移时，该义务会根据当前符号进行计算，并产生对自动机即将读取的下一个符号的约束。我们形式化了具有存在性与全称分支以及Emerson-Lei接受条件的义务自动机，其涵盖了经典自动机族，如Büchi、Rabin、Streett和奇偶自动机。我们证明这些自动机可识别严格超集于ω-正则语言的集合。为说明本方法的实用性，我们还引入了一种机器可读格式来表达义务自动机，并描述了一个工具，该工具实现了对它们的多种操作，包括自动机乘积和空性检查。