Papers › Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided...
Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis (Extended Version)
Chiao Hsieh, Masaki Waga, Kohei Suenaga
Finding Lyapunov functions to certify the stability of control systems has been an important topic for verifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications. Our work stems from the recent idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bounds on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination. Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. Our visualization also reveals the regions where the stability is difficult to prove. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections