An algorithmic approach to global asymptotic stability verification of hybrid systems

Abstract

In this paper, we present an algorithmic approach to global asymptotic stability (GAS) verification of hybrid systems. Our broad approach consists of reducing the GAS verification to the verification of a region stability (RS) analysis problem and an asymptotic stability (AS) analysis problem. We use a recently developed quantitative predicate abstraction technique for AS analysis and extract from it a stability zone with respect to which we perform RS analysis. We present a new algorithm for RS analysis based on abstractions. While we develop the theory for polyhedral hybrid systems, our broad approach of decomposing GAS analysis to RS and AS analysis can be applied to more general class of systems including linear hybrid systems. As a proof of concept, we apply the GAS verification algorithm to a linear hybrid system model of a cruise control for an automatic gearbox, and provide a semi-automated proof of GAS.