🤖 AI

Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

本文介绍了 Uppaal Coshy，这是一个通过利用仿真近似复杂的状态空间划分，并采用 Caap 算法将生成的策略高效地表示为决策树，从而为混合系统合成紧凑安全屏蔽的自动化工具。

原作者： Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, Andrzej Wąsowski

发布于 2026-08-06

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, Andrzej Wąsowski

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

想象一下，你正试图教一个机器人玩游戏，比如让一个球保持在空中，或者在风暴中驾驶汽车。你希望机器人尽可能做得出色，但你也必须确保它永远不会做出危险的行为，比如撞到墙或者让球掉落。在计算机科学领域，这被称为“屏蔽合成”（shield synthesis）。请不要把“屏蔽”想象成一块金属，而要把它想象成一个严厉的安全教练，站在机器人身边。如果机器人试图做出可能导致灾难的动作，教练就会介入并说：“不，不是那个！试试这个安全的动作。”这对于规则不断变化的复杂系统至关重要，比如受风力影响而产生反应的弹跳球，或者是处理电力的电路。挑战在于，这些系统拥有无限的可能性，使得编写一份完美的、针对每种情况的“安全”与“不安全”动作清单变得极其困难。

这就是论文《Uppaal Coshy：混合系统紧凑型屏蔽的自动合成》所要解决的问题。研究人员（来自丹麦的一个团队）开发了一种名为 Uppaal Coshy 的新工具，它就像是一个针对这些棘手的混合系统（由于它们结合了平滑、连续的变化，如速度，以及突然的数字跳变，如开关切换，因此被称为“混合系统”）的超级智能安全教练。他们的核心思想是首先将整个可能的宇宙划分为一个巨大的微小方格网。然后，他们运行数千次模拟，以确定哪些方格是安全的，哪些是危险的，从而创建一张庞大的允许动作地图。然而，这张地图可能会变得过于庞大，以至于无法存储或使用。为了解决这个问题，他们发明了一种聪明的算法，名为“Caap”（听起来像是一个友好的机器人名字），它可以将这张巨大且混乱的地图压缩成一个整洁、紧凑的决策树——就像把一本百页的说明书变成一个简单的流程图。他们在弹跳球模型上测试了该方法，发现该方法可以在不损失任何安全性的前提下，将安全规则缩小数千倍，从而使这些安全教练能够安装在真实的设备上。

弹跳球与安全教练的故事

让我们通过一个我们都熟悉的角色——弹跳球，深入到故事的核心。想象一个上下弹跳的球。人类玩家可以击打它以保持其运动，但如果击打力度过大或时机不对，球可能会飞向天空或完全停止弹跳。目标是让球永远弹跳下去，既不会停止也不会飞走。

在过去，要精确计算何时击打球以保持安全简直是一场噩梦。球的位置和速度在平滑且连续地变化，这意味着在每一秒钟，它都有无限个可能所在的位置。研究人员使用名为 Uppaal Coshy 的工具解决了这个问题。他们将球的世界视为一个巨大的棋盘。他们将球所在的空间切割成数百万个微小的矩形方格。对于每个方格，该工具都会问一个简单的问题：“如果球在这个方格里，哪些动作是安全的？”

为了回答这个问题，该工具不仅仅是在猜测；它反复进行游戏。它在方格内选取一个点，模拟球的弹跳，并观察它的落点。如果球落在“安全”的方格内，那么这个动作就是好的。如果球落在“危险”的方格内（例如球停止跳动的方格），那么这个动作就会被禁止。由于球的行为可能带有一点随机性（也许地面是凹凸不平的，或者击打并不完美），该工具多次运行这些模拟以确保万无一失。他们甚至必须处理球跳得太高而完全离开“棋盘”的情况。该工具通过创建一个特殊的“越界”区域，并根据模拟结果来决定离开棋盘是否安全，从而处理了这一问题。

巨大地图的问题

在这里，故事遇到了障碍。因为网格非常精细（为了保证精确度），该工具最终得到了一份庞大的规则清单。在他们的弹跳球示例中，初始安全地图拥有超过 140 万 个微小的方格，每个方格都有关于如何操作的规则。存储这么庞大的列表就像是试图把一座图书馆装进你的背包里；对于真正的机器人来说，这太重了，无法使用。

研究人员注意到了一些有趣的现象：许多相邻的方格具有完全相同的规则。如果球处于一个可以安全击打的方格，那么紧邻其侧的方格里的球很可能也是可以安全击打的。因此，与其保留数百万个微小的规则，为什么不把它们组合在一起呢？

