Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems
Authors: Hongchao Zhang, Mohamad H. Kazma, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha
Organizations: Department of Computer Science, Vanderbilt University, Nashville, TN 37235 USA. · Department of Civil and Environmental Engineering, Vanderbilt University, Nashville, TN 37235 USA.
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.
Figures & tables
Figure 1: Conceptual illustration of hidden infeasibility in standard CBF safety filters when applied to DAE systems. The algebraic constraint manifold M={x:ϕ(x)=0} imposes an additional compatibility requirement on the control input that is not accounted for by standard CBF conditions, which may render the safety filter infeasible even when the state lies within the safe set C .
Figure 2: Geometric illustration of Problem 1 . The state space contains the constraint manifold M , the safe set C , and the candidate barrier set D . The goal is to design a barrier function b(x) and a safe control policy μ such that D∩M⊆C∩M is positively invariant under the closed-loop DAE dynamics ( 1 ), ensuring that all system trajectories initialized in D∩M evolve on the constraint manifold and remain within the safe set for all t≥0 .
Figure 3: Simulation results for Example 1 using a DAE-unaware CBF. The figure shows (a) the CBF-QP trajectory on the constraint manifold ϕ(x)=0 , (b) the evolution of the barrier function b(x) (with b(x0)=0.130 and a minimum b(x)=−0.1059 ), and (c) the evolution of the safe set function h(x) (a minimum h(x)=−0.1059 ). The CBF-QP becomes infeasible when the CBF inequality conflicts with the algebraic equality constraints, leading to violation of the safety condition b(x)≥0 .
Subsection
Key Concept
Main Results
3.1 Preliminaries
Lie derivatives + relative deg.
Defs. 5 - 6 ; Thm. 2
3.2 Projected Fields
Revealing hidden dynamics
Eq. 10 ; Lem. 1
3.3 Index-1 DAEs
Compatibility + safety
Thm. 4 ; Cor. 4.1
3.4 Higher-Index
ν -order diff. + projection
Prop. 1 ; Thm. 5
Table I: Summary of Main Results for DAE-Aware CBF Construction, outlining the key concepts in each subsection.
Figure 4: Roadmap for the derivation of DAE-aware CBF conditions for index-1 systems. The algebraic constraints ϕ(x)=0 are differentiated to expose the compatibility condition and the constraint Jacobians Jd(x) and Ja(x) . Under the invertibility assumption on Ja(x) , the algebraic states are eliminated via the implicit function theorem, and the DAE ( 1 ) is projected onto the constraint manifold M . The CBF condition is then lifted back to the full state space, producing DAE-aware CBF conditions that jointly enforce manifold compatibility and positive invariance of D∩M .
Figure 5: Roadmap for deriving DAE-aware CBF conditions for higher-index systems ( ν≥2 ). The algebraic constraint ϕ(x)=0 is differentiated successively up to order ν , eliminating time derivatives via ( 1a ) at each step, until the control input appears explicitly in the extended constraint system. Full row rank of Jext(ν)(x) then yields a projected control-affine representation on M , from which the DAE-aware CBF conditions follow analogously to the index-1 case.
Figure 6: Roadmap for the verification of a candidate DAE-aware CBF b(x) (Problem 2 ). The framework consists of Left: the correctness branch verifies that D∩M⊆C∩M via an SOS program ( 28 ) for polynomial systems, or a nonlinear program (NLP) counterexample search ( 29 ) in the general case. Right: the feasibility branch applies Farkas duality to the affine input constraint system (Adae,rdae) , decomposing the feasibility certificate into an interior condition ( 36 ) and a boundary tangency condition ( 37 ). Both branches are unified in Theorem 7 : if correctness, interior feasibility, and boundary tangency all hold, then b(x) is certified as a valid DAE-aware CBF.
Figure 7: Simulation results for the DAE system ( 4 ) using a DAE-aware CBF. The figure shows (a) the CBF-QP trajectory on the constraint manifold ϕ(x)=0 remaining in the safe region, (b) the evolution of the barrier function b(x) (with b(x0)=0.014 and a minimum b(x(t))=0.0131 ), and (c) the evolution of the safe set function h(x) (with a minimum h(x(t))=0.0128 ). Both b(x) and h(x) remain positive over the horizon, indicating safety and feasibility.
Property
SMT (Z3)
SOS ( d=2 )
SOS ( d=4 )
#params
time (s)
#params
time (s)
#params
time (s)
Correctness
3
0.01
60
0.04
280
N/A
Interior
7
120.65
405
5.77
8,235
N/A
Boundary
7
126.08
405
5.30
7,695
N/A
Total
17
246.74
870
11.11
16,360
N/A
Table II: Wind turbine: problem size and runtime. Each entry reports the number of parameters and runtime for verifying the corresponding property. Degree-4 SOS timing is omitted due to excessive cost (N/A).
Item
Polynomial
NN (Z3)
Arch
b(x)=h(x)
8–8–tanh–8–tanh–1
Verifier
SOS ( d=2 )
Z3
Subproblem
#params
time (s)
#SMT vars
time (s)
Correctness
165
0.09
3
1.84 ( UNSAT )
Interior
2,565
4.90
4
1.77 ( UNSAT )
Boundary
2,565
4.48
5
1.74 ( UNSAT )
Table III: Flexible link manipulator: problem size and runtime. Each entry reports the problem size and runtime for the corresponding verification subproblem. #SMT vars denotes the number of free real variables in each SMT verification query. The NN has 153 stored parameters, with 4 independent trained quantities. NN times cover the complete verification process; Total sums times only. UNSAT denotes a passed verification check.
Figure 8: Simulation results for the flexible link manipulator. The figure shows (a) the trajectory in configuration space (θ1,θ2,ytip) , where the trajectory (blue) starts at the green marker and ends at the red marker, remaining within the safe region ( b(x)≥0 , green surface) and below the safety limit (red plane). (b) The manipulator trajectory in workspace, where the end-effector path (yellow) remains below the safety limit ymax=1.8m (red dashed); the snapshots indicate the manipulator configuration at selected times. (c) Evolution of the barrier function along the trajectory (with b(x0)=1.800 and with a minimum b(x(t))=0.2320 ), confirming that b(x(t))≥0∀t .
Formal verification of neural control barrier functions (NCBFs) remains challenging, especially for neural networks with nonlinear activations like tanh. Existing CROWN-based methods rely on conservative linear relaxations for Jacobian bounds, limiting scalability. We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions. Experiments on nonlinear control systems including the inverted pendulum, Dubins car, and planar quadrotor demonstrate that LightCROWN improves verification success rates up to 100%, while enhancing speed and scalability. Our approach provides a generalizable improvement for CROWN-based frameworks, enabling more efficient verification of complex NCBFs. The code can be found at github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF.
Jun Zhang, Haibo Zhang, Chun Liu +2
School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China +1
We consider safety-critical multi-agent systems with distributed control architectures and potentially varying network topologies. While learning-based distributed control enables scalability and high performance, a lack of formal safety guarantees in the face of unforeseen disturbances and unsafe network topology changes may lead to system failure. To address this challenge, we introduce structured control barrier functions (s-CBFs) as a multi-agent safety framework. The s-CBFs are augmented to a distributed predictive control barrier function (D-PCBF), a predictive, optimization-based safety layer that uses model predictions to guarantee recoverable safety at all times. The proposed approach enables a permissive yet formal plug-and-play protocol, allowing agents to join or leave the network while ensuring safety recovery if a change in network topology requires temporarily unsafe behavior. We validate the formulation through simulations and real-time experiments of a miniature race-car platoon.
Jonas Ohnemus, Alexandre Didier, Ahmed Aboudonia +2
Institute for Dynamic Systems and Control, ETH Zurich, 8092 Zurich, Switzerland · University of California Berkeley, 94720 CA, USA
Control Barrier Functions (CBFs) can provide provable safety guarantees for dynamic systems. However, finding a valid CBF for a system of interest is often non-trivial, especially for systems with low computational resources, higher-order dynamics, and moving close to obstacles of complex shape. A common solution to this problem is to use a purely distance-based CBF. In this paper, we study Hyperplane CBFs (H-CBFs), where a hyperplane separates the agent from the obstacle. First, we note that the common distance-based CBF is a special case of an H-CBF where the hyperplane is a supporting hyperplane of the obstacle that is orthogonal to a line between the agent and the closest point of the obstacle. We then show that a less conservative CBF can be found by optimising over the orientation of the supporting hyperplane, in order to find the Least Restrictive Hyperplane CBF. This enables us to maintain the safety guarantees while allowing controls that are closer to the desired ones, especially when moving fast and passing close to obstacles. We illustrate the approach on a double integrator dynamical system with acceleration constraints, moving through a group of arbitrarily shaped static and moving obstacles, and show that the proposed approach reduces the average gap between desired and safe controls by an order of magnitude.
Mattias Trende, Petter Ögren
The authors are with the Robotics, Perception and Learning Lab., School of Electrical Engineering and Computer Science, Royal Institute of Technology (KTH), SE-100 44 Stockholm, Sweden