Counterexample-guided computation of polyhedral Lyapunov functions for piecewise linear systems
Counterexample-guided computation of polyhedral Lyapunov functions for piecewise linear systems
复制标题
DOI：
10.1016/j.automatica.2023.111165
复制
发表时间：
2023-09
期刊：
影响因子：
--
通讯作者：
Guillaume O. Berger;S. Sankaranarayanan
中科院分区：
文献类型：
--
作者：
Guillaume O. Berger;S. Sankaranarayanan
本文提出了一种反例引导的迭代算法来计算连续时间分段线性系统的凸分段线性（多面体）Lyapunov 函数。多面体李雅普诺夫函数提供了常用多项式李雅普诺夫函数的替代方法。我们的方法首先表征多面体李雅普诺夫函数的内在属性，包括其对扰动的“偏心率”和“鲁棒性”。然后，我们推导出一种算法，该算法要么计算证明系统渐近稳定的多面体李亚普诺夫函数，要么得出结论，不存在其偏心率和鲁棒性参数满足用户提供的某些限制的多面体李亚普诺夫函数。值得注意的是，我们的方法对构成所需多面体李亚普诺夫函数的线性部分的数量没有先验限制。该算法在学习步骤和验证步骤之间交替，始终维护一组有限的见证状态。学习步骤求解线性程序，以计算与有限见证状态集兼容的候选李亚普诺夫函数。在验证步骤中，我们的方法验证候选李雅普诺夫函数是否是系统的有效李雅普诺夫函数。如果验证失败，我们将获得新的证人。我们证明了我们的算法所需的最大迭代次数的理论界限。我们通过数值例子证明了该算法的适用性。
This paper presents a counterexample-guided iterative algorithm to compute convex, piecewise linear (polyhedral) Lyapunov functions for continuous-time piecewise linear systems. Polyhedral Lyapunov functions provide an alternative to commonly used polynomial Lyapunov functions. Our approach first characterizes intrinsic properties of a polyhedral Lyapunov function including its “eccentricity” and “robustness” to perturbations. We then derive an algorithm that either computes a polyhedral Lyapunov function proving that the system is asymptotically stable, or concludes that no polyhedral Lyapunov function exists whose eccentricity and robustness parameters satisfy some user-provided limits. Significantly, our approach places no a-priori bound on the number of linear pieces that make up the desired polyhedral Lyapunov function. The algorithm alternates between a learning step and a verification step, always maintaining a finite set of witness states. The learning step solves a linear program to compute a candidate Lyapunov function compatible with a finite set of witness states. In the verification step, our approach verifies whether the candidate Lyapunov function is a valid Lyapunov function for the system. If verification fails, we obtain a new witness. We prove a theoretical bound on the maximum number of iterations needed by our algorithm. We demonstrate the applicability of the algorithm on numerical examples.