Region Stability for Hybrid Systems

discrete and continuous behaviors. The most natural examples of
hybrid systems are obtained when a digital system is embedded in an
analog environment. Several such systems operate in safety-critical
domains, for example, inside automobiles, aircrafts, and chemical
plants.

Stability is one of the central properties in system theory and
engineering. We call a hybrid system stable with respect to a given
region (= set of states) if every run of the system inevitably ends
up in the region. Region stability allows one to formalize
correctness properties such as "a heating system will bring the
temperature of a plant to a range between 68 and 82 degrees and keep
it there".

We have developed an algorithm for verifying region stability of
hybrid systems. The aim of this talk is to establish the intuition
behind our algorithm and its implementation.