Verification of hybrid systems

Hybrid systems are models which combine discrete and continuous behavior. They occur frequently in safety-critical applications in various domains such as health care, transportation, and robotics, as a result of interactions between a digital controller and a physical environment. They also have relevance in other areas such as systems biology, in which the discrete dynamics arises as an abstraction of fast continuous processes. One of the prominent models is that of hybrid automata, where differential equations are associated with each node, and jump constraints such as guards and resets are associated with each edge. In this chapter, we focus on the problem of model checking of hybrid automata against reachability and invariance properties, enabling the verification of general temporal logic specifications.We review the main decidability results for hybrid automata, and since model checking is in general undecidable, we present three complementary analysis approaches based on symbolic representations, abstraction, and logic. In particular, we illustrate polyhedron-based reachability analysis, finite quotients, abstraction refinement techniques, and logic-based verification. We survey important tools and application domains of successful hybrid system verification in this vibrant area of research.