Abstraction Based Model-Checking of Stability of Hybrid Systems

Abstract

In this paper, we present a novel abstraction technique and a model-checking algorithm for verifying Lyapunov and asymptotic stability of a class of hybrid systems called piecewise constant derivatives. We propose a new abstract data structure, namely, finite weighted graphs, and a modification of the predicate abstraction based on the faces in the system description. The weights on the edges trace the distance of the executions from the origin, and are computed by using linear programming. Model-checking consists of analyzing the finite weighted graph for the absence of certain kinds of cycles which can be solved by dynamic programming. We show that the abstraction is sound in that a positive result on the analysis of the graph implies that the original system is stable. Finally, we present our experiments with a prototype implementation of the abstraction and verification procedures which demonstrate the feasibility of the approach.