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

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

• 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

• 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

• What are the problems?
• Applying the previous theory
• More practical solution: difference-bound matrices etc.
• Tools
• TD verification of 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

(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

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