2025-11-12T00:43:29.720804

Efficient Shield Synthesis via State-Space Transformation

Brorholt, Høeg-Petersen, Larsen et al.
We consider the problem of synthesizing safety strategies for control systems, also known as shields. Since the state space is infinite, shields are typically computed over a finite-state abstraction, with the most common abstraction being a rectangular grid. However, for many systems, such a grid does not align well with the safety property or the system dynamics. That is why a coarse grid is rarely sufficient, but a fine grid is typically computationally infeasible to obtain. In this paper, we show that appropriate state-space transformations can still allow to use a coarse grid at almost no computational overhead. We demonstrate in three case studies that our transformation-based synthesis outperforms a standard synthesis by several orders of magnitude. In the first two case studies, we use domain knowledge to select a suitable transformation. In the third case study, we instead report on results in engineering a transformation without domain knowledge.
academic

Efficient Shield Synthesis via State-Space Transformation

基本信息

  • 论文ID: 2407.19911
  • 标题: Efficient Shield Synthesis via State-Space Transformation
  • 作者: Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Kim Guldstrand Larsen, Christian Schilling
  • 机构: Aalborg University, Denmark
  • 分类: cs.LO cs.AI cs.LG cs.SY eess.SY
  • 发表时间: 2024年7月（arXiv预印本）
  • 论文链接: https://arxiv.org/abs/2407.19911

摘要

本文研究控制系统安全策略合成问题，也称为屏蔽(shield)合成。由于状态空间无限，屏蔽通常在有限状态抽象上计算，最常见的抽象是矩形网格。然而，对于许多系统，这种网格与安全属性或系统动力学匹配不佳。粗网格通常不足，而细网格在计算上往往不可行。本文表明，适当的状态空间变换可以在几乎没有计算开销的情况下仍然使用粗网格。通过三个案例研究证明，基于变换的合成方法比标准合成方法的性能提升了几个数量级。

研究背景与动机

问题定义

本研究要解决的核心问题是如何高效地为控制系统合成安全策略（屏蔽）。在信息物理系统中，数字控制器需要保证系统安全性，这促使了自动控制器构造方法的发展。

重要性

  1. 安全关键性: 许多信息物理系统都是安全关键的，需要形式化的安全保证
  2. 方法互补: 强化学习提供最优性但缺乏安全保证，而反应式合成提供安全保证但缺乏最优性
  3. 屏蔽框架: 结合两种方法的优势，通过屏蔽在学习过程中防止不安全动作

现有方法局限性

  1. 网格抽象问题: 矩形网格通常与系统动力学和安全属性不匹配
  2. 计算复杂性: 粗网格精度不足，细网格计算不可行
  3. 状态空间爆炸: 随着精度要求增加，状态空间呈指数级增长

研究动机

通过状态空间变换，在新的状态空间中使网格更好地与系统动力学对齐，从而在保持计算效率的同时提高合成质量。

核心贡献

  1. 提出了基于状态空间变换的屏蔽合成方法，能够显著减少所需的网格单元数量
  2. 证明了变换方法的理论正确性，包括安全性保证从变换空间到原始空间的转移
  3. 在三个案例研究中验证了方法有效性，性能提升达到几个数量级
  4. 提供了无领域知识的变换工程方法，扩展了方法的适用性
  5. 实现了与强化学习的集成，展示了实际应用价值

方法详解

任务定义

给定控制系统(S,Act,δ)(S, Act, δ)，其中：

  • S⊆RdS ⊆ \mathbb{R}^d：有界d维状态空间
  • ActAct：有限控制动作集
  • δ:S×Act→2Sδ: S × Act → 2^S：后继函数

目标：为安全属性φ⊆Sφ ⊆ S合成安全策略σ:S→2Actσ: S → 2^{Act}

核心架构

