⚡ electrical engineering

A Pragmatic Guide to Building Conservative Discrete Abstractions of Cyber-Physical Systems

本文提出了一种务实的、通过构造保证保守性的工作流，用于构建网络物理系统的离散抽象，该工作流通过一个包含状态空间划分、保守性转换构造、虚假行为缓解以及可靠规范提升的模块化四步过程，解决了常见的陷阱，从而确保了可靠的验证保证。

原作者： Jordan Peper, Krish Kapadia, James Gast, Ethan Howes, Ivan Ruchkin

发布于 2026-08-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Jordan Peper, Krish Kapadia, James Gast, Ethan Howes, Ivan Ruchkin

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

想象一下，你正在试图教一个机器人如何在繁忙的城市中开车。现实世界是混乱且连续的；机器人可以在道路上的任何精确位置，以任何精确的速度，以及任何精确的角度转弯。但是计算机，尤其是那些需要在机器人移动之前证明其安全性的计算机，在处理无限种可能性时会感到吃力。它们更擅长处理有限的列表，就像一个具有固定方格数量的棋盘游戏。这就是信息物理系统（Cyber-Physical Systems, CPS）的核心：数字大脑与物理躯体的结合。为了检查机器人是否会发生碰撞，工程师使用一种叫做符号模型检测（symbolic model checking）的方法。你可以把它想象成一个超级精准的侦探，它会检查机器人可能采取的每一种可能的动作，以确保它永远不会撞到墙。但为了做到这一点，这个侦探需要将流畅、连续的现实世界转化为块状的、分步式的地图。这个过程被称为离散抽象（discrete abstraction）。

棘手之处在于，如果你把地图做得太简单，你可能会错过真实的危险（机器人在现实中发生了碰撞，但在地图上看起来是安全的）；如果你把地图做得太复杂，侦探就会应接不暇，无法完成任务。目标是构建一个“保守”的地图——这意味着它可能会想象一些现实中并不存在的危险（悲观主义），但它绝不会错过任何真实的危险。这篇论文是为工程师准备的一份指南，指导他们如何正确地构建这些地图，从而避免导致错误的安全性保证的常见陷阱。

安全机器人地图的蓝图

这篇论文是一份构建复杂机器“保守”地图的实用现场指南。来自佛罗里达大学的作者团队认为，虽然将连续的机器人转化为块状游戏对于安全性检查是必要的，但许多工程师无意中构建了要么过于危险（遗漏真实风险），要么过于偏执（想象不存在的风险）的地图。他们提出了一个四步工作流，通过“构造性”的方法来构建这些抽象，确保地图在设计上始终是安全的。

第一步：将世界切割成瓦片

首先，你必须将平滑、无限的状态空间（即机器人可以处于任何位置的空间）转化为有限的网格瓦片。想象一下，拿一张巨大的、连续的坐标纸，并将其切割成不同的、互不重叠的正方形。每个正方形代表一个“瓦片”或一个抽象状态。作者建议使用均匀网格，就像棋盘格一样，你决定在每个维度（长度、宽度、角度）上想要多少个瓦片。如果你为三维的独轮车机器人选择了每个维度 10 个瓦片，那么你最终会得到 1,000 个总瓦片（ $10 \times 10 \times 10$ ）。这一步确保了机器人可能处于的每一个现实世界位置都至少被一个瓦片所覆盖。

第二步：绘制箭头（棘手的部分）

现在你需要弄清楚机器人从当前瓦片出发可以跳到哪些瓦片。这是论文提供三种不同工具的地方，每种工具都有不同的“保守性”风格：

轴对齐包围盒 (AABB)： 想象机器人位于一个瓦片中。你计算出它在一秒钟后可能到达的所有位置。为了安全起见，你画出一个最小的可能矩形（轴对齐包围盒），完全包围所有这些可能的未来位置。如果这个矩形触碰到了相邻的瓦片，你就向该瓦片画一个箭头。这就像是用一个又大又笨拙的盒子包裹住机器人的未来。它很快，但盒子可能太大，从而产生指向机器人实际上永远无法到达的瓦片的“虚假”箭头。
多胞形 (Polytope)： 这是一种更紧凑、更灵活的形状（类似于拉伸的橡胶片），比方框能更贴合机器人的未来。它更精确，但计算它需要更多的计算能力。
采样法 (PAC)： 与其计算每一种可能性，不如投掷飞镖。你在瓦片内部随机选取起始点，模拟机器人的运动，并记录下你看到的箭头。论文引入了一个聪明的“证书”（一种统计保证），它声明：“我们有 99% 的信心，我们已经看到了所有发生概率超过 1% 的箭头。”这对于那些无法写出完美公式的复杂、黑盒机器人非常有效，但它依赖于概率而非绝对证明。

第三步：清理“虚假”路径

