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

TL;DR

This paper develops a new framework for verifying and ensuring safety in differential-algebraic systems using control barrier functions, addressing the challenges posed by algebraic constraints and extending applicability to complex systems.

Contribution

It introduces DAE-aware CBFs that incorporate algebraic constraints, along with a verification framework for their correctness and feasibility, applicable to polynomial and nonpolynomial systems.

Findings

Verified safety of wind turbine system

Ensured forward invariance of safe sets in DAEs

Extended CBF methods to higher-index DAEs

Abstract

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.