Skip to main content

Before choosing course

Hybrid systems are dynamical systems that exhibit both continuous and discrete behavior and as such, they allow to model complex dynamic phenomena in real-world systems, such as cyber-physical systems, with application examples varying from automotive industry, to consumer electronics, power systems, smart buildings, and transportation systems. For all of these examples, properties such as stability or correctness with respect to design specifications are crucial. However, the rich expressiveness of hybrid systems requires special techniques to analyze and derive these properties.  This course will focus on selected related topics in hybrid systems, with a special focus on their stability, stabilization, abstraction and formal verification.

Course offering missing for current semester as well as for previous and coming semesters
* Retrieved from Course syllabus FEL3230 (Spring 2019–)

Content and learning outcomes

Course contents

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.

Intended learning outcomes

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

Course Disposition

Lectures, relevant list of papers/book chapters.

Literature and preparations

Specific prerequisites

No information inserted

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

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).

Examination and completion

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

Grading scale

P, F

Examination

  • EXA1 - Examination, 7,5 hp, betygsskala: 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.

Other requirements for final grade

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

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

Profile picture Dimos Dimarogonas

Ethical approach

  • 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.

Further information

Course web

Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.

Course web FEL3230

Offered by

EECS/Decision and Control Systems

Main field of study

No information inserted

Education cycle

Third cycle

Add-on studies

No information inserted

Postgraduate course

Postgraduate courses at EECS/Decision and Control Systems