为微分代数系统设计可验证的安全控制方法
Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems
- 基于投影向量场构建适配DAE结构的屏障函数
- 确保安全集前向不变性且满足代数约束
- 支持多项式与神经网络模型的可验证性分析
微分代数方程（DAEs）广泛存在于电力网络、化工过程和多体系统中，其代数约束反映物理守恒规律。系统的安全性至关重要，但因代数约束限制状态轨迹，安全控制极具挑战。控制屏障函数（CBFs）在常微分方程（ODE）系统中提供高效的计算安全过滤器，但现有方法无法直接应用于DAEs，因CBF条件可能与约束流形冲突。本文提出一种考虑DAE结构的屏障函数，通过投影向量场建模，并推导出保证安全集前向不变性且保持代数约束的条件，进一步扩展至高指标DAE。建立了系统化验证框架，给出几何正确性和可行性所需的充要条件：对多项式系统使用平方和证书，对非多项式及神经网络候选者采用满足性模理论进行反例检测。方法在风力涡轮机与柔性连杆机械臂系统上验证有效。
原文摘要 · Abstract (English)
Differential-algebraic equations (DAEs) arise in power networks, chemical processes, and multibody systems, where algebraic constraints encode physical conservation laws. The safety of such systems is critical, yet safe control is challenging because algebraic constraints restrict allowable state trajectories. Control barrier functions (CBFs) provide computationally efficient safety filters for ordinary differential equation (ODE) systems. However, existing CBF methods are not directly applicable to DAEs due to potential conflicts between the CBF condition and the constraint manifold. This paper introduces DAE-aware CBFs that incorporate the differential-algebraic structure through projected vector fields. We derive conditions that ensure forward invariance of safe sets while preserving algebraic constraints and extend the framework to higher-index DAEs. A systematic verification framework is developed, establishing necessary and sufficient conditions for geometric correctness and feasibility of DAE-aware CBFs. For polynomial systems, sum-of-squares certificates are provided, while for nonpolynomial and neural network candidates, satisfiability modulo theories are used for falsification. The approach is validated on wind turbine and flexible-link manipulator systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。