Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification and Synthesis of Compatible Control Lyapunov and Control Barrier Functions

Hongkai Dai, Chuanrui Jiang, Hongchao Zhang, Andrew Clark

TL;DR

This work addresses ensuring joint safety and stability by verifying and synthesizing compatible Control Lyapunov Functions (CLFs) and Control Barrier Functions (CBFs) for control-affine systems, without relying on nominal controllers. It derives necessary and sufficient compatibility conditions via Farkas' Lemma and the Positivstellensatz, and implements tractable SOS programs (simplified with the S-procedure) for compatibility verification. It then proposes a bilinear alternating synthesis strategy to enlarge the compatible region, demonstrated on a toy system and a 13-state quadrotor, with open-source code available. The results show that compatible CLF/CBF pairs exist and can be expanded to ensure simultaneous safety and stability under input constraints, enabling robust CLF-CBF-QP control in nonlinear settings.

Abstract

Safety and stability are essential properties of control systems. Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are powerful tools to ensure safety and stability respectively. However, previous approaches typically verify and synthesize the CBFs and CLFs separately, satisfying their respective constraints, without proving that the CBFs and CLFs are compatible with each other, namely at every state, there exists control actions within the input limits that satisfy both the CBF and CLF constraints simultaneously. Ignoring the compatibility criteria might cause the CLF-CBF-QP controller to fail at runtime. There exists some recent works that synthesized compatible CLF and CBF, but relying on nominal polynomial or rational controllers, which is just a sufficient but not necessary condition for compatibility. In this work, we investigate verification and synthesis of compatible CBF and CLF independent from any nominal controllers. We derive exact necessary and sufficient conditions for compatibility, and further formulate Sum-Of-Squares programs for the compatibility verification. Based on our verification framework, we also design a nominal-controller-free synthesis method, which can effectively expands the compatible region, in which the system is guaranteed to be both safe and stable. We evaluate our method on a non-linear toy problem, and also a 3D quadrotor to demonstrate its scalability. The code is open-sourced at \url{https://github.com/hongkai-dai/compatible_clf_cbf}.

Verification and Synthesis of Compatible Control Lyapunov and Control Barrier Functions

TL;DR

This work addresses ensuring joint safety and stability by verifying and synthesizing compatible Control Lyapunov Functions (CLFs) and Control Barrier Functions (CBFs) for control-affine systems, without relying on nominal controllers. It derives necessary and sufficient compatibility conditions via Farkas' Lemma and the Positivstellensatz, and implements tractable SOS programs (simplified with the S-procedure) for compatibility verification. It then proposes a bilinear alternating synthesis strategy to enlarge the compatible region, demonstrated on a toy system and a 13-state quadrotor, with open-source code available. The results show that compatible CLF/CBF pairs exist and can be expanded to ensure simultaneous safety and stability under input constraints, enabling robust CLF-CBF-QP control in nonlinear settings.

Abstract

Safety and stability are essential properties of control systems. Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are powerful tools to ensure safety and stability respectively. However, previous approaches typically verify and synthesize the CBFs and CLFs separately, satisfying their respective constraints, without proving that the CBFs and CLFs are compatible with each other, namely at every state, there exists control actions within the input limits that satisfy both the CBF and CLF constraints simultaneously. Ignoring the compatibility criteria might cause the CLF-CBF-QP controller to fail at runtime. There exists some recent works that synthesized compatible CLF and CBF, but relying on nominal polynomial or rational controllers, which is just a sufficient but not necessary condition for compatibility. In this work, we investigate verification and synthesis of compatible CBF and CLF independent from any nominal controllers. We derive exact necessary and sufficient conditions for compatibility, and further formulate Sum-Of-Squares programs for the compatibility verification. Based on our verification framework, we also design a nominal-controller-free synthesis method, which can effectively expands the compatible region, in which the system is guaranteed to be both safe and stable. We evaluate our method on a non-linear toy problem, and also a 3D quadrotor to demonstrate its scalability. The code is open-sourced at \url{https://github.com/hongkai-dai/compatible_clf_cbf}.

Paper Structure

This paper contains 14 sections, 6 theorems, 26 equations, 3 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Mathematical background
  3. Problem statement
  4. System Model
  5. Control Barrier Function (CBF) and Control Lyapunov Function (CLF)
  6. Methodology
  7. Verification of compatibility
  8. Compatibility Verification
  9. CBF Correctness Verification
  10. Compatible CBF and CLF synthesis
  11. Results
  12. Toy system
  13. Quadrotor
  14. Conclusion

Key Result

Theorem 1

Let $\left(\phi_{j}\right)_{j=1, \ldots, s}$, $\left(\psi_{\ell}\right)_{\ell=1, \ldots, r}$ be finite families of polynomials in $\mathbb{R}\left[\mathbf{x}\right]$. Denote the cone generated from $\left(\phi_{j}\right)_{j=1, \ldots, s}$ by $\Sigma[\phi_{1},\ldots,\phi_{s}]$ , and the ideal generat

Figures (3)

  • Figure 1: With the CLF-CBF-QP controller, the quadrotor converges to the desired goal (red sphere in the center) from different initial states, while avoiding the grey ground. The compatible CLF/CBF are synthesized by our algorithm. We also plot each trajectory of the quadrotor body origin with a different color.
  • Figure 2: Results of jointly synthesizing compatible CLF/CBF (Fig \ref{['fig:nonlinear_toy_compatible']}, our approach), and separately synthesizing incompatible CLF/CBF (Fig \ref{['fig:nonlinear_toy_incompatible']}, previous approach) for the nonlinear toy example.
  • Figure 3: CLF/CBF trajectories of the quadrotor while simulated with the CLF-CBF-QP controller.

Theorems & Definitions (8)

  • Theorem 1: Positivstellensatz (P-satz)parrilo2000structured
  • Lemma 1: S-procedure
  • Lemma 2: Farkas' Lemma matousek2006understanding
  • Definition 1: CBF ames2019control
  • Definition 2: CLF sontag1989universal
  • Lemma 3
  • Lemma 4
  • Theorem 2