Hybrid systems are those that inherently combine discrete and continuous dynamics. This paper considers the hybrid system model to be an extension of the discrete automata associating a continuous evolution with each discrete state. This model is called the hybrid automaton. In this work, we achieve a mathematical formulation of the steady state and we show a way to obtain the initial conditions region to reach a specific limit cycle for a class of uncoupled and coupled continuous-linear hybrid systems. The continuous-linear term is used in the sense of the system theory and, in this sense, continuous-linear hybrid automata will be defined. Thus, some properties and theorems that govern the hybrid automata dynamic behavior to evaluate a limit cycle existence have been established; this content is explained under a theoretical framework.
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces