Table of Contents
## Systèmes cyber-physiques et leur vérification / Cyber-physical systems and their verification(2024-2025)- The lecturers for 2024-2025 are Eugene Asarin and Laurent Fribourg
- This course is 24h and corresponds to 3 ECTS.
- Lectures will take place on Thursday, 12:45-15:15, in Bat. Sophie Germain, Room ???.
- The first lecture takes place on September 19, the last one on November 21??
- The course is given in French or English, depending on the audience. Exams can be taken in French or English.
- The prerequisites are basic knowledge in automata theory, logics and complexity theory, as well as some basic calculus and differential equations. It is advised to take or have taken course 1.22 “Introduction to verification”. Related courses include course 2.9.1 “Mathematical foundations of the theory of infinite transition systems” and 2.9.2 “Algorithmic verification of programs”, and 2.20.1 “Game-theoretic techniques in computer science” and 2.20.2 “Mathematical foundations of automata theory”.
- The
**exam**will take place on**Thursday, November 28, 12:45-15:45**, in Bat. Sophie Germain, Room ???.
## ContentsThe lectures covers foundations of cyber-physical systems and their verification. ## Outline of the course (2024-2025)- Timed and Hybrid automata, timed languages and verification of timed systems (Eugene Asarin)
- Verification of continuous and hybrid systems (Laurent Fribourg)
## Part 1: Timed and Hybrid automata, timed languages and verification of timed systems (Eugene Asarin)(tentative plan) ## Lecture 1: introduction to the domain- Cyber-physical systems and the research area
- Hybrid automata as a very general model
- example
- anatomy of a HA and a possible definition
- two semantics of HA: trajectories and transition system
- Timed automata
- definition as a subclass of HA
- example
- imed words, acceptance by TA, timed language of a TA, regular timed language
- variants of TA in the literature
**TD:**modeling by HA and TA
## Lecture 2: timed regular languages- Main good properties
- Alur's theorem 1: L timed regular ⇒ Untime(L) regular
- Closure of timed regular languages by union, intersection, concatenation
- Decision procedures for emptiness, membership, empty intersection
- Main bad properties
- Non-closure by complementation
- Alur's theorem 2: Universality undecidable
- Inclusion and equality undecidable
**TD:**Properties of timed languages
## Lecture 3: proofs- Proving good things
- Finite bisimulations
- Region graph
- Proof of Alur's Thm 1
- Proving undecidability
- Minsky machines
- Undecidability proofs by simulation
- Proof of Alur's Thm 2
**TD:**decidability and undecidability
## Lecture 4: verification of TA- What are the problems?
- Applying the previous theory
- More practical solution: difference-bound matrices etc.
- Tools
**TD**verification of TA
## Lecture 5: current research on TA*How to extend automata for modeling a new kind of systems**How to model systems**What are basic properties of a class of automata**Techniques for proving closure and decidability**Techniques for proving undecidability**Techniques for verification*
## Part 2: Verification of continuous and hybrid systems (Laurent Fribourg)(tentative plan) ## Lecture 1: Continuous systems- State space form
- Existence and uniqueness of solutions
- Continuity with respect to initial condition and simulation
## Lecture 2: Hybrid systems trajectories and flows- Continuous-time flow and discrete-time reset
- Intrinsic distance
- Contractive hybrid systems
- Periodic orbits
## Lecture 3: Reachability of hybrid systems- Reachability
- Reachability algorithm
- Backward reachability algorithm
- Invariance algorithm
- Controller design based on backward reachability
## Lecture 4: Synchronization of hybrid systems- Synchronization conditions based on contractions
- Conditions based on graph structure
- Application to biomolecular reactions
## Lecture 5: Stability and convergence of hybrid systems- Lyapunov stability of ordinary differential equations
- Lyapunov stability of hybrid systems
- Asymptotic stability
- Stability of periodic solutions
## 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. |