基于有界控制输入的安全稳定控制Lyapunov-Barrier函数的形式化验证

我们提出了用于合成单一光滑Lyapunov函数以在有界控制输入下 certify 渐近稳定性和安全性的可验证条件。这些充分条件确保了控制屏障函数（CBF）与控制Lyapunov函数（CLF）在由屏障确立的确切安全集上的严格兼容性。随后通过一种可被证明按设计正确的补丁公式构造了一个显式的光滑控制Lyapunov-Barrier函数（CLBF）。两个示例说明了计算程序，显示所提出的方法比基于 sum-of-squares（SOS）的兼容CBF-CLF设计更不保守。