论文标题
从反例中学习固定复杂性多面体Lyapunov功能
Learning fixed-complexity polyhedral Lyapunov functions from counterexamples
论文作者
论文摘要
我们研究了杂交线性系统合成多面体Lyapunov函数的问题。这些功能定义为具有有限数量的凸面线性函数。我们首先证明，确定是否存在给定混合线性系统的$ M $ proce polyhedral lyapunov功能是NP-HARD。然后，我们提出了一种针对解决此问题的反例引导算法。该算法在基于有限的反例集合和验证候选人是否满足Lyapunov条件的情况下选择候选的多面体函数之间交替。如果验证失败，我们会找到一个添加到我们集合中的新反例。我们证明，如果算法终止，它会发现有效的lyapunov函数或得出结论，不存在这样的lyapunov函数。但是，我们的初始算法可能是非终止的。我们修改算法以根据非滑动优化的所谓的切割平面参数提供终止版本。我们在数值示例上演示了算法。
We study the problem of synthesizing polyhedral Lyapunov functions for hybrid linear systems. Such functions are defined as convex piecewise linear functions, with a finite number of pieces. We first prove that deciding whether there exists an $m$-piece polyhedral Lyapunov function for a given hybrid linear system is NP-hard. We then present a counterexample-guided algorithm for solving this problem. The algorithm alternates between choosing a candidate polyhedral function based on a finite set of counterexamples and verifying whether the candidate satisfies the Lyapunov conditions. If the verification fails, we find a new counterexample that is added to our set. We prove that if the algorithm terminates, it discovers a valid Lyapunov function or concludes that no such Lyapunov function exists. However, our initial algorithm can be non-terminating. We modify our algorithm to provide a terminating version based on the so-called cutting-plane argument from nonsmooth optimization. We demonstrate our algorithm on numerical examples.
