Hybrid automata: a formal paradigm for heterogeneous modeling

A hybrid automaton is a model of a system with interacting continuous and discrete dynamics. It has been successfully employed in emerging applications on the border between computer science and control theory. In this paper, hybrid automata are formally introduced. Some results on existence and uniqueness of executions for hybrid automata are obtained. Continuous dependence on initial states are shown for a class of hybrid automata. Zeno hybrid automata, i.e., hybrid automata that exhibit infinitely many discrete transitions in finite time, are also discussed