Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls
Systems and Control
2025-11-14 v1 Systems and Control
Optimization and Control
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.
Keywords
Cite
@article{arxiv.2511.10510,
title = {Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls},
author = {Jun Liu},
journal= {arXiv preprint arXiv:2511.10510},
year = {2025}
}