Visible to the public Sampling Quotient-Ring Sum-of-Squares Programs for Scalable Verification of Nonlinear Systems

TitleSampling Quotient-Ring Sum-of-Squares Programs for Scalable Verification of Nonlinear Systems
Publication TypeConference Paper
Year of Publication2020
AuthorsShen, Shen, Tedrake, Russ
Conference Name2020 59th IEEE Conference on Decision and Control (CDC)
Keywordscompositionality, Nonlinear dynamical systems, Optimization, Pipelines, Predictive Metrics, pubcrawl, Resiliency, Scalability, scalable verification, Standards, Task Analysis, Uncertainty
AbstractThis paper presents a novel method, combining new formulations and sampling, to improve the scalability of sum-of-squares (SOS) programming-based system verification. Region-of-attraction approximation problems are considered for polynomial, polynomial with generalized Lur'e uncertainty, and rational trigonometric multi-rigid-body systems. Our method starts by identifying that Lagrange multipliers, traditionally heavily used for S-procedures, are a major culprit of creating bloated SOS programs. In light of this, we exploit inherent system properties-continuity, convexity, and implicit algebraic structure-and reformulate the problems as quotient-ring SOS programs, thereby eliminating all the multipliers. These new programs are smaller, sparser, less constrained, yet less conservative. Their computation is further improved by leveraging a recent result on sampling algebraic varieties. Remarkably, solution correctness is guaranteed with just a finite (in practice, very small) number of samples. Altogether, the proposed method can verify systems well beyond the reach of existing SOS-based approaches (32 states); on smaller problems where a baseline is available, it computes tighter solution 2-3 orders of magnitude faster.
Citation Keyshen_sampling_2020