💻 computer science

Kofola 1.0: A Modular Approach to {\omega}-Regular Complementation and Inclusion Checking (Technical Report)

本文介绍了 Kofola，这是一种高效且稳健的工具，它采用模块化框架将 Büchi 自动机分解为强连通分量，以进行定制化的补运算和包含性检查，并通过即时空性检查和新启发式方法，展现出优于最先进工具的性能。

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

发布于 2026-05-18

📖 1 分钟阅读☕ 轻松阅读

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

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

想象你是一家庞大且无限的工厂的质量检验员。这家工厂生产着无尽的“产品流”（在计算机科学中称为“单词”）。你拥有两台机器：机器 A和机器 B。

你的任务是回答一个非常棘手的问题：“机器 A 生产的每一个产品，是否也都由机器 B 生产？”

如果答案是“是”，那么机器 A 可以安全使用。如果机器 A 生产的任何一个产品是机器 B从未生产过的，那么机器 A 就是不安全的。

这就是语言包含性检查的核心问题。它是验证计算机软件和硬件行为是否正确的一项基本任务。然而，由于产品流是无限的，人工检查是不可能的。你需要一个超级聪明的机器人来完成这项工作。

现在登场的是Kofola，这是一款专为解决此问题而设计的全新、高效机器人。以下是其工作原理，分解为简单的概念：

1. 旧方法 vs. Kofola 方法

以前，试图解决此问题的机器人必须同时审视整个工厂车间。它们会尝试构建机器 A 可能采取的所有路径的巨型地图，并将其与机器 B 进行比较。这张地图如此巨大，往往会导致机器人的大脑“爆炸”（即所谓的“状态空间爆炸”问题）。

Kofola 的独门秘籍：模块化方法
Kofola 不像以前那样一次性审视整个工厂，而是一位精通组织的专家。它审视机器 B 并指出：“这家工厂并非一团乱麻；它实际上是由不同的‘街区’组成的。”

Kofola 将机器 B 分解为强连通分量（SCCs）。你可以将这些分量想象成工厂中的不同房间或区域：

死胡同：机器停止生产产品的房间。
简单循环：机器在其中转圈、重复做同一件事的房间。
确定性区域：机器在每一步只有一个选择的房间（就像单轨上的火车）。
混沌区域：机器有多种选择、可以朝不同方向移动的房间（就像迷宫）。

Kofola 对每个“街区”采用不同的处理方式。它对简单循环使用专门的轻量级工具，而对混沌区域则使用重型工具。它不会浪费精力试图用大锤去解决简单的部分。

2. 新的"IADAC"发现

该论文介绍了一种新型街区，称为IADAC（初始几乎确定性接受分量）。

类比：想象一条走廊通向一个房间。走廊是一条笔直的单行道（确定性）。一旦你进入房间，你可能会有选择。但关键在于：一旦你离开那个房间，就再也无法回到走廊。
重要性：由于走廊如此可预测，Kofola 可以使用一种非常快速、轻量级的方法来检查它，而不需要处理混沌部分所需的那种笨重、缓慢的方法。这是作者识别并针对其进行优化的新型区域。

3. “懒惰”检验员（即时检查）

通常，为了检查工厂是否安全，你必须先构建工厂的完整地图，然后才能说“安全”或“不安全”。

Kofola 是极度懒惰的（这是好事）。它开始构建地图，但一旦发现足以做出决定的证据，它就立即停止。

如果它早期就发现了一个“坏产品”，它会立即大喊“不安全！”并停止工作。
如果答案已经明确，它就不会浪费时间去绘制工厂的其余部分。

这是通过一种新的“空性检查”算法实现的。想象你在黑暗的房间里寻找特定类型的漏洞。你不是打开整个房间的灯，而是只照亮你行走的路径。如果你发现了漏洞，你就停止。如果你走完了整条路径却没发现漏洞，你就知道房间是安全的。Kofola 在构建地图的同时，瞬间完成这一过程。

4. 结果：Kofola 赢得比赛

作者使用数千份真实的工厂蓝图，将 Kofola 与现有的最佳机器人（如 Spot、Rabit 和 Bait 等工具）进行了测试。

鲁棒性：Kofola 是唯一成功解决每一个测试用例而不会崩溃或耗尽内存的工具。其他工具在许多困难案例上失败了。
速度：在许多实际问题中，Kofola 不仅更快，而且快了几个数量级。在某些情况下，当其他工具在 2 分钟后仍在尝试构建地图时，Kofola 已在几分之一秒内完成。
规模：Kofola 构建的地图通常比竞争对手构建的地图更小、更紧凑。

总结

Kofola 是一种全新、超高效的工具，用于检查一个计算机系统是否“包含”在另一个系统之中。它的工作原理如下：

将问题分解为更小、更易于管理的“街区”。
为每种特定类型的街区使用正确的工具（包括它发现的一种新型街区）。
保持“懒惰”，一旦拥有足以给出答案的信息，就立即停止工作。

其结果是，该工具比目前可用的任何其他工具都更快、更可靠，并且能够处理更大、更复杂的问题。这是对计算机系统“质量控制”的重大升级。

技术摘要：Kofola 1.0——一种用于ω-正则补运算与包含性检查的模块化方法

问题陈述

Büchi 自动机（BAs）的语言包含性检查是自动机理论验证中的一个基本问题，在模型检测、监控和定理证明中具有关键应用。该问题是 PSpace 完全的，随着系统规范在规模和复杂性上的增长，其计算需求依然巨大。判定 $L_1 \subseteq L_2$ 可归约为检查 $L_1 \cap \overline{L_2}$ 的空性问题，其中 $\overline{L_2}$ 是 $L_2$ 的补集。这一归约带来了两个主要挑战：

