EECS 563: Hybrid Systems: Specification, Verification and Control

Professor Necmiye Ozay

Hybrid systems, dynamical systems where continuous dynamics and discrete events interact, are ubiquitous and can be found in many different contexts. Examples are as diverse as manufacturing processes, biological systems, energy systems, medical devices, robotics systems, automobiles and aircrafts. Advances in computing and communication technologies have enabled engineering such systems with a high degree of complexity. Most of these systems are safety-critical, hence their correctness must be verified before they can be deployed.

This course will provide a working knowledge of several analysis and design techniques to guarantee safety, reliability and performance of such systems. 

Topics include:

  • specifications: Automata theory, discrete transion systems, temporal logics 
  • modeling: Hybrid automata, switched systems, piecewise affine systems 
  • verification of hybrid systems: stability, model checking, direct methods (barrier certificates), abstraction-based methods 
  • correct-by-construction controller synthesis: reactive control synthesis, switching protocols, model-predictive control and more… 

Grading will be based on a few homework assignments, critiquing research papers and in-class discussions, and a (team) term project.

Additional Information