Abstract or Additional Information
Computer control is used increasingly in many safety-critical application domains, including aviation, automotive, railway, and robotics. Systems like these are cyber-physical systems, because they combine cyber capabilities (computers and communication) with physical abilities (sensing and actuation) to solve problems that neither part could solve alone. Because these systems operate in the physical world, stringent safety requirements are usually imposed on cyber-physical system designs. But how can we design computers that are guaranteed to interact correctly with the physical world?
Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions along difference equations and continuous evolutions along differential equations. This talk illustrates how logic and mathematics can work together to answer analytic questions about hybrid systems. It presents the logical foundations of hybrid systems and how they can be used to answer practical analysis questions. The approach combines discrete and continuous mathematics, and logic, and has connections to many other areas of mathematics. It has been used used successfully for verifying nontrivial properties in aircraft, railway, and car control applications.