由于第二步中的方法是保守的，它们经常会产生伪转移（spurious transitions）——即地图上看起来存在但现实中并不存在的箭头。更糟糕的是，它们经常产生自环（self-loops），即地图显示机器人可以永远停留在同一个瓦片中。这对安全性检查来说是一个噩梦，因为如果机器人可以永远停留在一个瓦片中，即使它在现实生活中可以到达目标，它也可能永远无法到达。

论文提出了两种清理方法：

CEGAR（反例引导的抽象细化）： 如果安全性检查器发现了一条机器人发生碰撞的“虚假”路径，系统会沿着该路径拆分瓦片，使地图变得更详细，从而有效地消除这条虚假路径。
自环消除： 作者展示了如何证明机器人必须在一定步数内离开某个瓦片。如果你能证明机器人无法永远停留，你就可以安全地删除这个“永远停留在此”的箭头。他们在“山路车（Mountain Car）”问题和“独轮车（Unicycle）”机器人上进行了测试，结果表明，移除这些虚假循环显著提高了安全性检查的准确性。

第四步：翻译规则

最后，你必须将现实世界的安全规则翻译到块状地图上。如果规则是“留在城市边界内”，在现实地图上，这意味着“不要触碰边缘”。在块状地图上，规则发生了变化。论文解释了如何使用“可能（May）”和“必须（Must）”逻辑。一个规则对某个瓦片“必须”成立，仅当该现实世界瓦片中的每一个点都满足该规则。而一个规则“可能”成立，则是指该瓦片中至少有一个点满足规则。通过仔细地翻译规则，他们确保如果机器人在块状地图上通过了测试，则保证它在现实世界中是安全的。

他们的发现

作者在三个场景下测试了这一四步流水线：一个简单的合成系统、一个“山路车”（经典的强化学习挑战）以及一个自主独轮车。

他们发现，基于采样的法（第三步）通常能产生最干净的地图，具有最少的虚假箭头和自环，特别是对于像独轮车这样复杂的非线性机器人。虽然“包围盒”方法构建速度更快，但它产生了过多的虚假路径，使得安全性检查器难以证明机器人是安全的。

至关重要的是，他们展示了移除自环（第三步）带来了巨大的差异。对于独轮车，仅仅删除那些虚假的“永远停留”箭头，在某些情况下就能将安全性检查的成功率从约 19% 提高到 60% 以上。这证明了，一个稍微复杂一点但更“干净”的地图，往往比一个充满虚假可能性的简单地图更好。

论文总结道，通过遵循这种结构化的、保守的工作流——划分空间、仔细构建转换、清理虚假路径并正确翻译规则——工程师可以构建出值得信赖的物理机器人数字孪生体。他们并不声称解决了机器人领域的所有问题，但他们提供了一个清晰、经过测试的配方，用于避免导致不安全或无效安全性检查的最常见错误。

技术摘要：构建赛博物理系统保守离散抽象的实用指南

问题陈述

赛博物理系统（CPS）运行在安全至关重要的环境中，其失效可能威胁生命与财产。虽然符号模型检测是验证复杂时序逻辑属性的一种有效方法，但它需要一个有限状态模型。然而，现实世界的 CPS 演化于连续状态空间。为了应用模型检测，工程师必须将这些连续动力学离散化为有限状态抽象。

核心挑战在于确保可靠性（Soundness）：从抽象模型中推导出的验证保证必须能够转移到具体系统。这要求抽象模型必须是具体状态空间及其行为的保守过近似（Conservative Over-approximation）。在实践中，模型构建者经常遇到四个破坏可靠性或引入过度悲观性的陷阱：

覆盖不足：未能完全覆盖具体状态空间。
近似不足：对转移关系进行欠近似（遗漏了可行的行为）。
不当剪枝：对“退化”行为（例如，未经认证地移除自环）进行不安全的剪枝。
不当的规范提升：未能保持从抽象满足到具体满足的逻辑蕴含关系。

这些问题通常会导致“伪造”的反例，即抽象模型违反了实际由具体系统满足的规范，从而使验证变得毫无意义。

方法论

本文提出了一个用于构建保守离型离散抽象的四步模块化工作流。该工作流是“按构造实现保守性（Conservative-by-construction）”的，这意味着通过特定的数学保证在每个阶段都维持了可靠性。

第一步：状态空间抽象

使用均匀的长方形网格将连续状态空间 $X$ 划分为有限的抽象状态集 $\hat{X}$ 。量化函数 $\psi: X \to \hat{X}$ 将具体状态映射到抽象单元。逆映射 $\Psi(\hat{x})$ 定义了每个抽象状态的具体区域（原像）。这一步确保了每个具体状态和初始条件在抽象模型中都有代表。

第二步：保守转移构造

本文提出了三种可互换的方法来计算转移关系 $\hat{f}$ （即确定哪些抽象状态可以跟随其他状态），以确保每一个具体转移都在抽象模型中得到表示：

