通过路线图理解自动机理论

I’m happy to help translate the article, but I need the text you’d like translated. Could you please paste the content (or the portion you want translated) here? Once I have the text, I’ll provide the Simplified Chinese translation while keeping the source link and formatting intact.

Source: …

正式验证与自动机理论

正式验证是一种用于保证软件行为正确的技术。在正式验证中，系统的行为被数学建模，必须满足的规范则以逻辑公式的形式表达。

与仅仅列出状态不同，正式验证的目标是：

• 将规范表示为数学模型
• 机械地判断这些规范是否始终得到满足或被违反
• 保证安全性，包括那些通过测试容易遗漏的情况

自动机理论被用作实现这些目标的工具。

为什么自动机会让人感到压倒性

在该领域，诸如 DFA、NFA、NBA、LTL 等技术术语接连出现，容易让人困惑。诸如“状态转移”“非确定性”“无限执行”等抽象概念乍看之下可能并不容易理解。

使用 火车线路图 的类比来可视化这些概念，有助于直观地理解正式验证的工作原理。

目标受众

• 刚在大学开始学习自动机理论或正式验证的学生
• 在模型检查或 LTL 课程中感到“我大概懂了，但还是没有真正领会”的学习者
• 对系统验证感兴趣的工程师

两个基本视角

在理解自动机时，实际上只需要记住 两个维度：

通过组合这两个维度，理论上可以将自动机划分为四类：

确定性、非确定性以及无限执行的含义将在后面的具体示例中解释。

注意： DBA（确定性 Büchi 自动机）——处理确定性的无限执行——在此将不作讨论，因为从表达能力和实际用途的角度来看，它很少被需要。

Source: …

最简情况：DFA（确定性有限自动机）

DFA 是最直观的自动机。在路线图类比中，它对应于 单线路线。

示例路线

Start ──Green Line──► G0 ──Green Line──► Goal

特征

• 站点（状态）： Start、G0、Goal
• 轨道（转移）： 从每个站点到下一个站点的连接
• 票（输入）： “乘坐 Green Line” 的操作

关键点：当你位于某个站点时，恰好只有一个 下一站可以前往。如果你从 Start 乘坐 Green Line，你总是会到达 G0。不存在其他选择。

正式定义

DFA 是一个 5‑元组

[ A = (Q,; q_0,; \Sigma,; \delta,; F) ]

这个定义可以可视化为 状态转移图。在教材中，图本身常被称为“自动机”。严格来说，自动机 是整个元组；多个此类元组统称为 自动机（automata）。

扩展到 NFA（非确定性有限自动机）

DFA 中的 “D” 代表 Deterministic（确定性）；将其换成 Nondeterministic（非确定性） 就得到 NFA。此时可能出现 多个可能的下一状态。

路线图类比

Start ──Green Line──► G1 ──Green Line──► Goal
          │
          └─Blue Line──► B1 ──(Green/Blue)──► Goal

• 从 Start 可以前往 G1（绿色） 或 前往 B1（蓝色）。
• 从 G1 可以直接到达 Goal（绿色） 或 到达 B1（蓝色）。
• 从 B1 你可以再次在 G1 和 Goal 之间选择。

Nondeterminism（非确定性） 意味着当前并未确定具体走的路线。若 至少有一条 可能的路径能够到达接受状态，则 NFA 接受该输入。

Source: …

NBA（非确定性 Büchi 自动机）——处理无限执行

NBA 将 NFA 扩展以处理 无限行为。在路线图类比中，这对应于可以 永远循环 的 环线。

示例：环线

S0 ──► S1 ──► S2 ──► … ──► S7 ──► S0 (repeat)

• 这条线路只有 8 个站点（有限），但你可以 无限次 环绕（无限时间）。

NBA 正好捕捉了这种无限执行。许多程序和系统“一旦启动就会永远运行”，因此对它们进行推理需要使用 NBA。

重要提示： 无限性 体现在 执行时间 上，而不是状态数量。NBA 使用 有限 的状态集合来表示 无限时间 的行为。

核心观点回顾

