FEL3230 Graduate Course on Hybrid Systems 7.5 credits

Lecture 1: Course outline. Introduction to hybrid systems. Motivating examples. Modelling and hybrid Automata. Zeno behavior.

Lecture 2: Stability of hybrid systems. Multiple Lyapunov Functions.

Lecture 3: Stabilization of hybrid systems. Quantized and event-based control.

Lecture 4: Transitions systems, simulation and bisimulation relations for transition systems, motivational examples (motion planning problem-higher level specifications). Control systems as transition systems. Examples of transition systems as abstractions for control systems.

Lecture 5: Bisimulation relations for linear control systems (generalization of state space equivalence). Approximate simulation and bisimulation relations.

Lecture 6: Approximate symbolic models for control systems. Symbolic models for certain classes of nonlinear systems.

Lecture 7: Verification of hybrid systems: motivation, problems, approaches. Verification via abstraction. Safety and reachability analysis of finite transition systems.Verification of timed automata, region graphs.

Lecture 8: Symbolic reachability analysis of hybrid systems. Reachability computation via over-approximation. Flow pipes.

Lecture 9: Advanced verification questions. Temporal logics, model checking. Automata-based approach to LTL model checking.

Lecture 10: Project presentations.

After the course, the student should be able to:

·know the essential theoretical tools to model hybrid control systems and cope with  related          verification problems

· know the essential problems and results in the area

· apply the theoretical tools to problems in the area

· contribute to the research frontier in the area

J. Lygeros, K.H Johansson, S. Simic, J. Zhang, and S.Sastry, Dynamical properties of hybrid automata, IEEE Transactions on Automatic Control, 48:1, 2-17, 2003.

D. Libertzon, Switching in Systems and Control, Birkhäuser, 2003, part II-III

C. Baier, and J. P. Katoen, Principles of Model Checking, The MIT Press, 2008 (Chapters 2, 7)

P. Tabuada, Verification and Control of Hybrid Systems, Springer, 2009 (Chapters 1, 4, 8)

G. Pappas, Bisimilar linear systems, Automatica, 39(12):2035-2047, 2003

G. Pappas,Bisimilar linear systems, Automatica, 39(12):2035-2047, 2003

A. Van der Schaft, Equivalence of Dynamical Systems by Bisimulation, IEEE Transactions on Automatic Control, 49(12):2160-2172, 2004

A. Girard, and G. Pappas, Approximation Metrics for Discrete and Continuous Systems, IEEE Transactions on Automatic Control, 52(5):782-798, 2007

P. Tabuada, Verification and Control of Hybrid Systems, Springer, 2009 (Chapter 9)

G. Pola, A. Girard, and G. Pappas, Approximately bisimilar symbolic models for nonlinear control systems, Automatica, 44:2508-2516, 2008

M. Zamani, G. Pola, M. Mazo, and P. Tabuada, Symbolic Models for Nonlinear Control Systems Without Stability Assumptions, IEEE Transactions on Automatic Control, 57(7):1804-1809, 2012

P. Tabuada, Verification and Control of Hybrid Systems, Springer, 2009 (Chapter 11)

R. Alur, Formal Verification of Hybrid Systems, 11th International Conference on Embedded Software, 2011.

R. Alur, Timed Automata, Conference on Computer Aided Verification (CAV), pp. 379-395, 1999.

C. Baier, and J. P. Katoen, Principles of Model Checking, The MIT Press, 2008 (Chapter 9).

A. Chutinan, and B. H. Krogh, Computing polyhedral approximations to flow pipes for dynamic systems, IEEE Conference on Decision and Control, pp. 2089 - 2094, 1998.

G. Frehse, C. Le Guernic, A. Donze, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler, SpaceEx: scalable verification of hybrid systems. Conference on Computer Aided Verification (CAV), pp. 379-395, 2011.

C. Baier, and J. P. Katoen, Principles of Model Checking, The MIT Press, 2008 (Chapter 5).

If the course is discontinued, students may request to be examined during the following two academic years.

• EXA1 - Examination, 7.5 credits, grading scale: P, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

Passing Grade based on 3 homework assignments and final project presentations.

Dimos Dimarogonas

• All members of a group are responsible for the group's work.
• In any assessment, every student shall honestly disclose any help received and sources used.
• In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.