无限对象上的自动机

无限对象上的自动机读取永不结束的输入，例如无限字或无限树，并根据哪些状态或转换被无限次访问来接受输入，为推理持续的、非终止的系统提供了数学工具。

Definition

ω-自动机是一种有限状态机，其运行是无限的，接受条件由无限次访问的状态集合定义；此类自动机识别无限字或树的集合，称为ω-正则语言。

Scope

本主题涵盖无限字上的Büchi、Muller、Rabin和奇偶自动机，区分它们的接受条件，确定化和补集化结果，无限树上的自动机，以及这些自动机、一阶逻辑和用于综合与验证的无限博弈之间的深层联系。

Core questions

• 有限机器如何接受或拒绝没有结束的输入？
• 为什么非确定性Büchi自动机和确定性Büchi自动机在表达能力上有所不同？
• 无限对象上的自动机与用于指定系统行为的逻辑有何关系？
• 这些自动机的补集化为何困难，以及为何重要？

Key theories

Büchi接受和ω-正则语言

当某个接受状态被无限次访问时，Büchi自动机接受一个无限字，并且由此识别的语言（ω-正则语言）与自然数上的一阶逻辑中可定义的语言一致。

确定化和奇偶条件

非确定性Büchi自动机通常无法在不改变接受条件的情况下确定化，但Safra的构造将其转换为确定性Rabin或奇偶自动机，这对于补集化和解决博弈至关重要。

Clinical relevance

ω-自动机是模型检测的算法核心：反应系统和时态逻辑属性分别被转换为无限字上的自动机，检查属性归结为非空性测试，从而实现硬件、协议和并发软件的自动化验证。

History

Büchi在大约1960年引入了无限字上的自动机，以判定自然数的一阶逻辑理论；McNaughton展示了如何通过更强的接受条件来确定化它们；Rabin将该理论扩展到无限树。这些结果在1970年代后期时态逻辑进入计算机科学后，成为验证的核心。

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

机器如何接受无限输入？

接受的定义不是通过到达最终状态（因为没有最终状态），而是通过哪些状态重复出现。例如，Büchi自动机在其无限运行期间，当它无限次地通过一个指定的接受状态时，就接受输入。

为什么这些自动机对验证很重要？

操作系统和网络协议等非终止系统自然地通过无限行为进行建模。诸如“系统永不发生死锁”或“每个请求最终都会得到服务”之类的属性成为ω-正则语言，因此检查它们归结为模型检测器可以自动执行的自动机操作。