1. 状态空间变换

  • 变换函数: f:S→Tf: S → T，将原始状态空间SS映射到变换空间TT
  • 逆变换: f−1:T→2Sf^{-1}: T → 2^S，定义为f−1(t)={s∈S∣f(s)=t}f^{-1}(t) = \{s ∈ S | f(s) = t\}
  • 网格友好性: 变换应使网格边界与决策边界对齐

2. 变换空间中的后继函数

在变换空间TT中定义新的控制系统(T,Act,δT)(T, Act, δ_T)： δT(t,a)=f(δS(f−1(t),a))δ_T(t, a) = f(δ_S(f^{-1}(t), a))

3. 网格扩展

可控单元集合CφfC_φ^f定义为： Cφf=⌊f(φ)⌋G∩{C∈G∣∃a∈Act.∀C′.C→aC′⟹C′∈Cφf}C_φ^f = ⌊f(φ)⌋_G ∩ \{C ∈ G | ∃a ∈ Act. ∀C'. C \xrightarrow{a} C' ⟹ C' ∈ C_φ^f\}

技术创新点

1. 网格对齐策略

  • 极坐标变换: 对于圆形轨迹和障碍物，使用极坐标(θ,r)(θ, r)
  • 能量变换: 利用系统不变量（如机械能）作为变换维度
  • 多项式拟合: 通过拟合决策边界自动生成变换

2. 理论保证

定理1: 变换方法的正确性

  • 变换空间中的安全策略σY(t)=σG([t]G)σ_Y(t) = σ_G([t]_G)
  • 原始空间中的安全策略σX(s)=σG([f(s)]G)σ_X(s) = σ_G([f(s)]_G)

3. 计算优化

  • 三步计算: f−1→δS→ff^{-1} → δ_S → f
  • 集合扩展: 自然处理非双射变换
  • 按需计算: 避免预计算完整转移系统

实验设置

案例研究

1. 卫星模型 (Satellite Model)

  • 状态空间: (x,y)∈[−2,2]×[−2,2](x, y) ∈ [-2, 2] × [-2, 2]
  • 变换: 极坐标 f(x,y)=(atan2(y,x),x2+y2)Tf(x, y) = (atan2(y, x), \sqrt{x^2 + y^2})^T
  • 动作: {ahead,out,in}\{ahead, out, in\}
  • 安全约束: 避障 + 距离限制

2. 弹球模型 (Bouncing Ball Model)

  • 状态空间: (v,p)∈[−13,13]×[0,8](v, p) ∈ [-13, 13] × [0, 8]
  • 变换: 机械能 f(v,p)=(mgp+12mv2,v)Tf(v, p) = (mgp + \frac{1}{2}mv^2, v)^T
  • 目标: 保持球持续弹跳

3. 倒立摆模型 (Cart-Pole Model)

  • 状态空间: (θ,ω)∈[−2.095,2.095]×[−3,3](θ, ω) ∈ [-2.095, 2.095] × [-3, 3]
  • 变换: 多项式拟合 f(θ,ω)=(θ,ω−p(θ))Tf(θ, ω) = (θ, ω - p(θ))^T
  • 目标: 保持杆直立

评价指标

  • 网格单元数量: 衡量计算复杂性
  • 计算时间: 合成效率
  • 决策树节点数: 策略表示复杂性
  • 累积奖励: 强化学习性能

实验结果

主要结果

网格规模减少

模型原始空间单元数变换空间单元数减少倍数
卫星176,40027,3006.5×
弹球520,000650800×
倒立摆9004002.25×

计算时间改进

  • 卫星模型: 从2分41秒减少到10秒
  • 弹球模型: 从19分钟减少到1.3秒（三个数量级）
  • 倒立摆: 从512毫秒减少到244毫秒

决策树表示

通过决策树表示进一步减少存储需求：

  • 卫星：从4,913节点减少到544节点
  • 弹球：从940节点减少到49节点
  • 倒立摆：从99节点减少到32节点

强化学习性能

在1000个episode的累积奖励对比中：

  • 卫星模型: 变换屏蔽达到最高奖励1.499
  • 弹球模型: 变换屏蔽达到最低成本36.593
  • 倒立摆: 变换屏蔽达到最低成本0.000

结果表明变换屏蔽不仅计算效率更高，而且实际性能更优。

重要发现

  1. 变换选择关键: 合适的变换可以带来数量级的性能提升
  2. 不变量利用: 利用系统不变量（如能量、角动量）效果显著
  3. 自动变换可行: 无领域知识的变换工程方法是可行的
  4. 性能提升: 变换不仅提高效率，还改善最终控制器性能

相关工作

抽象控制器合成

  • 传统方法: 基于规则超矩形网格的符号转换系统
  • 多层抽象: 使用不同尺寸网格的多层方法
  • 椭球抽象: 近期使用椭球类网格抽象的努力

屏蔽技术

  • Uppaal Stratego: 工具实现和应用
  • 概率屏蔽: 使用概率屏蔽的安全强化学习
  • 模型预测控制: 安全模型预测控制的相似概念

状态空间变换相关

  • 抽象解释: Galois连接中的抽象和具体化函数
  • 模型降阶: 降低系统维度的近似方法
  • 双模拟: 基于双模拟的状态空间约简

结论与讨论

主要结论

  1. 状态空间变换是屏蔽合成的强大工具，能够显著提高计算效率
  2. 理论正确性得到保证，安全属性从变换空间正确转移到原始空间
  3. 实际应用价值高，不仅提高计算效率还改善控制性能
  4. 方法具有通用性，适用于多种类型的控制系统

局限性

  1. 变换选择依赖性: 变换质量直接影响方法效果
  2. 领域知识需求: 前两个案例需要领域专业知识
  3. 非双射变换: 可能引入额外的近似误差
  4. 适用范围: 主要适用于可以找到合适变换的系统

未来方向

  1. 自动变换发现: 开发更通用的自动变换生成方法
  2. 多变换组合: 研究变换族的组合使用
  3. 在线变换: 探索运行时自适应变换
  4. 扩展集成: 与多层抽象等正交方法结合

深度评价

优点

  1. 创新性强: 首次系统性地将状态空间变换应用于屏蔽合成
  2. 理论完备: 提供了完整的理论分析和正确性证明
  3. 实验充分: 三个不同类型的案例研究验证了方法的广泛适用性
  4. 实用价值高: 数量级的性能提升具有重要的实际意义
  5. 方法通用: 可与现有的网格抽象方法正交结合

不足

  1. 变换设计挑战: 对于复杂系统，找到合适变换仍然困难
  2. 自动化程度: 第三个案例的自动方法还不够成熟
  3. 理论分析: 缺乏关于何时存在好变换的理论指导
  4. 比较基准: 与其他非网格方法的比较不够充分

影响力

  1. 学术贡献: 为控制系统安全合成领域提供了新的研究方向
  2. 实用价值: 显著的性能提升使得更复杂系统的安全合成成为可能
  3. 可复现性: 提供了完整的实现和重现包
  4. 扩展性: 方法可以扩展到其他抽象和合成技术

适用场景

  1. 具有几何结构的系统: 如机器人导航、航天器控制
  2. 存在物理不变量的系统: 如能量守恒系统
  3. 需要高效安全合成的应用: 嵌入式系统、实时控制
  4. 强化学习安全应用: 需要安全保证的学习系统

参考文献

论文引用了31篇相关文献，涵盖了控制理论、形式化方法、强化学习和抽象解释等多个领域的重要工作，为研究提供了坚实的理论基础。

总体评价: 这是一篇高质量的研究论文，提出了创新性的解决方案来应对屏蔽合成中的计算挑战。方法具有强理论基础和显著实用价值，为控制系统安全合成领域做出了重要贡献。