Table of Contents
Systèmes cyber-physiques et leur vérification / Cyber-physical systems and their verification(2024-2025)
ContentsThe lectures covers foundations of cyber-physical systems and their verification. Outline of the course (2024-2025)
Part 1: Timed and Hybrid automata, timed languages and verification of timed systems (Eugene Asarin)(tentative plan) Lecture 1: introduction to the domain
Lecture 2: timed regular languages
Lecture 3: proofs
Lecture 4: verification of TA
Lecture 5: current research on TA
Part 2: Verification of continuous and hybrid systems (Laurent Fribourg)(tentative plan) Lecture 1: Continuous systems
Lecture 2: Hybrid systems trajectories and flows
Lecture 3: Reachability of hybrid systems
Lecture 4: Synchronization of hybrid systems
Lecture 5: Stability and convergence of hybrid systems
Lecture Notes and other documents* Eugene Asarin's tutorial slides pdf * P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, J. Ouaknine, and J. Worrell. Model Checking Real-Time Systems. In Handbook of Model Checking, pages 1001–1046. Springer, 2018. pdf * John Lygeros: Lecture Notes on Hybrid Systems, ENSIETA 2-6/2/2004 * João P. Hespanha: Hybrid Control and Switched Systems, Lecture 6: Reachability, UCSB * Zahra Aminzare and Eduardo D. Sontag: Synchronization of diffusively-connected nonlinear systems - results based on contractions with respect to general norms, IEEE Transactions on Network Science and Engineering, 2014. * Samuel A. Burden, Thomas Libby, and Samuel D. Coogan: On infinitesimal contraction analysis for hybrid systems, arXiv:1811.03956v2, 2020. |