💻 computer science

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

本文提出了一种名为 TREBL 的相对完备的相对完整时间事件 B 逻辑，该逻辑允许在事件 B 机器状态上表达迹属性，并定义了一套针对安全领域示例的健全推导规则，证明了在机器经过包含可定义变项的适当细化后，所有有效的蕴涵式均可被推导。

原作者： Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

发布于 2026-04-22

📖 1 分钟阅读☕ 轻松阅读

原作者： Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière, Neeraj Kumar Singh, Guillaume Dupont, Yamine Aït Ameur

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

这篇文章介绍了一种名为 TREBL 的新逻辑工具，它是为了帮助计算机科学家更严格地验证软件系统（特别是那些涉及安全、并发和实时性的系统）而设计的。

为了让你轻松理解，我们可以把这篇论文的核心思想想象成**“给软件系统安装一个全知全能的‘预言家’和‘导航仪’"**。

1. 背景：为什么我们需要这个？

想象你在设计一个复杂的交通控制系统（比如红绿灯或地铁调度）。

状态（State）：就是系统在某一瞬间的样子（比如：红灯亮，车在路口）。
轨迹（Trace）：就是系统随时间变化的完整过程（比如：红灯 -> 绿灯 -> 车走 -> 红灯...）。

以前的验证方法（比如 Event-B）非常擅长检查**“状态”是否安全。例如：“红灯亮的时候，绝对不能有车闯红灯”。这就像检查每一张照片**是否合规。

但是，很多重要的问题不是关于“照片”的，而是关于**“视频”**（轨迹）的。比如：

活性（Liveness）：“只要有人按了按钮，电梯最终一定会来吗？”（不能永远停在 1 楼不动）。
公平性（Fairness）：“每个请求最终都会被处理吗？”（不能只服务 VIP，忽略普通人）。

以前的工具很难证明这些“最终会发生”的事情，因为它们通常只能看单张照片，或者需要把整个视频流当作一个黑盒子，导致证明过程要么太复杂，要么根本证明不完（数学上叫“不完备”）。

2. 核心突破：TREBL 是什么？

这篇论文提出的 TREBL 就像是一个超级导航仪。它的核心创新在于一个非常巧妙的视角转换：

以前的做法：为了证明“最终会发生 X"，我们需要分析整条视频流（轨迹）。这就像为了证明“明天会下雨”，你要把未来一年的每一分钟都模拟一遍，太难了。

TREBL 的做法：它发现，只要知道了现在的状态（照片），未来的所有可能轨迹其实就已经被“锁定”了。就像你站在山顶（当前状态），虽然你可以走很多条路（轨迹），但所有的路都从你脚下出发。

比喻：TREBL 不需要去追踪整条河流（轨迹），它只需要站在源头（当前状态），就能通过一套特殊的规则，推导出河流最终一定会流向大海（满足某个条件）。

3. 关键工具：变体（Variants）——“能量条”或“倒计时”

为了证明“最终会发生”，TREBL 使用了一种叫做**“变体（Variant）”**的工具。

通俗解释：想象你在玩一个游戏，每走一步，你的**“能量条”**就会减少一点。
规则：
1. 能量条必须是一个有限的数字（比如不能是负无穷）。
2. 只要游戏还没结束（还没达到目标），每走一步，能量条必须严格减少。
结论：因为能量条是有限的，而且每一步都在减少，所以它最终一定会耗尽。一旦耗尽，就意味着你到达了目标状态。

论文的贡献：
以前的方法只能处理简单的“能量条”。这篇论文发明了一套更强大的规则，可以处理各种复杂的“能量条”组合：

单线程能量条：只有一条路，必须走到黑。
多线程能量条：有很多条路，只要存在一条路能走到黑，或者所有路都能走到黑。
条件能量条：只有在特定条件下（比如“如果下雨”），能量条才开始减少。

4. 相对完备性：只要你能“细化”，就能证明

论文提出了一个非常有力的概念：相对完备性（Relative Completeness）。

意思：如果某个软件系统真的满足“最终会成功”这个条件，那么理论上我们一定能找到一个“能量条”来证明它。
前提：有时候，原始的代码里可能没有现成的“能量条”。这时候，我们需要对系统进行**“细化（Refinement）”**。
比喻：这就像你要证明“这辆车能跑完马拉松”。如果车上没有里程表（变体），你证明不了。但你可以给车加装一个里程表（细化）。一旦装上了，你就能通过读数证明它跑完了。
论文的保证：作者证明了，对于任何合理的系统，我们总是可以通过这种“加装里程表”（细化）的方式，构造出所需的证明工具。

