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:07]
asarin [Documents]
cours:c-2-8-2 [2018/11/22 17:14] (current)
asarin
Line 40: Line 40:
 This part of the lecture will start on Thursday 13th September, and will last for five weeks (12:45 - 15:15). This part of the lecture will start on Thursday 13th September, and will last for five weeks (12:45 - 15:15).
  
-Lecture slides are available {{: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}}+
  
 **Timed systems**  **Timed systems** 
Line 76: Line 76:
 ==== **Part 2: Safe control synthesis for hybrid automata (Laurent Fribourg)** ==== ==== **Part 2: Safe control synthesis for hybrid automata (Laurent Fribourg)** ====
  
-Lecture slides are available [[http://www.lsv.fr/~fribourg/?l=fr/ | here]] 
  
 **o   Hybrid automata: the model** **o   Hybrid automata: the model**
Line 143: Line 142:
   * 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 =====
-===== Documents =====+
   * {{:cours:upload:2-8-2exam2016.pdf|Exam 2016}}   * {{: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]]   *  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]]   * 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.   * 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 David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
 
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