💻 computer science

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library

本文介绍了在 Lean 计算机科学库（CSLib）中形式化 Hennessy-Milner 逻辑（HML）的工作，该工作涵盖了语法、满足关系、指称语义及包含 Hennessy-Milner 定理在内的完整元理论，并强调其参数化设计、与 CSLib 基础设施的集成以及对自动化证明的支持。

原作者： Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

发布于 2026-02-18

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

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

这篇文章介绍了一个名为 CSLib 的“计算机科学数字图书馆”中的新成果。简单来说，作者们用一种叫 Lean 的“数学证明助手”（类似超级严谨的数学老师），把一种叫 Hennessy-Milner 逻辑（HML） 的理论彻底地、无懈可击地“翻译”成了计算机代码。

为了让你更容易理解，我们可以把这个过程想象成给复杂的交通系统制定“交通规则”并编写“自动驾驶验证器”。

1. 背景：什么是“带标签的转换系统”（LTS）？

想象一下，你正在玩一个巨大的迷宫游戏，或者观察一个复杂的交通网络。

状态（States）：就是迷宫里的每一个路口，或者交通网络里的每一个红绿灯位置。
标签（Labels）：就是路口的指示牌，比如“左转”、“右转”、“直行”。
转换（Transitions）：就是当你看到“左转”的牌子时，你从路口 A 移动到了路口 B。

在这个世界里，我们想知道：两个不同的路口（状态）是不是“本质上”一样的？ 比如，路口 A 和路口 B，虽然位置不同，但如果它们面对所有指示牌（左转、右转等）时的反应完全一样，那它们在逻辑上就是“双胞胎”。

2. 核心工具：Hennessy-Milner 逻辑（HML）

HML 就是一种用来描述和检查这些路口行为的“语言”。它就像是一个超级侦探，手里拿着两个特殊的放大镜：

钻石放大镜（⟨µ⟩）：意思是“只要有一条路能通向某个地方，且那个地方满足条件，我就满意”。（存在性：只要有一个就行）。
方框放大镜（[µ]）：意思是“所有能通向的地方，都必须满足条件，我才满意”。（全称性：必须全部通过）。

举个例子：

命题：“只要按‘左转’，就能到达一个有宝藏的地方。”（钻石）
命题：“只要按‘左转’，所有能到达的地方都必须有宝藏。”（方框）

3. 这个研究做了什么？（CSLib 中的形式化）

以前，数学家们虽然知道 HML 很厉害，但大多是在纸面上推导。这篇论文做的是：把这套理论彻底写进了计算机代码里，并让计算机亲自验证了所有逻辑。

作者们做了三件大事：

A. 建立“字典”和“语法” (Syntax & Semantics)

他们定义了 HML 的每一个单词和句子结构。就像在计算机里建了一个完美的词典，确保“左转”、“宝藏”、“所有”这些词在计算机眼里含义绝对清晰，没有歧义。

B. 验证“侦探”的准确性 (Correctness)

他们证明了：用 HML 语言写的规则，和实际观察到的迷宫行为是完全一致的。

比喻：就像你写了一本《迷宫检查手册》，然后证明这本手册里的每一条规则，都能精准地预测你在迷宫里实际会看到什么。

C. 证明“双胞胎定理” (The Hennessy-Milner Theorem)

这是最精彩的部分！

定理内容：如果一个迷宫网络是“有限”的（每个路口能通向的地方数量是有限的），那么：两个路口如果看起来完全一样（逻辑等价），那它们在行为上就绝对是“双胞胎”（强双模拟）；反之亦然。
比喻：
想象你在两个不同的城市（系统）里。
- 方法一（行为观察）：你试着在两个城市里走，看它们对“左转”、“右转”的反应是否完全同步。如果完全同步，它们就是双胞胎。
- 方法二（逻辑描述）：你写了一堆描述这两个城市的句子（比如“左转能到公园”、“右转不能到河边”）。如果这两个城市满足完全相同的所有句子，它们就是双胞胎。
- 论文的贡献：作者用计算机证明了，只要城市不是无限大的（每个路口出口有限），方法一和方法二得出的结论是一模一样的！ 这就像证明了“看长相”和“测指纹”在特定条件下能 100% 确认身份。

4. 为什么这很重要？（现实意义）

给软件做“体检”：现在的软件（比如自动驾驶、通信协议、区块链）越来越复杂。我们需要确保它们不会出 Bug。HML 就像一套完美的体检标准。
自动化验证：因为作者把这套逻辑写进了 Lean（一个能自动检查证明的数学工具），所以以后任何使用这套标准的软件，计算机都能自动帮你检查：“嘿，你的代码逻辑是完美的，没有漏洞！”
通用性：这个成果不是只针对某一个特定的迷宫，而是通用的。无论是交通系统、通信协议，还是复杂的并发程序，只要符合这个标准，都能用这套逻辑来验证。

总结

这就好比作者们在计算机里建造了一个“逻辑实验室”。
在这个实验室里，他们不仅重新发明了“交通规则”（HML），还亲自用超级计算机跑通了所有测试，证明了**“行为上的双胞胎”和“描述上的双胞胎”是完全等价的**。

这意味着，未来我们在设计复杂的计算机系统时，可以更加放心地使用这套逻辑工具，让计算机帮我们自动证明系统的安全性，就像给软件穿上了一层由数学证明编织的“防弹衣”。

以下是基于论文《Hennessy–Milner Logic in CSLib, the Lean Computer Science Library》的详细技术总结：

1. 研究背景与问题 (Problem)

背景：带标签的转换系统（Labelled Transition Systems, LTSs）是定义计算系统（如进程演算、通信协议、自动机等）操作行为的核心框架。Hennessy–Milner 逻辑（HML）是用于推理此类系统的基础模态逻辑。
核心定理：HML 最著名的成果是 Hennessy–Milner 定理，该定理指出：在图像有限（image-finite）的 LTS 中，两个状态满足完全相同的 HML 命题，当且仅当它们是强双模拟（strongly bisimilar）的。这一对应关系使得 HML 成为并发理论和模型检查的重要逻辑基础。
现有问题：尽管 HML 具有基础地位，但在定理证明器中，达到库级通用性（library-grade generality）的机械化形式化工作非常稀缺。现有的形式化工作通常局限于 HML 的变体或特定类型的 LTS，缺乏一个能够广泛集成、参数化且可重用的通用库。
目标：在 Lean 计算机科学库（CSLib）中构建一个通用、可重用且完全形式化的 HML 库，涵盖语法、满足关系、指称语义以及完整的元理论（包括 Hennessy–Milner 定理）。

2. 方法论 (Methodology)

该研究基于 Lean 4 定理证明器和 CSLib（Lean 计算机科学库）进行开发，主要方法论包括：

参数化设计：
- 定义是宇宙多态（universe-polymorphic）的，不依赖于具体的状态或标签类型，而是参数化于任意 State 和 Label 类型。
- 直接利用 CSLib 中已有的 LTS 基础设施（如 LTS 结构体、Tr 转换关系谓词）。
形式化组件：
1. 语法（Syntax）：定义了一个归纳类型 Proposition，包含 true, false, and, or, diamond（ $\langle\mu\rangle$ ）和 box（ $[\mu]$ ）。作者选择包含 false 但不包含显式否定算子的语法，以便通过递归定义满足关系，并通过函数推导否定。
2. 满足关系（Satisfaction Relation）：通过归纳定义 Satisfies 谓词（ $s \models \phi$ ），描述状态与命题之间的语义关系。
3. 指称语义（Denotational Semantics）：定义了一个函数 denotation，将每个命题映射为满足该命题的状态集合（Set State）。
4. 理论等价（Theory Equivalence）：定义状态的理论（满足的所有命题集合）及理论等价关系（TheoryEq）。
自动化证明策略：
- 大量利用 Lean 的自动化策略，特别是 grind 战术。由于 CSLib 和 Mathlib 提供了完善的集合论基础设施和定义注解，grind 能够自动处理大多数归纳证明中的繁琐案例（如展开定义、处理集合运算）。
集成与复用：
- 代码完全集成到 CSLib 的命名空间 Cslib.Logic.HML 中，确保下游项目（如自动机理论、CCS 演算）可以直接调用。

3. 关键贡献 (Key Contributions)

通用定义：提供了 HML 语法、满足关系和指称语义的宇宙多态定义，适用于任意 LTS。
完整的元理论形式化：
- 语义等价性：证明了归纳定义的满足关系与指称语义（状态集合）是等价的（Theorem 1）。
- 双模拟不变性：证明了双模拟状态在逻辑上不可区分（Theorem 2），即双模拟蕴含理论等价。
- Hennessy–Milner 定理：在图像有限（image-finite）的 LTS 上，证明了理论等价蕴含双模拟，从而确立了理论等价与双模拟的等价性（Theorem 3）。
CSLib 集成：
- 提供了完善的文档和 API。
- 直接应用于 CSLib 中定义的自动机理论和通信系统演算（CCS），证明了这些系统继承 HML 的元理论结果。
代码可用性：所有代码已开源，并在 Lean 4.28.0-rc1 上验证通过。

4. 主要结果 (Results)

语义一致性：成功证明了 $s \models \phi \iff s \in \llbracket \phi \rrbracket$ ，确保了归纳语义与指称语义的一致性。
Hennessy–Milner 定理的机械化：
- 在图像有限条件下，证明了 TheoryEq 本身就是一个双模拟关系。
- 证明技巧：对于图像有限的状态，如果 $s_1$ 和 $s_2$ 理论等价但 $s_1$ 能执行 $\mu$ 动作到达 $s_1'$ ，而 $s_2$ 无法匹配，则利用图像有限性收集 $s_2$ 的所有 $\mu$ -后继，构造一个区分命题 $\langle\mu\rangle \bigvee \phi_i$ ，从而导出矛盾。这一证明过程在 Lean 中得到了完整形式化。
实际验证：在 CCS（通信系统演算）的具体实现中验证了定理，证明了只要满足图像有限性（如使用受保护递归），CCS 进程的理论等价即等同于双模拟。

5. 意义与影响 (Significance)

填补空白：这是 CSLib 中第一个模态逻辑形式化，填补了通用级 HML 形式化的空白，为后续在 Lean 中进行并发系统验证提供了坚实基础。
通用性与互操作性：通过参数化设计和对 CSLib 基础设施的紧密集成，该库不仅适用于理论证明，还能直接服务于使用相同 LTS API 的下游项目（如自动机、协议验证）。
自动化效率：展示了利用现代定理证明器（Lean 4）的自动化策略（如 grind）可以高效处理复杂的元理论证明，降低了形式化逻辑的门槛。
未来扩展的基础：该工作作为参考实现，为未来扩展至弱等价（weak equivalences）、不动点算子（fixpoint operators）以及处理绑定变量（如 $\pi$ -演算中的名义转换系统）奠定了基础。

总结：该论文成功地在 Lean 中构建了一个高质量、通用且可重用的 Hennessy–Milner 逻辑库，不仅完整形式化了其核心元理论（包括著名的 Hennessy–Milner 定理），还通过深度集成 CSLib 生态，为形式化验证计算系统提供了强有力的逻辑工具。