2022/04/14 by Guillaume O. Berger, Berger, Guillaume O., Sriram Sankaranarayanan +1 · 1 citation
Computer Science · Engineering · Mathematics · #FOS: Electrical engineering #FOS: Mathematics #Formal Methods in Verification #Low-power high-performance VLSI design #Machine Learning and Algorithms #Optimization and Control (math.OC) #Systems and Control (eess.SY) #cs.SY #eess.SY #electronic engineering #information engineering #math.OC
paper · pdf · doi:10.48550/arxiv.2204.06693
openalex publication_date 2022/04/14 · arxiv created 2022/09/14 · arxiv updated 2022/09/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.