💻 computer science

Complementing Emerson-Lei Elevator Automata (Technical Report)

本文引入了将 Büchi 电梯自动机推广至更丰富接受条件的 Emerson-Lei 电梯自动机，并提出了一种与现有最先进工具相比，在渐近复杂度与实际效率上均有显著提升的补集算法。

原作者： Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

发布于 2026-06-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在管理一座巨大的、无限的图书馆，其中的每一本书都代表了一个计算机程序的可能未来。有些书描述的是“好”的未来（程序运行正确），而另一些书描述的是“坏”的未来（程序崩溃或陷入死循环）。

在计算机科学的世界里，我们使用被称为**自动机（automata）**的数学机器来对这些书进行分类。一种特定类型的机器——Emerson-Lei 自动机，就像是一个超级灵活的图书管理员。它可以处理非常复杂的规则来定义什么是“好”的书。例如，它可以规定：“如果一本书中无限多次出现‘成功’这个词，但‘错误’这个词只出现了几次，那么这本书就是好的。”

然而，这里有一个棘手的问题：有时我们需要寻找补集（complement）。这意味着我们需要一台机器来做完全相反的事情：它负责筛选出所有的“坏”书（即那些不符合上述标准的书）。对于一个通用的、灵活的图书管理员来说，这样做是非常困难且缓慢的，就像试图徒手在沙漠中寻找一颗特定的沙粒一样。

“电梯”的发现

论文的作者注意到，我们现实生活中使用的图书馆其实并非完全混乱。大多数时候，这些图书管理员都有一个特定的结构：他们的行为就像电梯。

想象一栋设有电梯的大楼：

大堂（非确定性部分）： 当你刚进入时，你可能会面临选择去乘哪部电梯。这有点混乱。
电梯井（确定性部分）： 一旦你进入了电梯并关上了门，路径就是固定的。你只能上升或下降，以一种可预测的方式运行。你不能突然决定跳到随机的楼层；电梯遵循着严格的轨道。

论文将这些称为“电梯自动机（Elevator Automata）”。作者发现，大多数现实世界的计算机验证问题实际上都看起来像这些电梯。它们有一个混乱的开始，但随后会进入一个可预测的、确定性的流程。

新的解决方案：更聪明的分类机器

论文介绍了一种为这些电梯自动机构建“补集”机器（即寻找“坏”书的机器）的新型、更快速的方法。

以下是他们新算法运作方式的类比：

旧方法（通用方法）：
想象一下，试图通过同时检查一本书可能采取的所有路径来筛选坏书，而不去辨别哪条路径是“电梯”路径。这就像是在蒙着眼睛驱赶一群猫。可能性的数量会爆炸式增长，使得整个过程极其缓慢且耗费内存。

新方法（电梯方法）：
作者的算法意识到：“嘿，一旦书进入了电梯井，路径就固定了！”因此，它不再去猜测所有疯狂的可能性，而是将任务拆分：

大堂阶段： 它会追踪开始时的混乱选择。
电梯阶段： 一旦路径进入“电梯井”，它就不再进行猜测。它知道规则是固定的。它使用一种巧妙的“检查点”系统（就像电梯门前的保安）来观察这本书是否违反了规则。

他们使用了名为**断点（breakpoints）**的技术。想象一群跑步者（书）进入赛道。算法设置了一个检查点。

如果一名跑步者看到了“坏”标志（特定的颜色），他们就会被移出小组。
如果小组人数变为空，算法会重置检查点并重新开始。
如果这种“重置”无限多次发生，则证明了所有可能的路径最终都撞到了“坏”标志。因此，这本书确定是“坏”的。

为什么这很重要

论文证明，通过使用这种“电梯”结构，用于寻找坏书的机器规模会比旧方法小得多。

结果： 他们开发了一个工具（称为 Kofola）来使用这种新方法。
对比： 他们将它与目前的行业标准工具（称为 Spot）进行了测试。
结果： 在几乎所有的测试用例中，他们的工具创建的机器都更小、更高效。这就像是从驾驶一辆笨重、耗油的卡车切换到驾驶一辆轻巧的电动汽车来完成同样的工作。

总结

简而言之，这篇论文在说：“我们意识到大多数计算机验证问题表现得像电梯一样（混乱的开始，固定的路径）。我们构建了一种全新的、超快速的方法，通过对固定路径部分进行差异化处理，来寻找‘坏’的结果。这使得数学计算变得简单得多，也让计算机程序运行得更快。”

这是一种在提高计算机验证工具效率方面的技术突破，特别是针对那些在现实世界软件测试中出现的特定类型问题。

技术摘要：补充 Emerson-Lei 电梯自动机

问题陈述

$\omega$ -自动机的补集运算是形式化方法中的一项基本操作，对于程序终止分析、时序逻辑（如 LTL、HyperLTL）的模型检测以及判定逻辑理论（如 S1S）等任务至关重要。然而，对通用 $\omega$ -自动机进行补集运算是非常困难的，通常会导致状态空间爆炸，使得实际的验证工作变得不可行。

