Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)


This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-8-2 [2018/11/22 17:14]
cours:c-2-8-2 [2020/02/21 13:56] (current)
bouyer [Description]
Line 3: Line 3:
 ===== Lecturers ===== ===== Lecturers =====
-  *  [[|Eugene Asarin]] +  *  [[|Patricia Bouyer-Decitre]] 
-  *  [[|Laurent Fribourg]]+  *  [[|François Laroussinie]]
 ===== Dates ===== ===== Dates =====
-The lectures (2.5 + 5 x 2.5 hours) will take place on Thursday (12h45-15h15), in Bat. Sophie Germain, room 1003.+The lectures (hours) will take place on Thursday (12h45-15h45), in Bat. Sophie Germain, room 1013.
-The first lecture is on **September 13rd**.+:!: **There will be no lecture on December 5th 2019!!**
-Basic knowledge in Automata, Logics, Complexity.+The first lecture is on **December 12th 2019**.
-While not mandatory, it is useful to know the basics of verification. See for instance the level 1 course 1-22 Basics of verification which can also be taken during M2. Course 1-22 is organized at ENS Cachan.+:!: **There will be no lecture on January 9th 2020!!**
 +There will be no lecture on February 13th 2020. Last lecture will take place on February 20th 2020.
-===== Description =====+**The exam will take place on February 27th 2020!**
-Computing devices have to meet numerous quantitative 
-constraints, like resource constraints (power consumption, memory 
-usage, costs, bandwidth, etc.), timing constraints (response 
-time, propagation delays, etc.), and constraints on the 
-environment in which they operate (signal sensors, interactions with a 
-(possibly continuous) environment, etc.). Another important 
-characteristic of these systems is that they have to be powerful, 
-performant, and reliable. Thus, their conception and verification pose 
-a great challenge, and require the development of complex models and 
-analysis techniques. In this context, verification of timed systems (that is, 
-systems with constraints over delays) is a real success, 
-with lots of theoretical and practical developments. 
-In this lecture, we will present advanced technics in standard model-checking 
-of finite systems, and extend the approach progressively to timed and hybrid systems. 
 +Basic knowledge in Automata, Logics, Complexity.
 +While not mandatory, it is useful to know the basics of verification. See for instance the level 1 course 1-22 Basics of verification which can also be taken during M2. Course 1-22 is organized at ENS Paris-Saclay.
-==== **Part 1: Verification of timed automata (Eugene Asarin)** ==== 
-This part of the lecture will start on Thursday 13th September, and will last for five weeks (12:45 - 15:15).+===== Description =====
 +Ce cours s’inscrit dans le domaine de la vérification automatique de programmes. Ici nous mettons l’accent sur les contraintes liées au temps. En général, on parle de contraintes temporelles pour désigner le «temps qualitatif» où on s’intéresse à l’ordre des actions d’un système (ou d’un programme) : «l’alarme doit retentir après le déclenchement d’un problème». Et on parle de contraintes temps-réel (ou temporisées) lorsqu’on s’intéresse aux délais séparant les actions, on parle alors de «temps quantitatif» : «l’alarme doit retentir moins de 10 millisecondes après le déclenchement d’un problème».
 +Dans les deux approches, on cherche à:
 +- modéliser des programmes avec ces contraintes, 
 +- spécifier (énoncer) des propriétés portant sur le temps, et
 +- vérifier (avec un algorithme) qu’un modèle vérifie ou non une propriété.
 +Dans ce cours, nous aborderons ces différents aspects, en commençant par une présentation des logiques temporelles classiques (LTL, CTL, CTL*) pour énoncer des propriétés temporelles. Nous nous intéresserons notamment aux questions d’expressivité et aux algorithmes de décision en lien avec la vérification.
 +Ensuite nous nous intéresserons aux aspects temps-réel en étudiant le modèle des automates temporisés (et de certains systèmes hybrides), puis à des extensions des logiques temporelles pour exprimer des propriétés temps-réel et enfin à des algorithmes d’analyse de ces modèles temporisés. 
