

 DESCRIPTION:

Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behaviour. Many applications are safetycritical, including car, railway, and air traffic control, robotics, physicalchemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerized controllers for physical systems which are guaranteed to meet their design goals.

This course covers mathematical models for complex physical systems, including discrete dynamical systems, continuous dynamical systems, realtime dynamical systems, and hybrid dynamical systems (or hybrid systems for short). Our primary focus will be on the mathematical foundations and analytic techniques for these complex systems. We will study the questions that are important for designing system models and for understanding their behaviour. We will emphasize concise representations of analytic problems in logic and their algorithmic solutions in automated theorem provers and model checkers.
The class will provide you with modern techniques for analyzing the correct functioning of important safetycritical systems ranging from embedded systems in cars and biomedical devices, over chemical/physical process control and chip design, to full car, aircraft, and train control. The opportunity to gain practical experience in analysis of cyberphysical systems will be given as part of the course. The class should be appropriate for graduate students and for advanced undergraduates with an interest in mathematical, logical, or formal analysis methods.
 OBJECTIVES:
 You will develop an understanding for important safetycritical aspects of embedded and cyberphysical systems. You will be able to understand and develop discrete/continuous/hybrid dynamical system models. You will learn how you can analyze if a hybrid system works as intended and if it actually meets its design goals. You will learn how to use formal methods and calculi to analyze system correctness and you will understand how automatic verification techniques work.
 PREREQUISITES:
 Basic knowledge in logic (e.g., propositional logic) and continuous mathematics (e.g., differential equations) is of advantage but not strictly required.
 TEXTBOOK:

 METHOD OF EVALUATION:

Grading will be based on a set of homework assignments, including handson analysis experience, midterm exam, and a final project (30% Homework, 15% Midterm, 55% Project).
The project is worth 260 points, with 20 points for the whitepaper, 50 points for the proposal, and 190 points for the project report.  MORE INFORMATION:
 See case studies for some illustrations and examples of hybrid system applications.
 TOPICS TO BE COVERED:

 Safetycritical complex physical systems
 Discrete dynamical systems
 Continuous dynamical systems
 Hybrid dynamical systems
 Differential equations (select topics like Peano, PicardLindelöff)
 Controllability, safety & stability
 Firstorder logic
 Firstorder real arithmetic
 Realclosed fields and semialgebraic geometry
 Numerical analysis and integration
 Symbolic reachability analysis
 Computable analysis
 Hybrid programs and hybrid automata
 Compositionality
 Dynamic logic & dynamical systems
 Differential dynamic logic
 Disturbances in hybrid control
 Deduction modulo
 Differential variance and invariance
 Differential closure properties
 Differentialalgebraic equations and differential algebra
 Differential transformations and differential reductions
 Railway control applications
 Air traffic control applications
 Distributed car control applications
 Time permitting: Nullstellensätze and Positivstellensätze
 Time permitting: Gröbner bases and algebraic geometry
 Time permitting: Proof theory of hybrid systems
 Time permitting: Fixedpoint model checking engines