15-819/18-879L: Logical Analysis of Hybrid Systems (Sp'11)

15-819N: Logical Analysis of Hybrid Systems (Spring 2011)
18-879L: Logical Analysis of Hybrid Systems (Spring 2011)
Instructor: André Platzer
Units: 12
Semester: Spring 2011
Time: Tue, Thu 3:00-4:20 (note change)
Place: NSH 3002 (note change)
Blackboard: blackboard (only for grades)
This course is cross-listed in Computer Science as 15-819N in the Advanced topics in Programming Language area. It is also cross-listed in Electrical & Computer Engineering as 18-879L in the Special Topics in Systems and Controls area at Carnegie Mellon University
Hybrid Systems Analysis & Design logo of course Logical Analysis of Hybrid Systems
DESCRIPTION:

Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behaviour. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical 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, real-time 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 safety-critical 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 cyber-physical 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 safety-critical aspects of embedded and cyber-physical 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:
  1. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

Logical Analysis of Hybrid Systems
METHOD OF EVALUATION:
Grading will be based on a set of homework assignments, including hands-on 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:
  • Safety-critical complex physical systems
  • Discrete dynamical systems
  • Continuous dynamical systems
  • Hybrid dynamical systems
  • Differential equations (select topics like Peano, Picard-Lindelöff)
  • Controllability, safety & stability
  • First-order logic
  • First-order real arithmetic
  • Real-closed 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
  • Differential-algebraic 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