Learning fixed-complexity polyhedral Lyapunov functions from counterexamples

Guillaume O. Berger, Sriram Sankaranarayanan

In this paper, we present an algorithm for synthesizing polyhedral Lyapunov functions for hybrid systems with multiple modes, each with linear dynamics and state-based switching between these modes. The problem of proving global asymptotic stability (GAS) for such systems is quite challenging. In this paper, we present an algorithm to synthesize a fixed-complexity polyhedral Lyapunov function to prove that such a system is GAS. Such functions are defined as the piecewise maximum over a fixed number of linear functions. Previous work on this problem reduces to a system of \emph{bilinear} constraints that are well-known to be computationally hard to solve precisely. Therefore, heuristic approaches such as alternating descent have been employed. In this paper, we first prove that deciding if there exists a polyhedral Lyapunov function for a given piecewise linear system is a NP-hard problem. We then present a counterexample-guided algorithm for solving this problem. Our approach alternates between choosing candidate Lyapunov functions based on a finite set of counterexamples, and verifying if these candidates satisfy the Lyapunov conditions. If the verification of a given candidate fails, we find a new counterexample that is added back to our set. We prove that if this 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 small numerical examples.

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment