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-1 [2019/10/06 12:11]
gastin [Lecture Notes]
cours:c-2-8-1 [2020/02/11 11:07] (current)
bollig [Outline of the course]
Line 13: Line 13:
 The lectures will take place on Wednesday, **10:15 - 11:45**, in Bat. Sophie Germain, room 1013. The lectures will take place on Wednesday, **10:15 - 11:45**, in Bat. Sophie Germain, room 1013.
  
-**The first lecture is on Wednesday, 18th September 2019.** +**The second exam takes place on Wednesday, 26th February 2020, 10:15 - 11:45, in Bat. Sophie Germain, room 1013.**
 ==== Description ==== ==== Description ====
  
Line 24: Line 23:
  
  
-| **1st Lecture** || 18/09/2019 || Introduction and motivating examples. ||  +| **Lecture** || **Date** || **Contents** ||  
-| **2nd Lecture** || 25/09/2019 || automata models of concurrent processes with data structures; operational semantics; graph semantics || +| **1st** || 18/09/2019 || Introduction and motivating examples. ||  
-| **3rd Lecture** || 02/10/2019 || MSO logic; expressive power of MSO logic || +| **2nd** || 25/09/2019 || Automata models of concurrent processes with data structures; operational semantics; graph semantics || 
- ||  || underapproximate verification; special tree-width, decomposition game || +| **3rd** || 02/10/2019 || MSO logic; expressive power of MSO logic || 
- ||  || special tree-width and tree interpretation; decision procedures via tree automata || +**4th** || 09/10/2019 || Expressive power of MSO logic; underapproximate verification || 
- ||  || propositional dynamic logic (PDL)|| +| **5th** || 16/10/2019 || Underapproximate verification; co-graphs and tree interpretation; special tree-width || 
- ||  || model-checking of existentially bounded behaviors; synthesis from PDL formulas into CPDS || +| **6th** || 23/10/2019 || Special tree-width, decomposition game, examples || 
- ||  || asynchronous automata || +**7th** || 06/11/2019 || Special tree-width and tree interpretation; decision procedures via MSO; decision procedures via tree automata || 
- ||  || revision and exercises ||+**8th** || 13/11/2019 || Exercises || 
 +|  || 20/11/2019 || First exam || 
 +| **9th** || 04/12/2019 || Propositional dynamic logic (PDL) || 
 +**10th** || 18/12/2019 || Synthesis of CPDS from PDL formulas (1) || 
 +| **11th** || 08/01/2020 || Synthesis of CPDS from PDL formulas (2) || 
 +**12th** || 15/01/2020 || Underapproximate verification for ICPDL (1) || 
 +| || **22/01/2020** || **No lecture** || 
 +| **13th** || 29/01/2020 || Underapproximate verification for ICPDL (2) || 
 +| **14th** || 05/02/2020 || Asynchronous automata || 
 +**15th** || 12/02/2020 || Exercises || 
 +|  || 26/02/2020 || Second exam ||
 ==== Lecture Notes ==== ==== Lecture Notes ====
  
Line 38: Line 47:
  
 [[http://www.lsv.ens-cachan.fr/~gastin/Temp/non-sequential.pdf|Lecture Notes]] [[http://www.lsv.ens-cachan.fr/~gastin/Temp/non-sequential.pdf|Lecture Notes]]
-(version as of 6th October 2019)+(version as of 6th November 2019)
  
 /* /*
 
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