5. 实际应用：安全与隐私

论文中用了很多安全领域的例子来展示 TREBL 的威力：

非干扰性（Non-interference）：想象一个保密系统。高权限的人（VIP）在操作时，低权限的人（普通员工）看到的屏幕不应该有任何变化。TREBL 可以非常简单地证明：无论 VIP 怎么操作，普通员工看到的“照片”永远是一样的。
有界可推导性（Bounded Deducibility）：证明黑客即使观察了系统的所有操作，也无法推断出超过一定限度的秘密信息。

总结

这篇论文就像是为软件验证领域发明了一种新的语言。

以前：验证“未来会发生什么”很难，要么做不到，要么只能做一部分。
现在（TREBL）：
1. 它把复杂的“时间流”问题，转化为了简单的“当前状态”问题。
2. 它提供了一套完整的“能量条”规则（变体），用来证明系统不会死锁、不会卡住、最终会完成任务。
3. 它保证了只要系统逻辑是对的，我们就一定能找到证明方法（通过细化系统）。

简单来说，TREBL 让计算机科学家能够像解数学题一样，严谨、完整且机械地证明软件系统**“不仅现在是对的，未来也一定会是对的”**。这对于开发自动驾驶、医疗设备、银行系统等关键软件至关重要。

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

现有方法的局限性：
- 传统的基于状态的严格方法（如 Event-B, B, TLA+, ASM）主要关注状态不变性（Invariants）和转换不变性。这些逻辑通常是完备的（Complete），因为它们基于带有类型的谓词逻辑。
- 然而，验证活性条件（如进展 Progress、存在性 Existence、持久性 Persistence、公平性 Fairness）需要推理完整的执行轨迹（Traces），这通常涉及时序逻辑（如 LTL, CTL）。
- 表达能力与完备性的两难（Scylla and Charybdis）：
  - 经典的时序逻辑（如 LTL, CTL）虽然完备，但本质上是命题逻辑的扩展，表达能力有限，难以直接处理 Event-B 中的复杂状态变量和量词。
  - 若将时序算子扩展到一阶或二阶逻辑（如 LTL(EB)），虽然表达能力增强，但会导致逻辑不完备（Undecidable/Incomplete），使得自动或半自动验证变得困难。
- 之前的尝试： Hoang 和 Abrial 曾尝试结合 Event-B 和 LTL 片段，但缺乏完备性证明。Ferrari 等人之前的工作（[FRS+24]）定义了一个片段 $\square$ $□$ LTL 并证明了相对完备性，但存在两个主要限制：
  1. 要求机器必须是**尾部同质（Tail-homogeneous）**的（即所有轨迹在某种意义上必须表现一致），这限制了非确定性系统的处理。
  2. 时序公式仍然被解释为在轨迹上，而非状态上，未能充分利用 Event-B“状态决定轨迹”的特性。

2. 方法论 (Methodology)

本文提出了一种名为 TREBL (Temporal Event-B Logic) 的新逻辑框架，其核心思想是将时序逻辑的语义从“轨迹”转移到“状态”上，利用 Event-B 的状态更新机制来定义时序算子。

核心思想：状态决定轨迹
- 在 Event-B 中，一个状态 $S$ 决定了从该状态开始的所有可能轨迹。因此，不需要将轨迹作为逻辑中的第一类对象（First-class objects）。
- 通过扩展 Event-B 逻辑，引入**更新集（Update Sets）**的概念，将多步状态转换显式化。
- 定义扩展逻辑 $L_{ext}$ ，其中包含描述多步更新集的公式（如 $USet^*(k, X)$ ）和模态算子 $[X]\phi$ （表示应用更新集 $X$ 后 $\phi$ 成立）。
时序算子的定义（作为快捷方式）：
- 在 $L_{ext}$ 中，常见的时序算子（Always $\square$ , Eventually $\diamond$ , Until $U$ ）被定义为复杂的一阶逻辑公式的快捷方式（Shortcuts）。
- 关键创新： 这些公式虽然在语义上描述轨迹性质，但在语法和解释上完全基于状态。
- 支持多种量化：
  - 全轨迹（All-traces）： $\square\phi$ （所有轨迹中 $\phi$ 始终成立）。
  - 单轨迹（One-trace）： $\square_1\phi$ （存在某条轨迹 $\phi$ 始终成立）。
  - 可定义轨迹集： 支持基于特定条件筛选轨迹子集进行量化。