1. 确定性 vs. 非确定性
2. 有限 vs. 无限执行

当我第一次学习自动机时，我把第 1 点和第 2 点混淆了，错误地认为无限执行必然意味着无限多个不同的结果。实际上，即使可能的转移很多，只要把转移适当地归类，状态的数量仍然是有限的。

我们并不是在“把无限变成有限”。
我们是在使用状态数为 有限 的自动机，使 无限时间行为可判定。

红绿灯示例

红绿灯有三种状态

状态转换如下：

[Green]  --time passes-->  [Yellow]  --time passes-->  [Red]  --time passes-->  [Green]  --> …

这形成了一个无限循环。

如果我们将红绿灯表示为 确定性有限自动机 (DFA)，则每一时刻的状态都是确定的。例如，当当前状态是 Green 时，下一状态必定是 Yellow。

由于红绿灯会永远运行下去，将其建模为 非确定性 Büchi 自动机 (NBA) 是自然的选择。无限循环 Green → Yellow → Red → Green → … 可以仅用三个状态来表达。

从系统行为到规范

到目前为止，我们已经描述了系统如何行为。
下一步是检查系统是否行为正确。为此我们使用线性时序逻辑（LTL）。

LTL 是一种用于编写关于时间的规范的逻辑。使用路线图类比，它描述“操作规则”；对于交通信号灯，它描述“颜色变化的规则”，使用符号运算符来书写。

LTL 运算符

注意：全局（Globally）和最终（Finally）并非原始运算符；它们可以由 U 和否定（¬）推导得到。

G p ≡ ¬F ¬p
F p ≡ true U p

通过组合这些运算符，我们可以表达复杂的时序属性。

交通灯的 LTL 规范示例

1. “一旦红灯亮起，随后必须点亮绿灯。”

   G (Red → X Green)

2. “不存在红灯和绿灯同时亮起的状态。”

   G ¬ (Green ∧ Red)

3. “无论经过多长时间，绿灯都应不断重复出现。”

   GF Green          // always eventually green

LTL 对人类来说易于编写，但计算机需要一种更易于机械处理的形式：NBA。

将 LTL 转换为 NBA

已经在数学上证明，任何 LTL 规范都可以转换为等价的 NBA（因为 LTL 属于 ω‑正则语言 类）。

示例: 规范 “绿色无限次出现” (GF Green) 可以转化为以下 NBA：

S1 (start) ──[¬Green]──► S1
   │
   └─[Green]──► S2 ──► S1

• 在 S1，自动机检查当前符号是 Green 还是 not Green。
• 如果看到 Green，它会转到 S2，接受该出现，然后在下一步返回 S1。
• 如果看到 not Green，它会停留在 S1。

该 NBA 正好接受那些 Green 无限次出现的运行。

模型检查过程

1. 将实际系统表示为状态转移图（或 NBA）。
2. 用 LTL 编写规范。
3. 将 LTL 公式转换为 NBA。
4. 对系统 NBA 与规范 NBA 取乘积。
5. 在乘积自动机中搜索接受的无限路径。

如果存在这样的路径，则它是一个 反例（错误）。
如果不存在接受路径，则系统满足规范。

红绿灯示例

Source: …

为什么形式化验证很重要

• 错误检测： 彻底探索时序相关和罕见情况的错误，这类错误在传统测试中难以发现。
• 安全保证： 在安全关键领域（例如航空、医疗设备），我们需要数学证明系统不存在错误。
• 规范澄清： 用 LTL 编写需求会迫使对系统必须保证的内容进行精确、无歧义的定义。

通过使用路线图类比，自动机理论中的专业术语变得更直观。虽然形式化验证乍看之下可能令人生畏，但其本质其实很简单：

1. 描述系统的行为（自动机）。
2. 描述它必须满足的规则（LTL → NBA）。
3. 机械化检查（乘积自动机 + 空性测试）。

理解自动机是为此目的而使用的工具后，整个主题会变得更加易于接受。

给傻瓜的自动机理论基础（由傻瓜编写）

基于自动机的线性时间属性和线性时序逻辑（LTL）表示