Polyhedral Control Lyapunov Functions for Switched Affine Systems

We present a counterexample-guided approach for synthesizing convex piecewise affine control Lyapunov functions, obtained as the maximum over a finite number of affine functions, for stabilizing switched linear systems. Our approach considers systems whose dynamics are defined by a set of affine ODEs over different regions of the state-space. The goal is to synthesize a control feedback function that uses state-based switching by assigning a dynamical mode to each state from the set of available dynamics. This is achieved by synthesizing a piecewise affine control Lyapunov function that guarantees that for each state variable, the appropriate choice of a control input can cause an instantaneous decrease in the value of the Lyapunov function. Since piecewise affine functions are not smooth, we use a non-smooth analytic characterization of piecewise affine Lyapunov functions. The key contribution of our approach is a counterexample driven algorithm that alternates between verification that a given convex PWA function is a control Lyapunov function or generating a counterexample point where the Lyapunov conditions fail, and synthesis from a finite set of counterexamples generated in the past. We demonstrate that the two steps can be performed using mixed integer linear programming problems (MILP) although no termination guarantees are possible. We show that the branch and cut approach used inside a MILP solver can be adapted to yield a termination guarantee. Although the resulting approach is computationally expensive, it has the advantage of not requiring a "demonstrator" or a pre-existing controller. We provide an empirical evaluation that explores the results of this approach over a set of numerical examples.