Learning fixed-complexity polyhedral Lyapunov functions from counterexamples

TL;DR

This paper introduces a counterexample-guided algorithm for synthesizing fixed-complexity polyhedral Lyapunov functions for hybrid linear systems, addressing NP-hardness and ensuring termination through cutting-plane methods.

Contribution

The paper presents a novel counterexample-guided approach with a termination guarantee for synthesizing polyhedral Lyapunov functions, advancing control theory methods.

Findings

Algorithm successfully synthesizes Lyapunov functions in numerical examples.

Proves NP-hardness of the synthesis problem.

Provides a terminating version using cutting-plane techniques.

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 $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.