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

Differences

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]
asarin
cours:c-2-8-2 [2019/09/10 13:21] (current)
bouyer [Dates]
Line 3: Line 3:
 ===== Lecturers ===== ===== Lecturers =====
  
-  *  [[https://www.irif.fr/~asarin/|Eugene Asarin]] +  *  [[http://www.lsv.fr/~bouyer/|Patricia Bouyer-Decitre]] 
-  *  [[http://www.lsv.fr/~fribourg/?l=fr/|Laurent Fribourg]]+  *  [[https://www.irif.fr/~francoisl/|François Laroussinie]]
 ===== Dates ===== ===== Dates =====
  
-The lectures (5 x 2.5 + 2.5 hours) will take place on Thursday (12h45-15h15), in Bat. Sophie Germain, room 1003.+The lectures (5 x 2.5 + hours) will take place on Thursday (12h45-15h15), in Bat. Sophie Germain, room 1003.
  
-The first lecture is on **September 13rd**.+The first lecture is on **December 5th 2019**.
  
 Basic knowledge in Automata, Logics, Complexity. 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 Cachan.+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.
  
  
 ===== Description ===== ===== Description =====
  
-Computing devices have to meet numerous quantitative +[Français] 
-constraints, like resource constraints (power consumption, memory +Ce cours s’inscrit dans le domaine de la vérification automatique de programmesIci nous mettons l’accent sur les contraintes liées au tempsEn 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éeslorsqu’on s’intéresse aux délais séparant les actionson parle alors de «temps quantitatif» «l’alarme doit retentir moins de 10 millisecondes après le déclenchement d’un problème»
-usage, costs, bandwidth, etc.), timing constraints (response +Dans les deux approches, on cherche à
-time, propagation delays, etc.)and constraints on the +modéliser des programmes avec ces contraintes,  
-environment in which they operate (signal sensors, interactions with a +spécifier (énoncerdes propriétés portant sur le tempset 
-(possibly continuousenvironment, etc.). Another important +vérifier (avec un algorithmequ’un modèle vérifie ou non une propriété.
-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. +
- +
- +
- +
-==== **Part 1: Verification of timed automata (Eugene Asarin)** ==== +
- +
-This part of the lecture will start on Thursday 13th Septemberand will last for five weeks (12:45 - 15:15)+
- +
- +
- +
-**Timed systems**  +
- +
-**o   Timed automatathe model** +
- +
-//§ an example// +
- +
-//§ definition of TA , timed words, timed 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 complementation, lack of determinization, undecidable problems// +
- +
- +
- +
-**o   Verification ** +
- +
-//§  Decidability of reachability. PSPACE-completeness.  (with generic principles of verification etc…// +
- +
-//§  ZonesDBMs 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 automataswitching 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 +
-// +
- +
- +
  
 +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. 
  
 +Nous veillerons à nous concentrer sur les techniques et les problèmes classiques : comment comparer l’expressivité des formalismes étudiés, comment vérifier des systèmes ayant un nombre infini d’états, comment analyser la complexité des problèmes de vérification, etc. 
  
 +[English]
 +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.
  
 ===== Language ===== ===== Language =====
- 
  
 French (or English upon request) French (or English upon request)
Line 142: Line 55:
   * 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  [[http://www.lsv.fr/~fribourg/?l=fr/ | here]] 
-  * Rajeev Alur's slides [[http://www.sti.uniurb.it/events/sfm04rt/slides/sfm-rt-04.pdf|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.  [[http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf|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 [[http://www.it.uu.se/research/group/darts/papers/texts/by-lncs04.ps|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  ===== 
-  * [[https://www.irif.fr/~asarin/sujets/bitsPerSecond.html|Information per time unit]] 
-  * [[https://www.irif.fr/~asarin/sujets/compression.html|Timed compression]] 
-  * [[https://www.irif.fr/~asarin/sujets/quantitative.html|Comparison of quantitative verification approaches]] 
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA