Computing Control Lyapunov-Barrier Functions: Softmax Relaxation and Smooth Patching with Formal Guarantees
Jun Liu, Maxwell Fitzsimmons
TL;DR
This paper addresses safe stabilization of nonlinear control-affine systems by constructing a single smooth Lyapunov-barrier function $W$ (a CLBF) that certifies both asymptotic stability and safety. The authors introduce a log-sum-exp softmax relaxation $h_{ ext{sm}}(x;\tau)$ to enlarge the certifiable safe set while preserving differentiability, and employ counterexample-guided refinement to enforce a strict barrier condition. A smooth patching theorem then combines a strictly compatible CBF $h$ and CLF $V$ into $W$, yielding an exact representation of the safe set as $\{W(x)\le 1\}$ with guaranteed decrease along system trajectories; the construction is SMT-verifiable via a Farkas’ lemma reformulation to handle boundary-band compatibility. The framework is demonstrated on benchmarks including a power converter, where the resulting CLBF often provides less conservative safe stabilization regions than state-of-the-art SOS-compatible designs, while offering formal guarantees. Overall, the work delivers a scalable, formally verified method for safe stabilization by unifying safety and stability into a single, smooth certificate.
Abstract
We present a computational framework for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety. We show that the existence of a strictly compatible pair of control barrier and control Lyapunov functions (CBF-CLF) guarantees the existence of such a function on the exact safe set certified by the barrier. To maximize the certifiable safe domain while retaining differentiability, we employ a log-sum-exp (softmax) relaxation of the nonsmooth maximum barrier, together with a counterexample-guided refinement that inserts half-space cuts until a strict barrier condition is verifiable. We then patch the softmax barrier with a CLF via an explicit smooth bump construction, which is always feasible under the strict compatibility condition. All conditions are formally verified using a satisfiability modulo theories (SMT) solver, enabled by a reformulation of Farkas' lemma for encoding strict compatibility. On benchmark systems, including a power converter, we show that the certified safe stabilization regions obtained with the proposed approach are often less conservative than those achieved by state-of-the-art sum-of-squares (SOS) compatible CBF-CLF designs.