Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls

TL;DR

This paper introduces verifiable conditions for synthesizing a smooth control Lyapunov function that guarantees both stability and safety under bounded controls, improving upon existing less conservative methods.

Contribution

It provides a novel, less conservative approach to jointly synthesize control Lyapunov and barrier functions ensuring safety and stability with explicit construction methods.

Findings

The method guarantees safety and stability under bounded controls.

Constructs a smooth control Lyapunov-barrier function explicitly.

Less conservative than sum-of-squares based designs.

Abstract

We present verifiable conditions for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety under bounded controls. These sufficient conditions ensure the strict compatibility of a control barrier function (CBF) and a control Lyapunov function (CLF) on the exact safe set certified by the barrier. An explicit smooth control Lyapunov-barrier function (CLBF) is then constructed via a patching formula that is provably correct by design. Two examples illustrate the computational procedure, showing that the proposed approach is less conservative than sum-of-squares (SOS)-based compatible CBF-CLF designs.