虽然结构限制（如“电梯自动机”，即每个强连通分量要么是确定性的，要么是本质上弱的）已被证明能够为标准 Büchi 自动机实现更高效的补集运算，但这些优化尚未完全扩展到具有更丰富接受条件的自动机。Emerson-Lei 自动机（ELA）支持 Inf（无限多次）和 Fin（有限多次）谓词的任意布尔组合，提供了更高的简洁性和灵活性，但目前缺乏高效的、感知结构的补集算法。现有的针对非限制性 ELA 的算法面临着高渐近复杂度的问题，且在处理在实际应用中频繁出现的“电梯”结构的 ELA 时，缺乏实用的方法。

方法论

本文引入了 Emerson-Lei 电梯自动机 (ELEA)，这是将 Büchi 电梯自动机推广到 Emerson-Lei 接受框架的概念。作者提出了一种新型补集算法，利用 ELEA 的结构特性，实现了比通用 ELA 补集算法显著更优的复杂度界限。

该方法分为三个主要阶段：

具有特定条件的半确定性自动机 (ELSA)：
作者首先解决了 Emerson-Lei 半确定性自动机 (ELSA) 的补集问题，这类自动机的运行最终会进入一个确定性分量。他们为两种特定情况开发了构造方法：
- 广义 Rabin 对： 该算法结合了用于 Fin 条件的 Miyano-Hayashi 构造和用于 Inf 条件的 NCSB 算法。它利用宏状态结构 $(N, R, C, S_1, \dots, S_k, B)$ 来追踪非确定性部分 ( $N$ ) 和确定性部分的运行。确定性部分被拆分为追踪 Fin 违规的集合 ( $R$ ) 以及 Inf 违规和安全集合 ( $C$ 和 $S_i$ )。全局断点集 $B$ 确保所有运行都被无限次检查。
- 广义 Streett 对： 作为 Rabin 情况的对偶，该构造使用轮询调度计数器 ( $z$ ) 按顺序使所有 Streett 对中的条件失效。它在用于 Inf 条件的 NCSB 实例与多个用于 Fin 条件的 Miyano-Hayashi 实例之间复用集合。
针对任意 Emerson-Lei 条件的归纳程序：
为了处理 Inf 和 Fin 的任意布尔组合，作者引入了一种 树-宏状态 (tree-macrostate) 方法。被否定的接受条件 $\psi = \neg Acc$ 被表示为一个镜像其句法结构的树。
- 采样模式 (Sampling Mode)： 进入确定性分量的运行被非确定性地分配到对应于 $\psi$ 析言项的子树中。
- 检查模式 (Checking Mode)： 算法验证运行是否满足分配的子公式。对于 Inf 条件，使用断点集来确保无限访问；对于 Fin 条件，则确保运行避开特定的颜色。
- 优化措施： 文中详细介绍了旨在减少状态空间爆炸的几种优化方法：
  - 树-宏状态归一化 (Tree-Macrostate Normalization)： 当运行合并时，合并冗余的运行追踪。
  - 共享断点优化 (Shared Breakpoint Optimization)： 通过轮询调度，为多个 Inf 叶节点使用单个共享断点。
  - OR-FIN 优化 (OR-FIN Optimization)： 在析言中的 Fin 叶节点中顺序传播违规状态，以避免指数级的分支。
向完整电梯和非限制性自动机的扩展：
开发出的 ELSAs 技术被扩展到了完整的 ELEAs。作者指出，在实践中，许多非电梯自动机是“近似电梯”的（仅包含极少数非电梯 SCC）。他们的转换方法通过利用这些特性高效地处理这些自动机，因为大多数 SCC 已经是电梯组件。

主要贡献与结果

ELEAs 的定义： 本文正式定义了 Emerson-Lei 电梯自动机，将电梯自动机的概念推广到了丰富的接受条件。
改进的复杂度界限： 与已知最好的非限制性 ELA 算法相比，所提出的算法在 ELEA 的补集规模上实现了显著降低的渐近状态空间复杂度。
- 对于具有 $k$ 个对的广义 Rabin 对，补集大小被限制在 $(k+3)n$ （或第 3 节中呈现的一般情况下的 $(5+k)n$ ），而非限制性 ELA 的界限为 $O(n^{k}(0.76n)^{n})$ 。
- 论文中的表 1 提供了综合对比，显示了在各种条件（Büchi、Rabin、Streett、Parity 和 Emerson-Lei）下，相对于非限制性界限实现的指数级或多项式级的改进。
实际实现与评估： 该算法在工具 Kofola 中得到实现。通过与最先进的工具 Spot 进行实验对比，结果表明 Kofola 通常能生成尺寸小得多的补集。基准测试包括来自文献的 ELA、随机生成的广义 Rabin 自动机，以及由 LTL 转换而来的 ELA。

重要性与主张

作者声称，这项工作是实现对具有丰富接受条件的 Emerson-Lei 自动机进行补集、确定化以及测试通用性和包含性的实用算法的第一步。

其重要性在于弥合了理论上的简洁性（由 ELA 提供）与实际验证效率之间的差距。通过利用（如前人研究 [1] 所述）现实世界自动机中电梯组件的结构普遍性，作者提供了一种能够大幅减少补集运算中固有状态爆炸问题的方法。本文将此定位为一项基础性贡献，使得在不发明领域内已建立的新应用之外，能够更高效地处理使用复杂接受条件的系统模型验证工作流（如 LTL 模型检测、超属性验证）。

该工作的范围较为适度，严格专注于补集问题及其直接影响，同时也承认在实现 ELEA 所有操作的完整实用算法方面仍需进一步工作。