Discrete Asymptotic Abstractions of Hybrid Systems

In this paper we introduce the notion of finite time mode abstraction to relate a hybrid automaton to a timed automaton that preserves the stability and reachability properties of the former. The abstraction procedure discards the continuous dynamics of each mode in the hybrid automaton completely, keeping only the information about the maximum time in which the continuous state makes a discrete jump. This information is used to construct a timed automaton, based on the original hybrid automaton, and to prove that the stability and reachability properties of the original system are retained in the abstract timed automaton. In the process of abstracting a hybrid to a timed automaton we introduce a new notion of hybrid distance metric, which provides information about both the number of discrete transitions that a system would have to make to go from one hybrid state to another, and the distance between the continuous parts of such hybrid states