进入 Caap：神奇的压缩器

这时，他们的算法 Caap 登场了。把 Caap 想象成一个神奇的编辑，它审视着那张巨大且混乱的地图，然后说：“嘿，这 500 个方格都说‘击打球’。让我们把它们合并成一个大的区域吧。”它通过寻找模式并将相邻的方格合并成更大的矩形区域来实现这一点，只要规则保持不变。

结果是一个决策树。想象一个流程图：“球在高处吗？是的。移动得快吗？不。那么就击打它。”这个树状结构比原始的一百万个方格的地图要小得多，也更容易阅读。在测试中，Caap 成功地将弹跳球的安全规则从 1,430,000 个微小单元缩减到了仅有的 2,972 个区域。这是一个巨大的缩减！这就像把一部千页的小说变成了一本 20 页的连环画，而讲述的却是完全相同的故事。

它真的有效吗？

团队不仅缩小了地图，还确保了它依然有效。他们在弹跳球上测试了这个新的紧凑型屏蔽。他们运行了 10,000 次模拟，由这个新的压缩安全教练控制球。结果如何？在所有 10,000 次运行中，球从未停止弹跳或飞走。即使规则现在已经小到可以印在明信片上，安全性依然得到了完美的保留。

他们还展示了这种安全教练可以用来教机器人变得“更好”。首先，他们让机器人学习如何高效地击打球（使用尽可能少的能量），同时让屏蔽器在旁守护，以防止它犯下危险错误。机器人学会了用极少的击打次数让球保持在空中，证明了你可以同时拥有安全性和效率。

为什么这很重要

这篇论文不仅仅关于弹跳球。同样的数学原理也适用于现实世界中的事物，比如需要保持电压稳定的电路（称为升压转换器），或者需要避免溢出的水箱。研究人员也在这些模型上测试了他们的工具，在每种情况下，Caap 算法都成功地大幅缩小了安全规则——有时将数百万条规则减少到仅有的几十条——同时保持系统安全。

Uppaal Coshy 的美妙之处在于它是全自动的。你不需要成为数学天才才能使用它；你只需要描述你的系统，工具就会计算出安全规则，压缩它们，并给你一个准备好使用的紧凑型屏蔽器。这是为确保未来的智能机器人和自动化系统不仅聪明而且安全、可靠，并且足够小到可以在我们日常使用的设备上运行迈出的重要一步。

技术摘要：Uppaal Coshy —— 混合系统紧凑型屏蔽（Shields）的自动合成

1. 问题陈述

本文解决了为具有复杂混合动力学的马尔可夫决策过程（MDPs）连续状态空间合成安全策略（即屏蔽/Shields）的挑战。与安全屏蔽已在离散状态空间中得到成熟应用的现状不同，混合系统在算法上面临困难，特别是在非线性动力学的可达性分析以及无限状态空间管理方面。

作者指出，一个主要的实际瓶颈是合成屏蔽的可扩展性与存储问题。传统的基于分区的方案需要为网格中的每一个单独单元格存储允许的操作，这导致了庞大的数据结构，在存储和部署方面效率低下，尤其是在嵌入式设备上。此外，在一般混合系统中，确定安全单元格及其转换通常涉及不可判定的可达性问题。

2. 方法论

作者提出了 Uppaal Coshy，这是一个完全集成到 Uppaal 建模环境中的工具。该方法结合了基于分区的合成算法、基于仿真的近似处理以及一种新型的压缩技术。

2.1 基于分区的屏蔽合成

核心算法通过使用由粒度向量 $\gamma$ 和偏移量 $\omega$ 定义的正规网格，将连续状态空间 $S \subseteq \mathbb{R}^k$ 抽象为一组有限且不相交的矩形单元格。

安全博弈公式化：合成过程被构造成一个双人安全博弈。目标是计算最大化的“安全单元格”集合 ( $C_\phi$ )，从这些单元格出发，系统可以无限期地保持在安全属性 $\phi$ 之内。
通过仿真进行近似：由于对于一般的混合系统，精确的可达性分析往往是不可判定的，该工具采用了基于仿真的方法：
- 初始安全单元格 ( $C^0_\phi$ )：该工具并非采用符号推理，而是系统地在每个单元格内采样点。只有当所有采样点都满足安全规范时，一个单元格才被视为初始安全的。
- 转换关系：为了确定单元格之间是否存在转换（ $C \xrightarrow{a} C'$ ），工具会使用动作 $a$ 从 $C$ 中的采样状态开始模拟系统动力学。如果仿真到达了一个控制器必须做出新选择的状态，则将对应的目标单元格添加到转换关系中。
- 随机性：不同于以往需要手动构建随机维度采样的研究，Uppaal Coshy 允许模拟器直接从随机分布中采样，支持具有无界支撑集的通用分布。

2.2 处理实际挑战

无界状态空间：对于状态边界不明确的系统（例如弹球模型），该工具通过引入一个虚拟的“越界”单元格 ( $C_{out}$ ) 来处理。用户可以配置离开边界是安全的、不安全的，还是通过采样来确定。
变量省略：为了降低维度，用户可以将某些变量（如成本计数器或时钟）从网格划分中省略。只要这些变量不影响安全逻辑，它们在合成期间将被固定为初始值。

2.3 紧凑表示法：Caap 算法

为了解决基于网格的屏蔽带来的存储效率问题，作者引入了 Caap（轴对齐分区粗化算法）。

目标：将细粒度的、基于轴对齐网格的屏蔽转换为紧凑且等效的决策树。
机制：该算法通过迭代合并具有相同允许操作集的相邻单元格，从而形成更大的“区域”。
约束：合并受三个扩展规则的约束，以确保生成的划分仍然有效：
1. 新区域中的所有单元格必须具有相同的操作集。
2. 新区域不得与新划分中现有的区域相交。
3. 扩展不得将原始区域切割成非矩形的碎片。
结果：这产生了一个决策树，其中内部节点代表轴对齐谓词 ( $s_i < c$ )，叶节点代表允许的操作集，从而显著减小了表示规模。

3. 核心贡献

Uppaal Coshy 工具：一个用于 Uppaal 中屏蔽合成的全自动工具，支持包括随机混合自动机和外部 C 库调用在内的丰富形式化表达。它与 Uppaal Stratego 集成，以实现在合成屏蔽下的强化学习。
Caap 算法：一种将基于网格的屏蔽压缩为决策树的新颖算法，在保留功能性的同时大幅减小了体积。
基于仿真的近似：一种实用的实现策略，通过使用系统采样和仿真，绕过了不可判定的可达性问题，并支持非周期控制和通用随机分布。

4. 结果与评估

作者在四个模型上对工具进行了评估：弹球（bouncing ball）、升压转换器（boost converter）、随机游走（random walk）和水箱（water tank）。

合成与缩减：论文中的表 2 展示了显著的屏蔽规模缩减。对于弹球模型，屏蔽从 1,430,000 个单元格 缩减至 2,972 个区域（缩减因子约为 480 倍），耗时 53 秒。升压转换器的规模从 136,800 缩减至 571 个区域。
安全性验证：所有合成的屏蔽都通过 10,000 次运行进行了 99% 置信区间的统计评估。未观察到任何不安全运行，证实了屏蔽能够维持安全属性（例如，防止球停止运动或电压超过限制）。
工作流演示：弹球案例研究（第 5.1 节）展示了一个完整的工作流：合成一个基础的“高效”策略（该策略违反安全性），生成屏蔽，通过 Caap 进行压缩，最后使用 Uppaal Stratego 在紧凑屏蔽下学习一个近优策略。最终得到的策略既安全又高效。

5. 重要性与主张

本文将 Uppaal Coshy 定位为连接理论屏蔽合成与复杂混合系统实际应用之间的桥梁。

表达能力：该工具声称其处理的模型比现有工具（如 Tempest 或 Uppaal Tiga）具有更丰富的类，具体支持具有非周期控制和外部代码集成的随机混合系统。
可部署性：通过引入 Caap 算法，作者声称解决了屏蔽规模这一关键问题，使得在资源受限的嵌入式设备上部署合成策略变得可行。
集成性：与 Uppaal Stratego 的无缝集成允许了一种工作流，即由屏蔽保证安全性，同时通过强化学习优化性能，作者强调这是相对于以往工作的显著优势。

作者对其方法的近似性质保持了谦逊的态度，指出基于仿真的欠近似（under-approximation）依赖于采样数 ( $n$ ) 和重采样运行次数 ( $m$ ) 来逼近真实解，并且 Caap 算法目前是一个独立的工具，他们提议在未来的工作中将其直接集成到 Uppaal 用户界面中。