Algebraic analysis on asymptotic stability of switched hybrid systems

In this paper we propose a mechanisable approach for discovering multiple Lyapunov functions for switched hybrid systems. We start with the classical definition on asymptotic stability, which can be assured by the existence of multiple Lyapunov functions. Then, we derive an algebraizable sufficient condition on multiple Lyapunov functions in quadratic form for asymptotic stability analysis. Since different modes are considered, in addition to real root classification, we further apply a projection operator step by step to under-approximate this sufficient condition and obtain a set of semi-algebraic sets which only involve the coefficients of the multiple Lyapunov function. Moreover, for each step, we use the information on modes to optimize our intermediate computation results. Finally, we compute a sample point in the resulting semi-algebraic sets for coefficients. We tested our approach on five examples using prototypical implementation. The computation and comparison results demonstrate the applicability and efficiency of our approach.