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

The lectures covers foundations of cyber-physical systems and their verification.

1. Timed and Hybrid automata, timed languages, and verification of timed systems (Eugene Asarin)
2. Verification of continuous and hybrid systems (Laurent Fribourg)

(tentative plan)

• Cyber-physical systems and the research area

• Hybrid automata as a very general model
  • example
  • anatomy of an HA and a possible definition
  • two semantics of HA: trajectories and transition system
• Timed automata
  • definition as a subclass of HA
  • example
  • timed words, acceptance by TA, timed language of a TA, regular timed language
  • variants of TA in the literature
    • Proposition: TA with epsilon are more expressive than those without (proof)
• timed regular languages
  • Announcing main properties for Lecture 2

• TD: modeling by HA and TA exercises

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

• Proving good things
  • Finite bisimulations
  • Region graph
  • Proof of Alur's Thm 1
• Proving undecidability
  • Minsky machines
  • Undecidability proofs by simulation
• TD: undecidability exercices

• (not finished in Lecture 3) Proving undecidability
  • Proof sketch of Alur's Thm 2
• Verification of TA
  • What are the problems?
  • Applying the previous theory
  • More practical solution: difference-bound matrices etc.
  • Tools
• Exercise verification of TA

• Verification of TA explained informally
  • How zones work, why widening is needed, why DBM are a good data structure
• Current research: information content of timed words slides. This survey is not in the programme, you do not need to revise it before your exam.

• How to extend automata for modeling a new kind of systems
• How to model systems
• What are the basic properties of a class of automata
• Techniques for proving closure and decidability
• Techniques for proving undecidability
• Techniques for verification

(tentative plan)

• State space form

• Existence and uniqueness of solutions

• Continuity with respect to initial condition and simulation

• Continuous-time flow and discrete-time reset

• Intrinsic distance

• Contractive hybrid systems

• Periodic orbits

• Reachability

• Reachability algorithm

• Backward reachability algorithm

• Invariance algorithm

• Controller design based on backward reachability

• Synchronization conditions based on contractions
• Conditions based on graph structure
• Application to biomolecular reactions

• Lyapunov stability of ordinary differential equations
• Lyapunov stability of hybrid systems
• Asymptotic stability
• Stability of periodic solutions

* Eugene Asarin's tutorial slides pdf long pdf annotated and shortened for MPRI

* Eugene's Covid-19 lectures for MPRI 2-8-2 (in French, handwritten whiteboards) cours 2, cours 3, cours 4, cours 5

* Laurent Fribourg's Lecture 1 slides for MPRI 2-8-2 (24/10/2024) cours 1

* Laurent Fribourg's Lecture 2 reference paper for MPRI 2-8-2 (31/10/2024) cours 2

* Laurent Fribourg's Lecture 3 reference paper for MPRI 2-8-2 (07/11/2024) cours 3

* Laurent Fribourg's Lecture 4 reference paper for MPRI 2-8-2 (14/11/2024) cours 4cours 4bis

* Laurent Fribourg's Lecture 5 reference paper for MPRI 2-8-2 (21/11/2024) cours 5

* Laurent Fribourg's Exam Problem reference paper (28/11/2024). Questions and answers come from exam

* 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

* Bengtsson, J., Yi, W. Timed Automata: Semantics, Algorithms and Tools. In: Lectures on Concurrency and Petri Nets. Springer,2004 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.