This course is about formal (mathematical) methods that allow us to analyze the behavior of hybrid systems whose state can change discretely (similarly to executing an atomic command of a program) as well as continuously (similarly to the evolution of physical quantities like temperature or speed over time). Typical hybrid system examples are physical systems controlled by discrete controllers, but in general all cyber-physical systems can be seen as communicating hybrid systems.
Hybrid automata, which extend discrete automata with continuous behavior, are a popular formalism to formally model hybrid systems. To analyze their behavior, we are interested in solving the reachability problem, i.e. to answer the question whether certain states are reachable from a given initial state set in a given hybrid automaton. This problem is in general undecidable for hybrid automata, meaning that there is no complete algorithm that can answer all questions of this kind. However, we can pose some restrictions on the modeling language that make the problem decidable for models from those restricted fragments.
In this lecture we discuss the basic ideas of different kinds of reachability analysis algorithms for different subclasses of hybrid automata. Thereby we will make use of numerous notions and techniques like bisimulation, abstraction, model transformation and approximation, that are of general importance not only for hybrid system verification but in the whole area of formal methods.