FEL3230 Doktorandkurs i hybrida system 7,5 hp

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-approximaitos. Flow pipes.

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

Lecture 10: Project presentations.

Efter kursen ska studenten kunna:

Känna till de grundläggande teoretiska verktygen för att modellera hybrida kontrollsystem och hantera relaterade verifieringsproblem
Känna till de viktigaste problemen och resultaten inom området
Tillämpa de teoretiska verktygen till problem inom området
Bidra till forskningsfronten inom området

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

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

• EXA1 - Examination, 7,5 hp, betygsskala: P, F

Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Godkänd på 3 hemuppgifter och projektpresentation.

Dimos Dimarogonas

• Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
• Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
• Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.