⚡ electrical engineering

Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems

本文针对微分代数方程（DAE）系统，提出了一种融合投影向量场的 DAE 感知控制障碍函数（CBF）框架，通过建立几何正确性与可行性的充要条件及相应的验证方法，解决了代数约束与 CBF 条件冲突的难题，从而确保了系统安全集的前向不变性。

原作者： Hongchao Zhang, Mohamad H. Kazma, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha

发布于 2026-03-17

📖 1 分钟阅读☕ 轻松阅读

原作者： Hongchao Zhang, Mohamad H. Kazma, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha

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

这篇论文解决了一个非常棘手的问题：如何给那些“既受物理定律限制，又受安全规则约束”的复杂机器设计一套“自动驾驶”系统，确保它们既不会撞车，也不会违反物理定律。

为了让你更容易理解，我们可以把这篇论文的核心思想想象成**“在走钢丝的同时还要玩杂耍”**。

1. 背景：什么是 DAE 系统？（走钢丝的杂技演员）

想象一个杂技演员（比如风力发电机或机械臂），他在走钢丝。

普通系统 (ODE)：就像在平地上跑步。你想往哪跑，只要脚够力，就能往哪跑。
微分代数方程系统 (DAE)：就像在走钢丝。
- 微分部分：演员可以移动（像跑步一样）。
- 代数部分：但他必须时刻踩在钢丝上（这是物理守恒定律，比如能量守恒、电路定律）。如果脚离开了钢丝，物理世界就崩塌了（系统失效）。

问题出在哪？
以前的“安全控制器”（CBF）就像是一个只关心“别掉进坑里”的教练。教练会喊：“往左跑！别掉坑里！”
但在走钢丝时，如果教练喊“往左跑”，而左边是悬崖（钢丝边缘），或者往左跑会导致脚离开钢丝（违反物理定律），这个教练的指令就是无效的。

后果：系统试图执行指令，结果发现“指令”和“钢丝”冲突，导致系统卡死（数学上叫“不可行”），或者直接掉下去（发生安全事故）。

2. 核心创新：DAE 感知的 CBF（懂走钢丝的教练）

这篇论文提出了一种**“懂走钢丝的教练”**（DAE-aware CBF）。

以前的做法：教练只看“安全区域”，完全忽略“钢丝”的存在。结果指令发出去，演员发现根本做不到，系统崩溃。
新做法：教练在发出指令前，先投影了一下。
- 比喻：教练不再直接喊“往左跑”，而是先算一下：“往左跑会不会踩空？如果会，那就在钢丝允许的范围内，往左偏一点点。”
- 技术原理：他们发明了一种**“投影向量场”。这就好比给所有的指令加了一个“滤镜”，强制把所有指令都压扁**在钢丝（约束流形）上。这样，无论教练怎么喊，演员的动作永远都在钢丝上，同时又能避开危险区域。

3. 处理更复杂的情况（高指数 DAE）

有些系统不仅要在钢丝上走，还要在钢丝上倒立，或者钢丝本身还在晃动（高指数 DAE）。

比喻：这时候，简单的“踩在钢丝上”不够了，你还需要知道“倒立时重心怎么变”、“钢丝晃动时怎么调整”。
论文贡献：他们把这套方法升级了，不仅考虑“踩在钢丝上”，还考虑了**“隐藏的规则”**。比如，有些规则不是直接写在钢丝上的，而是你走一步、再走一步、再走一步（求导多次）才能发现的。论文通过一种“高阶”的数学工具，把这些隐藏规则也变成了教练的指令，确保系统在任何复杂情况下都能稳如泰山。

4. 验证：如何证明教练是靠谱的？（数学考试）

光有教练还不够，你得证明这个教练真的不会害死人。

以前的验证：大概看看，或者模拟一下。
这篇论文的验证：搞了一套**“数学考试”**。
- 多项式系统：用“求和平方”（SOS）的方法，就像给教练的每一个指令都盖上一个“数学印章”，证明它在数学上绝对成立。
- 神经网络/复杂系统：用“可满足性模理论”（SMT），就像请了一个超级严格的考官，试图找出教练指令里的任何漏洞（反例）。如果考官找了一整天都找不到漏洞，那就证明教练是安全的。

5. 实际效果：风力发电机和机械臂

论文在两个真实场景里测试了这套方法：

风力发电机：以前的方法会让发电机在强风下因为指令冲突而“死机”或失控。新方法让发电机在遵守物理定律的同时，稳稳地避开危险转速。
柔性机械臂：这是一个像蛇一样柔软的机械臂。以前的方法会让它乱扭甚至折断。新方法让它既能灵活运动，又不会超出安全高度，同时严格遵守关节的物理限制。

