Theory of Reals for Verification and Synthesis of Hybrid Dynamical Systems

Abstract

Real numbers are used to model all physical processes around us. The temperature of a room, the speed of a car, the angle of attack of an airplane, protein concentration in a cell, blood glucose concentration in a human, and the amount of chemical in a tank are a few of the countless quantities that arise in science and engineering and that are modeled using real-valued variables. Many of these physical quantities are now being controlled by embedded software running on some hardware platform. The resulting systems could possibly be communicating and coordinating with other such systems and reacting actively to changes in their environment. The net result is a complex cyber-physical system. Several such systems operate in safety-critical domains, such as transportation and health care, where failures can potentially cause a lot of financial as well as human life loss. Formal verification and synthesis are both indispensable components of any methodology for designing and efficiently developing safe cyber-physical systems.