Optimization-based verification and stability characterization of piecewise affine and hybrid systems

In this paper, we formulate the problem of characterizing the stability of a piecewise affine (PWA) system as a verification problem. The basic idea is to take the whole IRn as the set of initial conditions, and check that all the trajectories go to the origin. More precisely, we test for semi-global stability by restricting the set of initial conditions to an (arbitrarily large) bounded set chi(0), and label as "asymptotically stable in T steps" the trajectories that enter an invariant set around the origin within a finite time T, or as "unstable in T steps" the trajectories which enter a set X-inst of (very large) states. Subsets of chi(0) leading to none of the two previous cases are labeled as "non-classifiable in T steps". The domain of asymptotical stability in T steps is a subset of the domain of attraction of an equilibrium point, and has the practical meaning of collecting the initial conditions from which the settling time to a specified set around the origin is smaller than T. In addition, it can be computed algorithmically in finite time. Such an algorithm requires the computation of reach sets, in a similar fashion as what has been proposed for verification of hybrid systems. In this paper we present a substantial extension of the verification algorithm presented in [6] for stability characterization of PWA systems, based on linear and mixed-integer linear programming. As a result, given a set of initial conditions we are able to determine its partition into subsets of trajectories which are asymptotically stable, or unstable, or non-classifiable in T steps.