Model Checking on Hybrid Automata

Many systems, both natural and artificial, exhibit a mixed discrete-continuous behavior that cannot be fully captured by either continuous nor discrete models: they evolve in accordance to continuous laws, but these laws are controlled by a finite set of modes. Hybrid automata were proposed to represent such kind of behaviors and they have been used to model numerous natural phenomena in the last decades. Unfortunately, the Model Checking problem over them was proved undecidable and, because of that, many techniques were suggested so far to both approximate the original models and reduce the analysis complexity. This paper surveys some of such techniques and reports some open questions.