Sampling Quotient-Ring Sum-of-Squares Programs for Scalable Verification of Nonlinear Systems
Sampling Quotient-Ring Sum-of-Squares Programs for Scalable Verification of Nonlinear Systems
复制标题
用于非线性系统可扩展验证的采样商环平方和程序
DOI：
10.1109/cdc42340.2020.9304028
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Russ Tedrake
中科院分区：
文献类型：
--
作者：
Shen Shen;Russ Tedrake
本文提出了一种新颖的方法，结合新的公式和采样，以提高基于平方和（SOS）编程的系统验证的可扩展性。考虑多项式、具有广义 Lur’e 不确定性的多项式和有理三角多刚体系统的吸引区域近似问题。我们的方法首先确定传统上大量用于 S 程序的拉格朗日乘子是创建臃肿的 SOS 程序的罪魁祸首。有鉴于此，我们利用固有的系统属性（连续性、凸性和隐式代数结构）并将问题重新表述为商环 SOS 程序，从而消除所有乘数。这些新计划规模更小、更稀疏、限制更少，但也不那么保守。通过利用最近的代数簇采样结果，他们的计算得到了进一步改进。值得注意的是，只需有限（实际上非常少）数量的样本即可保证解的正确性。总而言之，所提出的方法可以验证系统，远远超出现有基于 SOS 的方法（32 个状态）的范围；对于有基线可用的较小问题，它计算更严格的解决方案的速度快 2-3 个数量级。
This 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.