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 [2019/10/23 14:27] (current)
gastin [Outline of the course]
Line 24: Line 24:
  
  
-| **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 || 
 +| **5th** || 16/10/2019 || underapproximate verification; co-graphs and tree interpretationspecial tree-width || 
 +| **6th** || 23/10/2019 || special tree-width, decomposition game, examples || 
 +|  ||  || tree interpretation; decision procedures via tree automata ||
 |  ||  || propositional dynamic logic (PDL)|| |  ||  || propositional dynamic logic (PDL)||
 |  ||  || model-checking of existentially bounded behaviors; synthesis from PDL formulas into CPDS || |  ||  || model-checking of existentially bounded behaviors; synthesis from PDL formulas into CPDS ||
 
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