Learning fixed-complexity polyhedral Lyapunov functions from counterexamples
Abstract
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 -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.
Cite
@article{arxiv.2204.06693,
title = {Learning fixed-complexity polyhedral Lyapunov functions from counterexamples},
author = {Guillaume O. Berger and Sriram Sankaranarayanan},
journal= {arXiv preprint arXiv:2204.06693},
year = {2022}
}