-**Timed systems**  +Nous veillerons à nous concentrer sur les techniques et les problèmes classiques comment comparer l’expressivité des formalismes étudiéscomment vérifier des systèmes ayant un nombre infini d’étatscomment analyser la complexité des problèmes de vérification, etc. 
- +
-**o   Timed automatathe model** +
- +
-//§ an example// +
- +
-//§ definition of TA timed wordstimed languages// +
- +
-//§ TA as a model of timed behaviors +
-// +
- +
-**o   Theory of timed regular languages** +
- +
-//§  Region graph construction and its consequences +
-// +
- +
-//§  Closure properties and decidable properties of timed regular languages +
-// +
- +
-//§  Lack of complementationlack of determinization, undecidable problems// +
- +
- +
- +
-**o   Verification ** +
- +
-//§  Decidability of reachability. PSPACE-completeness.  (with generic principles of verification etc…// +
- +
-//§  Zones, DBMs and associated algorithms.// +
- +
-//§  Practical  (zone-based) reachability algorithm.// +
- +
- +
-==== **Part 2: Safe control synthesis for hybrid automata (Laurent Fribourg)** ==== +
- +
- +
-**o   Hybrid automata: the model** +
- +
-//§  an example// +
- +
-//§  definition of HA// +
- +
-//§  HA as a model of cyber-physical systems//  +
- +
-//§  classes of HA: finite automata, linear hybrid automata, timed automata, switching systems +
-// +
- +
-// +
-§  input variables and disturbances +
-// +
- +
-**o   Verification and control synthesis +
-** +
- +
-//§  Reachability, safety,  control synthesis, stability, attractors, basins of attraction, robustness// +
- +
-//§  Generic algorithms (forward/backward, state space partition, reach-set computation)// +
- +
-//§  Maximal invariant sets and least permissive control[EA1]//  +
- +
-//§  Undecidability of reachability// +
- +
-//§  Approximate algorithms// +
- +
-**o   Efficient computations** +
- +
-//§  Set-theoretic concepts: Minkowski sum, convex sets, support function// +
- +
-//§  Data structures (polytopes, rectangles, zonotopes, ellipsoids) +
-// +
-//§  Finite-time reachability analysis, NP-hardness// +
- +
-//§  Basic operations (intersection, inclusion, projection, linear mapping), efficient implementations +
-// +
- +
-//§  Specialization for switching systems +
-// +
 +This lecture is part of the domain of automatic verification of programs. We will focus on timing constraints. In general, we speak of temporal constraints, when we only take care of the order of actions: «the alarm should ring after a problem has occurred». We speak of real-time or timed constraints when we are interested in quantitative constraints on delays between actions: «the alarm should ring after a problem has occurred, within 10ms».
 +In these two views, we are interested in:
 +- modelling programs with such constraints,
 +- specifying properties on time, and
 +- verifying (automatically using an algorithm) that a model satisfies a property.
 +In this lecture, we will study these different aspects. We will start with classical temporal logics (LTL, CTL, CTL*) that are used to express temporal properties. We will in particular be interested in expressiveness questions, and in verification algorithms. Then, we will study real-time aspects and will in particular study the model of timed automata and of some hybrid automata, timed logics and verification algorithms for those models.
 +We will focus on standard models and technics.
 +  * [[|Lecture Notes]] 23/01/2020 [[|Slides]]
 +  * [[|Lecture Notes]] 30/01/2020
 +  * [[|Lecture Notes]] 06/02/2020
 +  * [[|Lecture Notes]] 20/02/2020
 ===== Language ===== ===== Language =====
 French (or English upon request) French (or English upon request)
Line 142: Line 73:
   * 2-20-1 Game theory techniques in computer science   * 2-20-1 Game theory techniques in computer science
   * 2-20-2 Mathematical foundations of automata theory   * 2-20-2 Mathematical foundations of automata theory
-===== Very useful links ===== 
-  * {{:cours:upload:2-8-2exam2016.pdf|Exam 2016}} 
-  * Eugene Asarin's lecture slides {{:cours:upload:2-8-2-tutoea.pdf|here}} and the last lecture {{:cours:upload:mpri_2_8_2_lecture_eugene_asarin.pdf|there}}. Exercises: {{:cours:upload:tdmod.pdf|modeling}}, {{:cours:upload:tdundecidability.pdf|undecidability}} 
-  * Laurent Fribourg's lecture slides  [[ | here]] 
-  * Rajeev Alur's slides [[|there]] 
-  *  Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, Joël Ouaknine et James Worrell.  Model Checking Real-Time Systems.  In  Handbook of Model Checking. Springer, 2017.  [[|Temporary Link]] 
-  * Timed Automata: Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. In Lecture Notes on Concurrency and Petri Nets.  LNCS 3098, Springer, 2004 [[|Temporary Link]] 
-===== Documents ===== 
-  * Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. 
-  * Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. 
-  * Rajeev Alur and P. Madhusudan. Decision problems for timed automata: A survey. In Proc. 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time (SFM-04:RT), volume 3185 of Lecture Notes in Computer Science, pages 122–133. Springer, 2004. 
-  * Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaya. What's Decidable about Hybrid Automata? Journal of Computer and System Sciences, 57(1):94-124, 1998. 
-===== M2 internships  ===== 
-  * [[|Information per time unit]] 
-  * [[|Timed compression]] 
-  * [[|Comparison of quantitative verification approaches]] 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA