Finite abstractions for hybrid systems with stable continuous dynamics

This paper outlines an abstraction process in which a particular class of hybrid automata with continuous dynamics that have parameterized positive limit sets, are being abstracted into finite transition systems. The limit sets with their corresponding attraction regions define pre- and post-conditions for the continuous dynamics, and determine the transitions in the discrete abstraction. An observable (weak) bisimulation equivalence is established between the two models. The abstraction process described can find application in verification, as well as in planning and symbolic control.