Computing Control Lyapunov-Barrier Functions: Softmax Relaxation and Smooth Patching with Formal Guarantees
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908573690232832 |
|---|---|
| author | Liu, Jun Fitzsimmons, Maxwell |
| author_facet | Liu, Jun Fitzsimmons, Maxwell |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_02223 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computing Control Lyapunov-Barrier Functions: Softmax Relaxation and Smooth Patching with Formal Guarantees Liu, Jun Fitzsimmons, Maxwell Systems and Control Optimization and Control 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. |
| title | Computing Control Lyapunov-Barrier Functions: Softmax Relaxation and Smooth Patching with Formal Guarantees |
| topic | Systems and Control Optimization and Control |
| url | https://arxiv.org/abs/2510.02223 |