推导规则与变体（Variants）：
- 为了证明活性性质，引入了多种变体项（Variant Terms），这些项取值于良基集合（Well-founded sets），用于证明收敛性或发散性。
- 定义了多种变体：
  - c-variant / lc-variant： 用于收敛性（Convergence），证明存在性（Existence）。
  - d-variant / ld-variant： 用于发散性（Divergence），证明持久性（Persistence）。
  - e-variant： 用于可达性（Reachability）。
  - Simultaneous/Conditional variants： 用于处理复杂的进展（Progress）条件，特别是涉及多轨迹交互的情况。
相对完备性（Relative Completeness）：
- 证明了一组推导规则是相对完备的：只要 Event-B 机器经过充分细化（Sufficiently Refined）（即能够定义出所需的变体项），任何有效的时序公式都可以被推导出来。
- 关键引理： 证明了对于任何满足活性条件的机器，总存在一个保守细化版本，其中所需的变体项是可定义的。

3. 主要贡献 (Key Contributions)

定义 TREBL 逻辑： 提出了一个基于 Event-B 逻辑的时序逻辑片段，能够表达所有重要的活性条件（不变性、存在性、进展、持久性、可达性），并支持全轨迹、单轨迹及轨迹子集的量化。
语义状态化： 成功将时序公式的解释从“轨迹”转移回“状态”，消除了对轨迹作为独立逻辑对象的依赖，简化了语义并保留了 Event-B 的原有特性。
移除尾部同质限制： 通过引入“可定义轨迹集”和更精细的变体（如 pld-variant, pd-variant），完全移除了之前工作中对机器必须是“尾部同质”的限制，使得该逻辑能处理更广泛的非确定性系统。
证明相对完备性： 建立了一套包含 63 条推导规则的推导系统，并证明了其相对完备性。核心在于证明了所需变体项总是可以通过机器细化来构造。
安全属性示例： 展示了 TREBL 在安全领域的强大应用，特别是**非干扰（Non-interference）**属性。在 TREBL 中，非干扰可以表示为简单的状态转换不变性，而在传统 LTL/CTL 中则极难表达。
工具集成铺垫： 为后续部分（Part II）将 TREBL 集成到 RODIN 工具和 EB4EB 元理论中奠定了理论基础，旨在提供机械化的证明支持。

4. 研究结果 (Results)

理论结果：
- 证明了 TREBL 的推导规则系统是**可靠（Sound）**的。
- 证明了该系统在机器满足“相对性假设”（一致性、不变性包含、充分细化）下是**相对完备（Relatively Complete）**的。
- 通过构造性证明（如 Lemma 2.4, 2.6, 2.8 等），展示了如何将任意满足活性条件的机器细化为包含显式变体项的机器。
应用示例：
- 多用户栈（Non-interference）： 成功形式化了多级安全栈的非干扰属性，证明了低权限用户无法感知高权限用户的操作。
- 生产者 - 消费者模型： 验证了请求的公平性（Progress）和缓冲区的非阻塞性（Existence）。
- 有界推理性（Bounded Deducibility）： 展示了如何用状态转换不变性替代复杂的 BD 约束来描述隐私属性。

5. 意义与影响 (Significance)

解决形式化验证的核心痛点： 解决了在严格方法中验证活性性质时“表达能力”与“完备性”不可兼得的长期难题。TREBL 使得在保持逻辑完备性的同时，能够表达复杂的时序性质。
提升 Event-B 的实用性： 将 Event-B 从主要关注安全属性（不变性）扩展到能够全面验证活性属性（如死锁、公平性、最终稳定性），使其适用于更广泛的实时和并发系统验证。
通用性： 虽然基于 Event-B，但其核心思想（利用状态决定轨迹、通过细化引入变体）可推广到其他基于状态的方法（如 ASM, TLA+, B），具有广泛的理论价值。
自动化验证的基石： 通过证明变体项的可构造性，为自动化工具（如 RODIN）自动生成证明义务或辅助用户定义变体提供了理论依据，推动了形式化方法的自动化进程。

总结：
这篇文章通过重新定义时序逻辑的语义基础（从轨迹到状态），并引入基于机器细化的变体构造机制，成功构建了一个既强大又相对完备的 Event-B 时序逻辑（TREBL）。它不仅克服了以往方法的理论限制（如尾部同质性），还为复杂系统（特别是涉及安全属性的系统）的自动化验证提供了坚实的理论框架。