轴对齐包围盒（AABB）：计算具体单元在系统动力学下的图像的包围盒。任何与该包围盒相交的抽象单元都会被添加为后继状态。这种方法计算效率高，但对于非线性系统可能过于保守。
多胞体传播（Polytope Propagation）：使用多胞体（凸包）来过近似具体单元的图像。对于非线性动力学，它比 AABB 更紧凑，但计算成本更高。它采用 AABB 剔除法来过滤候选对象，然后再进行高成本的多胞体相交测试。
基于 PAC 证书的采样：对于黑盒或高度非线性的系统，通过对状态空间进行采样来发现转移。该方法不提供确定性保证，而是提供**概率近似正确（PAC）**保证。它证明了以高置信度（ $1-\delta$ ），构建的转移关系包含了所有“显著”转移（发生概率 $\ge \beta$ 的转移），从而界定了未观测到转移的“缺失质量”。

第三步：缓解退化行为

保守抽象往往会引入伪造转移（在具体系统中不可能发生的转移）和自环（从状态到自身的转移）。这些现象会导致验证中的假阴性，特别是对于活性（Liveness）属性。

伪造转移：通过**反例引导的抽象细化（CEGAR）**来解决。如果在抽象模型中发现反例轨迹，算法会针对具体动力学对其进行验证。如果该轨迹是伪造的（即可达集为空），则会对状态空间进行细化（分裂）以消除该伪造转移。
自环：通过经过认证的自环消除来解决。只有当能够证明从该单元出发的每一个具体轨迹都会在有限步数（ $K$ ）内逃逸时，才会移除自环。这可以通过迭代可达集传播或通过具有 PAC 保证的采样策略来进行验证。

第四步：LTL 规范的可靠提升

为了验证抽象模型，定义在具体空间上的线性时序逻辑（LTL）规范 $\phi$ 必须提升为抽象规范 $\hat{\phi}$ 。本文采用了**“或/必（May-Must）”语义**：

Must 谓词：仅当一个原子命题在单元内的所有具体状态下均成立时，该抽象状态才持有该命题。
May 谓词：如果该命题在至少一个具体状态下成立，则该抽象状态持有该命题。
提升算子 $\rho$ 通过将原子命题强化为“必（Must）”（用于安全性）或弱化为“或（May）”（根据逻辑结构适当处理）来将 $\phi$ 转换为 $\hat{\phi}$ ，从而确保 $\hat{s} \models \hat{\phi} \implies s \models \phi$ 。

核心贡献

实用的工作流：一个统一的四步流水线，将状态划分、转移构造、退化行为缓解和规范提升集成到一个单一的可靠框架中。
可互换的子程序：该方法支持多种转移构造方法（AABB、多胞体、采样）和退化行为移除方法（CEGAR、认证消除），允许用户在计算成本与抽象紧凑度之间进行权衡。
针对采样的 PAC 保证：引入了一种数据驱动的方法进行转移构造，为解析过近似难以处理的系统提供了严格的概率覆盖证书（通过 Good-Turing 估计器和 McAllester-Schapire 界限）。
系统化处理退化问题：通过认证消除和 CEGAR 显式地解决了伪造转移和自环问题，防止了通常困扰保守抽象的悲观性。

实验结果

作者在三个案例研究上评估了该流水线：一个合成线性系统、一个 Mountain Car 基准测试（非线性，学习策略）以及一个自主单轮车（Dubins 模型）。

转移构造：对于非线性系统，与 AABB 和多胞体方法相比，基于采样的方法通常能产生更稀疏的转移关系，具有更少的自环和更低的后继数量变异性。这导致了更高的真阳性率（TPR）。
自环消除：移除自环显著改善了验证结果。对于单轮车案例，消除后的 TPR 从约 0.19 提高到约 0.63。在 Mountain Car 案例中，TPR 从约 0.83 提高到约 0.93。
CEGAR：虽然 CEGAR 显著增加了模型规模和构建时间，但它一致地降低了自环比例（SLP）。它在 Mountain Car 系统中产生了显著的 TPR 提升，但在单轮车系统中影响较小，因为高 SLP 被归因于难以通过针对性消除来处理的平凡反例。
粒度：更细的状态空间粒度始终带来更高的 TPR，证实了模型规模与验证精度之间的权衡。

意义

本文声称其意义在于为构建 CPS 抽象的工程师和研究人员提供了一份实用指南。它通过以下方式填补了理论抽象技术与实际应用之间的鸿沟：

提供了一个按构造实现可靠性的工作流，防止导致不可靠验证的常见错误。
提供模块化工具，允许从业者根据系统复杂度和可用计算资源，在确定性（AABB/多胞体）和概率性（采样）方法之间进行选择。
证明了缓解退化行为（伪造转移和自环）不仅是一种优化，更是实现有意义的验证结果（特别是对于活性属性）的关键步骤。

作者总结道，虽然符号模型检测功能强大，但其效用完全取决于抽象的质量。本工作流提供了一个严谨且可调的框架，在平衡悲观性与可处理性的同时，实现高质量的抽象。