Dynamical properties of hybrid automata

Hybrid automata provide a language for modeling and analyzing digital and analogue computations in real-time systems. Hybrid automata are studied here from a dynamical systems perspective. Necessary and sufficient conditions for existence and uniqueness of solutions are derived and a class of hybrid automata whose solutions depend continuously on the initial state is characterized. The results on existence, uniqueness, and continuity serve as a starting point for stability analysis. Lyapunov's theorem on stability via linearization and LaSalle's invariance principle are generalized to hybrid automata.

I. Introduction

Hybrid systems are dynamical systems that involve the interaction of continuous and discrete dynamics. Systems of this type arise naturally in a number of engineering applications. For example, the hybrid paradigm has been used successfully to address problems in air traffic control [1], automotive control [2], bioengineering [3], process control [4], [5], highway systems [6], and manufacturing [7]. The needs of these applications have fuelled the development of theoretical and computational tools for modeling, simulation, analysis, verification, and controller synthesis for hybrid systems.