总结

这篇论文就像是为那些**“戴着镣铐跳舞”的复杂机器（如电网、化工厂、机器人）设计了一套“智能舞伴”**。

旧舞伴：只顾着让你别摔倒，不管你的脚是不是被绳子绑住了，结果把你绊倒。
新舞伴（DAE-aware CBF）：不仅知道怎么不摔倒，还精通绳子的规则。它会在绳子的限制范围内，完美地引导你跳出最安全的舞蹈。

一句话概括：这是一套让复杂机器在严格遵守物理定律的前提下，也能绝对安全运行的“智能导航系统”，并且我们还能用数学证明它绝对不会出错。

论文技术总结：微分代数系统的控制屏障函数验证与前向不变性

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

背景：
微分代数方程（DAEs）广泛应用于电力系统、化工过程和机械多体系统中，用于描述包含物理守恒定律（如质量、能量守恒）的代数约束。传统的控制屏障函数（Control Barrier Functions, CBFs）是处理常微分方程（ODE）系统在线安全控制的高效工具，能够实时合成安全滤波器。

核心问题：
现有的 CBF 方法直接应用于 DAE 系统时存在根本性缺陷。

可行性冲突： 标准 CBF 假设存在满足安全条件的控制输入，但 DAE 系统的代数约束限制了状态轨迹的演化空间。当 CBF 条件与代数约束流形（Constraint Manifold）发生冲突时，会导致安全滤波器（通常为二次规划 QP）无解（Infeasible），进而引发安全违规。
缺乏理论框架： 虽然已有针对特定 DAE 系统（如柔性机械臂）的研究，但缺乏通用的、能够处理任意指数（Index）DAE 系统的 CBF 设计框架，且未明确区分微分指数与屏障函数相对阶（Relative Degree）之间的关系。
验证缺失： 缺乏针对 DAE 系统候选 CBF 的形式化验证方法，无法保证几何正确性（安全集包含关系）和可行性（控制输入存在性）。

目标：
提出一种"DAE 感知（DAE-aware）”的 CBF 框架，通过投影向量场显式地处理代数约束，确保安全集的前向不变性，同时满足代数约束，并建立系统的验证方法。

2. 方法论 (Methodology)

本文提出了一套完整的理论框架，涵盖从系统建模、控制器设计到形式化验证的全过程。

2.1 DAE 感知 CBF 的构建 (DAE-aware CBF Construction)

核心思想是将 DAE 系统投影到由代数约束定义的流形 $M$ 上，构建等效的受控向量场。

投影向量场 (Projected Vector Fields)：
- 利用代数约束 $\phi(x)=0$ 及其导数，推导出代数状态导数 $\dot{x}_a$ 与微分状态导数 $\dot{x}_d$ 及控制输入 $u$ 之间的相容性条件。
- 定义投影算子 $P(x)$ ，将原始向量场 $f(x), g(x)$ 投影到流形 $M$ 上，得到投影后的向量场 $\hat{f}(x)$ 和 $\hat{g}(x)$ 。
- 在流形上，DAE 系统被转化为等效的 ODE 系统 $\dot{x} = \hat{f}(x) + \hat{g}(x)u$ ，且该演化自动满足代数约束。
针对不同指数的处理：
- 指数为 1 的 DAE (Index-1)： 直接对代数约束求一次导数，利用雅可比矩阵的可逆性（或广义逆）消除代数变量，构建投影向量场。
- 高指数 DAE (Higher-Index, $\nu \ge 2$ )： 需要对方程进行 $\nu$ 次微分以显式暴露控制输入 $u$ 。论文建立了微分指数 $\nu$ 与屏障函数相对阶 $d$ 之间的关系（ $d = \nu + d' - 1$ ），并提出了高阶 CBF (HOCBF) 条件，以处理隐藏约束。
安全条件：
设计控制输入 $u$ 需同时满足两个条件：
1. 流形不变性 (Manifold Invariance)： 满足投影相容性方程，确保轨迹始终停留在流形 $M$ 上。
2. 安全集不变性 (Safety Invariance)： 在投影后的向量场上满足 CBF 不等式（或 HOCBF 层级不等式），确保 $b(x) \ge 0$ 。

2.2 形式化验证框架 (Formal Verification)

为了证明候选 CBF 的有效性，论文提出了包含几何正确性和可行性的验证框架：

