Logics for hybrid systems

Hybrid systems are heterogenous dynamical systems characterized by interact ing continuous and discrete dynamics. Such mathematical models have proved fruitful in a great diversity of engineering applications, including air-tr affic control, automated manufacturing, and chemical process control. The h igh-profile and safety-critical nature of the application areas has fostere d a large and growing body of work on formal methods for hybrid systems: ma thematical logics, computational models and methods, and computer-aided rea soning tools supporting the formal specification and verification of perfor mance requirements for hybrid systems, and the design and synthesis of cont rol programs for hybrid systems that are provably correct with respect to f or-mat specifications. This paper offers a synthetic overview of and origin al contributions to, the use of logics and formal methods in the analysis o f hybrid systems.