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