紧凑的补运算：高效地构造补自动机 $\overline{L_2}$ ，同时避免状态空间爆炸。
高效的探索：探索通常极其庞大的 $L_1 \cap \overline{L_2}$ 乘积自动机。

现有工具主要依赖经典的基于 Ramsey 或基于确定化的补运算构造，这些方法的历史已超过三十年。尽管近期在补运算方面取得了进展，但它们尚未被完全整合到实用的包含性检查器中。

方法论

本文介绍了 Kofola，这是一个用 C++ 实现的高效工具，采用最先进的模块化补运算框架。该方法论基于将输入自动机分解为强连通分量（SCCs），并根据各分量的结构特性应用定制的补运算算法。

1. 结构分解与分量分类

Kofola 对需进行补运算的自动机（ $A_2$ ）执行细粒度的结构分析。它将最大强连通分量（SCCs）分类为四个不同的类别：

非接受分量：通过传统的子集构造处理。
固有弱接受分量（IWACs）：所有循环均接受的分量。
确定接受分量（DACs）：仅包含确定性转移的分量。
初始几乎确定接受分量（IADACs）：本文引入的一种新识别的分量类型。这些是确定性的 SCC，可通过确定性 SCC 从初始状态到达，仅在 SCC 之间的无环路径上允许非确定性。
非确定接受分量（NACs）：其余的接受 SCC。

2. 模块化补运算框架

针对每种分量类型，Kofola 应用专用的部分补运算算法：

IWACs：使用经典的 Miyano-Hayashi 构造，生成 $Inf(1)$ 接受条件。
DACs：使用 NCSB 算法的变体，生成 $Inf(2)$ 接受条件。
NACs：根据任务支持两种方法：
- 补运算：使用基于确定化的方法（Safra-Piterman 变体）以生成更小的自动机。
- 包含性检查：使用基于切片的方法，更适合在线的乘积空性测试。
IADACs：本文针对这些分量引入了一种新的部分算法。它使用子集构造对 IADACs 进行确定化，并在任何被追踪的运行遇到接受转移时发出拒绝标记（$Fin(0)$）。其正确性依赖于 IADACs 中运行受限的事实，这是由于其非确定性受到限制。

顶层算法同步这些部分构造。生成的补自动机是一个简单广义 Rabin 自动机（SGRA），具有单一形式的接受条件： $Fin(0) \land Inf(1) \land \dots \land Inf(k-1)$ 。

3. 在线空性检查

为了解决包含性检查中的状态空间爆炸问题，Kofola 采用了一种针对生成的 SGRA 的新型在线空性检查算法。

惰性构造：与需要显式构造完整乘积自动机的工具不同，Kofola 惰性探索状态空间。
算法：该算法是 Couvreur 算法的变体，并扩展了 $Fin$ 谓词。它执行深度优先搜索，管理转移集栈以检测 SCC。
终止：一旦探索的状态空间足以判定结果（即发现接受循环或证明空性），搜索即终止。这最大限度地减少了生成的补集部分，这一点至关重要，因为补运算是导致爆炸的主要来源。

主要贡献

Kofola 工具：一个用于 BA 补运算和语言包含性检查的高效、模块化工具。
IADAC 识别：引入并形式化了初始几乎确定接受分量（IADACs）作为一个独特的结构类别。
新补运算算法：针对 IADACs 的专用部分算法，生成 $Fin(0)$ 条件，从而能够构造单个广义 Rabin 对。
惰性空性检查：一种针对 SGRA 的新型在线算法，避免了显式的完整自动机构造，允许早期终止。
模块化框架：一种灵活的架构，允许基于结构分析同步组合不同的部分算法。

实验结果

作者将 Kofola 与最先进的工具进行了评估：Spot、Ranker、Owl、Bait、Forklift 和 Rabit。

补运算基准测试

数据集：来自多样化来源的 31,273 个自动机（程序终止、Sturmian 词逻辑、超性质、S1S、LTL 翻译以及随机生成）。
鲁棒性：Kofola 是唯一成功补运算所有 31,273 个输入自动机的工具。鲁棒性次之的工具 Spot 因内存限制在 2 个实例上失败。
规模：与 Spot（115.38 个状态）和 Ranker（45.80 个状态，尽管 Ranker 在 443 个实例上失败）相比，Kofola 平均生成了显著更小的补自动机（79.24 个状态）。
性能：Kofola 解决了最多的实例，并且在运行时间上经常比竞争对手快几个数量级。

包含性检查基准测试

数据集：来自程序终止、并发系统验证、超性质模型检测和定理证明的 1,014 个包含性问题。
性能：Kofola 解决了最多的实例（仅 2 个未解），并且具有最低的总运行时间（已解决问题为 141 秒）。
比较：Kofola 在 263 个实例上严格胜过 Spot(Det)，仅输掉 0 个。它显著优于基于 Ramsey 的工具（Bait、Forklift、Rabit），后者通常需要多一个数量级的时间。
观察：包含性查询右侧（即被补运算的）自动机中，98% 是电梯自动机（不包含 NACs），这突显了利用结构特性的实际相关性。

意义与主张

本文声称，Kofola 为 BA 补运算和包含性检查的效率与鲁棒性确立了新标准。其意义在于：

实用性：它将现代的、基于分解的补运算技术引入实用的包含性检查，超越了经典构造。
可扩展性：通过将结构分解与惰性在线空性检查相结合，它有效地缓解了状态空间爆炸，解决了现有工具无法处理的实例。
可扩展性：模块化架构允许针对特定分量类型集成新的部分补运算算法。

作者将 Kofola 定位为不仅仅是渐进式的改进，而是一款极具竞争力的工具，在源自实际应用的基准测试中，其性能往往比最先进的解决方案快几个数量级。