玻尔百科当我们设计从自动驾驶汽车到金融软件等复杂系统时，我们有两个基本期望：一是它们不会引发灾难，二是它们最终会实现其预定目标。这些直观的期望对应于计算机科学与工程领域一个精确而强大的区分：安全性（safety）和活性（liveness）属性的概念。虽然“坏事永不发生”（安全性）和“好事终将发生”（活性）之间的区别看似简单，但理解它能让我们更深入地洞察系统可靠性、验证和设计。本文旨在揭示这一关键二元性的奥秘。第一章“原理与机制”将探讨安全性与活性的形式化定义、数学基础及理论意义。在此基础上，接下来的“应用与跨学科联系”将展示这些原则如何在机器人学、故障安全工程、网络安全和人工智能等不同领域中实际应用。
想象一下，你正在为一辆自动驾驶汽车设计规则。你无疑会从一些基本指令开始。其中最重要的可能是：“永远不要撞车。” 第二条几乎同等重要的规则是：“最终要到达目的地。”
乍一看，这两条规则似乎是同一枚硬币的两面——都关乎成功完成一次旅程。但如果我们仔细观察，就会发现它们之间存在着深刻而优美的区别。这种二元性不仅支配着自动驾驶汽车，也支配着我们构建的几乎所有复杂系统的可靠性，从手机里的微处理器到为我们城市供电的庞大电网。这就是安全性（safety）与活性（liveness）之间的区别。
让我们暂时回到汽车的例子上。规则“永远不要撞车”就是我们所说的安全性属性。它规定坏事永远不许发生。“坏事”在这里指的就是碰撞。工程领域的其他例子可能包括：仓库机器人撞上障碍物、化学反应器的温度超过临界阈值，或者关键计算错过其截止时间。在所有这些情况中，规则都是一种绝对的禁止。
规则“最终要到达目的地”则是一个活性属性。它规定好事最终必须发生。“好事”就是到达你的目标。你可能会遇到交通堵塞，可能会绕道而行，但规则坚持你不能放弃。旅程必须在某个时刻成功结束。其他例子包括：计算机的请求最终收到确认 [@problem_id:4250103, @problem_id:4222935]、故障组件最终得到修复，或者一个自学习系统的误差最终稳定在某个容差范围以下。
这种区别感觉很直观，但其后果却影响深远。差异不仅仅在于语义，更在于你能证明什么，以及何时能证明它。
为了使这个区别更加严谨，让我们把一个系统的行为想象成一个无限延续的故事，一个随时间展开的事件序列。我们称这个故事为一个迹（trace）。一个监视器在读取这个故事的过程中，如何知道规则是否已被破坏？
对于像“永不撞车”这样的安全性属性，其违背是一个具体、可观察的事件。如果下午3:15发生了一次碰撞，那么这个故事就已被不可挽回地玷污了。那个瞬间——碰撞——就是一个“不歸点”。任何包含此事件的未来版本都是一个“坏”故事。用形式化的术语来说，对于任何违反安全性属性的迹，都必然存在该故事的一个有限开端——一个坏前缀（bad prefix）——它是失败的无可否认的证据。一旦系统产生了这个坏前缀，无论之后发生什么，该安全性属性都将永远被违背 [@problem_id:4253603, @problem_id:4205107]。试图查找错误的模型检测器只需呈现导致碰撞的这个有限事件序列作为反例——一份完整、独立的错误报告。
现在考虑一个活性属性，比如“最终到达目的地”。你何时可以宣布这条规则被打破了？在堵车一小时后？不行，交通可能会畅通。十小时后？一天后？你都无法确定。你必须永远观察这辆车，才能绝对肯定它永远不会到达。对于你观察到的任何有限的旅程片段，总存在一个可能的未来（无论多么不可能），汽车最终还是到达了目的地。形式上，活性属性是指任何有限前缀都可以被扩展成一个满足该属性的有效迹的属性 [@problem_id:4243226, @problem_id:4222935]。活性的失败没有“不归点”。一个报告活性违背的模型检测器不能只给你一个有限的事件列表，它必须向你展示一个无限的陷阱。在一个有限状态系统中，这表现为一个“套索（lasso）”的形式：一条路径通向一个循环，系统永远陷在其中，持续无法完成那件“好事”（就像一辆车在原地打转，永远到不了目的地）。
事情在这里变得真正非凡起来。安全性与活性之间的这种实践区别，对应着一个深刻的数学结构。想象一个广阔的抽象空间，其中包含所有可能的无限未来——即我们的系统可能产生的每一条迹。我们可以在这个空间中定义一种“距离”概念：如果两个未来在很长一段时间内都是相同的，那么它们就被认为是“相近”的。它们共享的开端越长，它们就越近。这赋予了我们的未来空间一种几何结构，即一种拓扑结构。
在这个未来的宇宙中，所有满足给定安全性属性的迹的集合构成一个闭集（closed set）。在拓扑学中，闭集是包含其所有极限点的集合。这在这里意味着什么呢？想象一系列未来，每一个都满足我们“不撞车”的规则，并且每一个都是对某个最终的、无限未来的越来越长的近似。如果这些近似从未发生碰撞，那么它们所趋近的最终极限未来也不应该发生碰撞，这似乎是理所当然的。这正是闭集的含义。“安全”未来的集合包含了它自身的边界。
那么活性属性呢？所有满足活性属性的迹的集合在这个空间中构成一个稠密集（dense set）。稠密集是指一个能任意接近空间中每一个点的集合。这是对我们“永恒希望”原则的一个优美的几何描绘！它意味着，无论你有一个怎样的部分故事（有限前缀），你总能找到一个以该故事为开端的“好”未来。好的结果遍布于所有可能未来的整个空间中。
因此，“坏事不发生”与“好事会发生”之间的直觀划分，正对应于闭集和稠密集这两个基本的拓扑学概念。安全性关乎远离一个禁区边界；活性则关乎保证目标永远触手可及。
那么像“总是避开不安全区域，并且无限次访问目标”这样的属性呢？ 这个属性既不是纯粹的安全性，也不是纯粹的活性。它不是安全性，因为要证明其被违背，你可能需要永远观察以确认目标没有被无限次访问。它也不是活性，因为机器人进入不安全区域的有限前缀就是一个不归点。
这不是一个例外，而是通向一个更宏大统一体的关键。著名的 Alpern-Schneider 定理表明，每个属性都可以表示为一个安全性属性和一个活性属性的交集。
我们的混合属性可以清晰地分解为：
这是一个强大的启示。任何复杂的需求，无论多么错综复杂，本质上都是一个禁止坏的有限事件的规则和一个承诺好的无限结果的规则之间的二重奏。
这不仅仅是理论上的好奇心。这种二元性对于工程可靠系统具有深远的实际意义。
首先，正如我们所见，它决定了我们如何发现和报告错误。安全性违背是一个有限的失败故事。活性违背则是一个无限的徒劳故事。
更重要的是，它塑造了我们设计能在不可预测的世界中取得成功的系统的方式。一个系统保证活性属性的能力，通常取决于外部世界在一定安全程度内的行为。控制器可以承诺最终确认一个请求，但这个承诺隐含地以执行器不会着火为条件。控制器的活性保证依赖于对其环境的一个安全性假设。
这被称为假设-保证推理（assume-guarantee reasoning）。为了构建一个能正常工作的系统，我们在一个安全性假设（即其运行的世界不会发生灾难性坏事）下，实现一个活性属性（我们的代码取得进展）。我们承诺我们的汽车最终会把你送回家（活性），前提是道路不会突然坍塌成深渊（安全性）。安全性与活性之间的相互作用是系统与其世界之间的基本契约。正是这个无形的原则，让我们能够建造出那些在重重困难下仍能正常工作的东西。
当我们建造某样东西时，无论是一个简单的电路还是一个横跨城市的电网，我们都怀有两个基本希望。首先，我们希望永远不会发生可怕的事情——桥梁不会坍塌，起搏器不会失灵，银行软件不会丢失我们的钱。这是安全性（safety）的本质。其次，我们希望我们建造它的目的——那件好事——确实会发生：当我们按下按钮时，电梯最终会到达；当我们发送消息时，它最终会被送达。这是活性（liveness）的核心。
你可能会认为这些仅仅是哲学上的愿望。但在科学与工程统一性的非凡展示中，这两个思想——“坏事永不发生”和“好事终将发生”——不仅仅是愿望，更被锻造成了精确的数学工具。它们为我们提供了一种通用语言，用以推理、设计并信任那些驱动我们现代世界的极其复杂的系统。让我们穿越其中一些世界，看看这个优美的框架是如何运作的。
让我们从最底层，从硅的世界开始。想象一下计算机芯片的两个部分需要通信。它们不能依赖共享时钟，因此必须进行一场谨慎的异步对话。其中一部分，即发送方，升起一个“请求”信号（）。另一部分，即接收方，看到这个信号后，在准备就绪时升起一个“确认”信号（）。这就是所谓的握手。那么规则是什么呢？
首先，接收方决不能在没看到请求的情况下就发出确认。如果在 信号尚未为高电平时 信号就升起，这将是一个灾难性的错误。用时序逻辑的语言，我们会将其写成一个全局保证：。这是一个典型的安全性属性。为什么？因为你可以在有限的时间内发现违规。如果你在任何时候看到 变为高电平而 仍为低电平，规则就被永久地破坏了。你在事件时间轴上找到了一个“坏前缀”，任何未来的行为都无法挽回这个错误。
但活性呢？系统仅仅不犯错是不够的，它还必须取得进展。如果发送方升起 信号，我们当然希望接收方不会永远忽略它。我们需要一个保证，即请求最终会被确认：。这是一个活性属性。你永远无法通过有限时间的观察来证明它被违背了。如果接收方还没有响应，你怎么知道它不会在下一微秒响应呢？它可能只是慢而已。一次违背——接收方的永远沉默——只能通过观察整个无限历史来确认。
同样的数字之舞从硬件扩展到现代软件中复杂的抽象概念。在异步编程中，我们使用像 promises 和 futures 这样的概念。一个任务可以创建一个 promise，这就像一个它承诺稍后会用结果填满的空盒子。其他任务可以持有对应于该盒子的 future，从而等待结果。规则是相同的。一个关键的安全性属性是 promise 是“一次写入”的；一旦用一个值实现，它就不可变，被时间冻结。它不能今天用一个值实现，明天又用另一个值实现。一个关键的活性属性是故障传播。如果打算填充盒子的任务失败或崩溃，任何等待其 future 的任务都不会永远等待。系统保证它们最终会收到失败通知，以便它们可以做出相应反应。
现在，让我们将这些思想带入信息物理系统（CPS）的物理世界——这些系统将计算与物理过程相结合。考虑一个在房间中导航的简单机器人。它最重要的工作是不撞墙或障碍物。这是一个安全性属性：“全局来看，机器人的位置永远不在障碍物内”，即 。当然，它的目标是到达目的地。这是一个活性属性：“最终，机器人的位置是目标点”，即 。
现代系统要复杂得多。想象一个自动驾驶卡车编队在高速公路上行驶。一个关键的安全性属性是保持它们之间的最小距离以防止碰撞：。一次违背是即时且灾难性的。但这个系统的目的是什么？是为了形成一个高效、符合空气动力学的车队。这个目标可以表示为一个活性属性：最终，卡车编队将达到并维持一个期望的队形，其中每辆卡车的速度和间距都符合目标策略。卡车为争夺位置而进行的任何有限轨迹都不会违背这一点；它们可能只是正在收敛的过程中。
在像汽车车道保持辅助这样的实际系统中，“最终”是不够的。我们需要知道，如果汽车偏离，它必须在零点几秒内返回车道中心。这需要一个更强的、有时间限制的活性属性，通常用信号时序逻辑（STL）等形式化语言表示：例如，“在任何时候，都必须在接下来的 秒内，汽车会靠近中心线”：。这不仅保证了最终的正确性，还保证了响应性。同时，首要的安全性属性，“始终保持在车道边界内”，绝不能被违背。
“我无法创造的，我就不理解，”Feynman 在他的黑板上写下了这句名言。对于工程师来说，一个推论可能是：“一个我不知道如何破坏的系统，我并未真正理解它。” 为故障进行设计至关重要，而安全性-活性二元性为此提供了完美的视角。
考虑一个故障安全（fail-safe）系统，比如化学反应器的控制系统。其绝对的首要任务是防止灾难。如果一个关键传感器出现故障，系统必须转换到一个预定义的安全状态，例如关闭反应。这个需求是安全性与活性的一个美妙结合。其规约可以是：“全局来看，如果检测到故障，系统必须不执行任何不安全的操作，直到它达到安全状态”：。这包含一个安全性组件（承诺谨慎行事，）和一个活性组件（承诺最终到达安全状态，）。
现在考虑一个故障-运行（fail-operational）系统，比如航天器的飞行控制器或现代汽车的线控驾驶系统。关闭不是一个选项。即使有故障，任务也必须继续。这种设计需要同时满足两类属性。它必须遵守其安全性属性（例如，保持姿态控制，维持在操作温度限制内）和其活性属性（例如，继续接受命令并提供推力）。一个故障-运行系统是在面对指定数量的组件故障时，能同时保证安全性和活性的系统，尽管可能以一种降级的形式。
“坏事”的定义并不局限于物理损害。在我们互联的世界里，它越来越多地涉及到数据和安全的泄露。
在一个工业控制系统（ICS）中，例如管理电网的系统，一个关键的安全目标是数据完整性。这意味着控制器接受的任何命令都必须是真实的且未被篡改的。这是一个安全性属性。我们可以这样陈述：“全局来看，如果一条消息被接受，那么它必须有有效的签名”：。如果系统接受了哪怕一条伪造的消息，完整性属性就被破坏了。
相应的活性属性是可用性。我们需要保证合法的消息不会被对手阻挡。“全局来看，如果一个有效的测量值被发送，它最终会被送達”：。一个导致拒绝服务攻击的攻击者就违背了这个活性属性。
这些思想甚至延伸到了隐私保护机器学习的前沿。在一个联邦学习系统中，多家医院合作训练一个医疗AI模型而不共享原始病人数据，我们也可以识别出类似的属性。一个核心的安全性属性是机密性：系统在任何情况下都绝不能泄露单个病人的记录。这是一个必须保持的不变量。同时，系统必须取得进展。一个活性属性是，由诚实的医院贡献的有效模型更新最终会被整合到共享的全局模型中，从而确保协作训练确实在进行。
所以我们有了这种绝妙的语言来指定我们的系统应该做什么。但我们的系统极其复杂。我们如何才能说服自己，一辆拥有数百万行代码的自动驾驶汽车，真正满足“永不导致碰撞”的安全性属性？
我们无法测试每一种可能的情景，可能性的数量是天文数字。因此，我们转向逻辑学和计算机科学中一个强大的思想：抽象，如今常以“数字孪生”的概念实现。我们构建一个真实系统的简化数学模型或抽象，并尝试证明关于该模型的属性。
但这提出了一个微妙而深刻的问题。如果我们证明了关于简化模型的某件事，它能告诉我们关于真实事物的什么呢？答案原来精妙地取决于我们是在证明安全性还是活性。
为了证明一个安全性属性（例如，“系统永不进入坏状态”），我们的抽象模型需要是一个过近似（over-approximation）。这意味着模型包含了系统的所有真实行为，外加一些可能在现实中不会发生的“幽灵”或虚假行为。如果我们能够证明模型的所有行为都不是坏的——甚至包括那些幽灵行为——那么我们就可以确定真实系统也是安全的。
这种策略对于活性（例如，“系统最终达到好状态”）则会失败。如果我们在过近似模型中找到一条“好”路径，我们怎么知道它不只是一个幽灵呢？它可能是一个在真实系统中不存在的行为。为了证明活性属性，我们需要其对偶：一个欠近似（under-approximation）。这是一个只包含真实系统行为子集的模型。如果我们能在这个更受约束的模型中找到一个好的行为，我们就能确定这个好的行为在现实中是可能存在的。
这种优雅的二元性——安全性证明需要过近似，而活性证明需要欠近似——是形式验证领域的基石，并展示了这种简单分类所带来的深刻、实际的后果。
从处理器握手的嘀嗒声，到构建安全可靠的人工智能这一宏大的社会挑战，安全性与活性的原则提供了一条共同的主线。它们为我们提供了一种严谨的方式来谈论我们对所创造技术的期望，以及一个将这些期望转化为可验证确定性的框架。这证明了一个好思想的力量：这种简单的二元划分——避免坏事和实现好事——能够为如此多的复杂性带来清晰和秩序。