几何正确性 (Correctness)： 验证候选安全集 $D$ $D$ 是否包含在真实安全集 $C$ $C$ 内（即 $D \cap M \subseteq C \cap M$ $D \cap M \subseteq C \cap M$ ）。
- 多项式系统： 使用 Sum-of-Squares (SOS) 编程和 Positivstellensatz 定理进行证书搜索。
- 非多项式/神经网络： 使用 Satisfiability Modulo Theories (SMT) 求解器（如 Z3）进行反例搜索（Falsification）。
可行性 (Feasibility)： 验证在 $D \cap M$ $D \cap M$ 的每一点是否存在满足相容性条件和输入约束的控制输入。
- 利用 Farkas 引理 将原问题的可行性转化为对偶系统的不存在性证明。
- 分别针对内部点（Interior）和边界点（Boundary，需满足切向条件）建立验证条件。

3. 主要贡献 (Key Contributions)

DAE 感知 CBF 理论框架： 首次提出显式处理微分代数结构的 CBF 方法。通过投影向量场，将 DAE 系统的安全控制问题转化为流形上的 ODE 问题，解决了标准 CBF 在 DAE 上因代数约束冲突导致的不可行性问题。
高指数 DAE 的扩展与理论关联： 将框架推广至高指数 DAE 系统，形式化地建立了微分指数（Differentiation Index）与屏障函数相对阶（Relative Degree）之间的数学关系，推导出了包含隐藏约束的高阶 CBF 条件。
系统化的验证方法： 开发了针对 DAE 感知 CBF 的验证工具链。
- 对于多项式系统，提供了基于 SOS 的充分必要条件证书。
- 对于非多项式及神经网络表示的 CBF，提供了基于 SMT 的证伪（Falsification）方法。
- 验证涵盖了从几何正确性到控制输入存在性的完整链条。
实验验证： 在风力涡轮机（指数 1）和柔性连杆机械臂（指数 2）两个基准系统上进行了验证。结果表明，DAE 感知 CBF 能保持流形不变性并确保安全，而标准 CBF 会导致 QP 不可行并引发安全事故。

4. 实验结果 (Results)

论文在两个典型 DAE 系统上进行了仿真验证：

案例 1：风力涡轮机系统 (指数 1 DAE)
- 现象： 标准 CBF 方法在仿真中导致二次规划（QP）不可行，系统轨迹偏离安全集，安全函数 $h(x)$ 变为负值。
- DAE 感知 CBF 表现： 引入相容性条件后，QP 始终保持可行。轨迹严格保持在代数约束流形上，且安全函数 $h(x)$ 和屏障函数 $b(x)$ 始终非负。
- 验证： 通过 SOS 和 SMT 方法成功验证了候选 CBF 的正确性、内部可行性和边界切向性。
案例 2：柔性连杆机械臂 (指数 2 DAE)
- 挑战： 系统具有二阶微分指数，且包含三角函数非线性项。
- 方法： 应用了针对高指数系统的 HOCBF 条件（相对阶为 3）。
- 表现： 即使在激进的初始条件下（高角速度），控制器成功调节关节力矩，使末端执行器高度始终低于 1.8m 的安全限制，同时满足代数约束。
- 验证： 对多项式候选和神经网络候选分别进行了 SOS 和 SMT 验证。SMT 验证在合理时间内确认了安全性（尽管内部和边界检查耗时较长，显示了计算复杂性）。

5. 意义与局限性 (Significance & Limitations)

意义：

填补理论空白： 解决了 CBF 方法在 DAE 系统应用中长期存在的“不可行性”难题，为电力、化工等强约束系统的实时安全控制提供了理论依据。
通用性与扩展性： 提出的框架不仅适用于指数 1 系统，还通过高阶投影向量场扩展至高指数系统，具有广泛的适用性。
形式化保证： 结合 SOS 和 SMT 的验证框架，为安全关键系统提供了数学上严格的安全性保证，超越了传统的仿真测试。

局限性与未来工作：

可扩展性： 基于 SOS 和 SMT 的验证方法在处理高维 DAE 系统（如大规模电网）时面临计算瓶颈。
模型不确定性： 当前框架假设系统模型精确已知，未考虑参数不确定性或外部扰动。
合成问题： 目前仅验证给定的候选 CBF，尚未解决如何从安全规范自动合成 DAE 感知 CBF 的问题。

总结：
该论文通过引入投影向量场和形式化验证，成功构建了适用于微分代数系统的安全控制框架，显著提升了复杂物理约束系统的安全控制能力，是控制理论与形式化方法结合的重要进展。