This talk will introduce a novel abstraction technique and a model checking algorithm for analysing stability of a particular class of hybrid systems. Hybrid systems are physical systems evolving in time, which exhibits a mixed discrete and continuous behaviour. Stability is a control design property establishing that small perturbations on the input just induce small changes on the output.

The proposed technique consists of defining a simple system, an abstraction, from an initial hybrid system, and applying a model checking algorithm to determine stability. The proposed abstraction procedure is a modified predicate abstraction, which gives an abstract weighted graph. Model checking consists of analysing the finite weighted graph for the absence of certain kinds of cycles which can be solved by dynamic programming. It is shown that the abstraction is sound in that a positive result on the analysis of the graph implies that the original system is stable.

The feasibility of the approach has been demonstrated by a prototype implementation.