带义务的符号ω-自动机

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