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-9-1 [2019/06/19 18:03]
finkel [Aspects Algorithmic de la Théorie des Beaux préordres / Algorithmic Aspects of WQO Theory (24h, 3 ECTS)]
cours:c-2-9-1 [2019/11/22 11:46] (current)
phs [Evaluation]
Line 2: Line 2:
      
  
-**Où, quand ? / Where, when?:** The course takes place on Monday in the evening slot (from **16h15**  +**Où, quand ? / Where, when?:** The course takes place on Friday in the morning slot (from **08h45**  
-to **19h15**), building Sophie Germain room 1003 (not 2035, as previously advertised).+to **11h45**), building Sophie Germain room 1013.
  
 **Poly / Lecture notes:** can be found at this link **Poly / Lecture notes:** can be found at this link
Line 10: Line 10:
 **Prérequis / Prequisites:** Elementary notions from logic (ordinals, ..), from complexity, and from recursion theory. **Prérequis / Prequisites:** Elementary notions from logic (ordinals, ..), from complexity, and from recursion theory.
  
-**Intervenants / Lecturers (2017-18):**+**Intervenants / Lecturers:**
 [[http://www.lsv.ens-cachan.fr/~goubault/|Jean Goubault-Larrecq]] <goubault@lsv.fr> (LSV, ENS Paris-Saclay & CNRS) [[http://www.lsv.ens-cachan.fr/~goubault/|Jean Goubault-Larrecq]] <goubault@lsv.fr> (LSV, ENS Paris-Saclay & CNRS)
 [[http://www.lsv.ens-cachan.fr/~phs/|Ph. Schnoebelen]], <phs@lsv.fr> (LSV, ENS Paris-Saclay & CNRS) [[http://www.lsv.ens-cachan.fr/~phs/|Ph. Schnoebelen]], <phs@lsv.fr> (LSV, ENS Paris-Saclay & CNRS)
  
  
-**Responsable / In charge (2017-18):**+**Responsable / In charge:**
 [[http://www.lsv.ens-cachan.fr/~finkel/|Alain Finkel]], <finkel@lsv.fr> (LSV, ENS Paris-Saclay & CNRS) [[http://www.lsv.ens-cachan.fr/~finkel/|Alain Finkel]], <finkel@lsv.fr> (LSV, ENS Paris-Saclay & CNRS)
  
Line 34: Line 34:
 ===== Outline of the course ===== ===== Outline of the course =====
  
-1. 17 Sep. 2018 (J. Goubault-Larrecq): Introduction. Definition, a few characterizations of wqos.+1. 13 Sep. 2019 (J. Goubault-Larrecq): Introduction. Definition, a few characterizations of wqos.
 A library of well quasi-ordered data types: announcement, and proofs for the simplest cases.  All the other cases will be seen in further lectures.  Our first wqo: Dickson's Lemma.  Application to coverability of WSTS, and of Petri nets in particular.   A library of well quasi-ordered data types: announcement, and proofs for the simplest cases.  All the other cases will be seen in further lectures.  Our first wqo: Dickson's Lemma.  Application to coverability of WSTS, and of Petri nets in particular.  
 The {{cours:upload:slides-2-9-1-cours1.pdf|slides}}.  The {{cours:upload:slides-2-9-1-cours1.pdf|slides}}. 
 Exercises for next time: 1.1, 1.2, 1.3, 1.22, 1.13, 1.14. Exercises for next time: 1.1, 1.2, 1.3, 1.22, 1.13, 1.14.
  
-2. Petri nets continued.  Dickson's original application. Our second operation on wqos: Higman's Lemma.  Applications: lossy channel systems.  The {{cours:upload:slides-2-9-1-cours2.pdf|slides}}.  +2. 20 Sep. 2019: Petri nets continued.  Dickson's original application. Our second operation on wqos: Higman's Lemma.  Applications: lossy channel systems.  The {{cours:upload:slides-2-9-1-cours2.pdf|slides}}.  
-Exercises for next time: 1.6, 1.9, 1.15 (oops, sorry, no: next time), 1.29.+Exercises for next time: 1.6, 1.9, 1.29.
  
  
-3. Multisets, finite sets, Rado's counterexample.  Van der Meyden's algorithm for satisfiability of disjunctive queries on indefinite databases.  A quick word on parameterized complexity.  Kruskal's theorem.  Application to the termination of rewriting systems.  The {{cours:upload:slides-2-9-1-cours3.pdf|slides}}. +3. 27 Sep. 2019: Multisets, finite sets, Rado's counterexample.  Van der Meyden's algorithm for satisfiability of disjunctive queries on indefinite databases.  A quick word on parameterized complexity.  Kruskal's theorem.  Application to the termination of rewriting systems.  The {{cours:upload:slides-2-9-1-cours3.pdf|slides}}. 
 Exercises for next time: 1.15, 1.5, 1.7, 1.8, 1.10, 1.11, 1.12. Exercises for next time: 1.15, 1.5, 1.7, 1.8, 1.10, 1.11, 1.12.
  
  
-4. Beyond trees: graph minors, and the Robertson and Seymour theorem (no proof).  Applications to algorithmic graph theory.  Beyond wqos: bqos, Noetherian spaces.  Ideals and irreducible (downwards-)closed subsets.  The {{cours:upload:slides-2-9-1-cours4.pdf|slides}}. +4. 4 Oct. 2019: Beyond trees: graph minors, and the Robertson and Seymour theorem (no proof).  Applications to algorithmic graph theory.  Beyond wqos: bqos, Noetherian spaces.  Ideals and irreducible (downwards-)closed subsets.  The {{cours:upload:slides-2-9-1-cours4.pdf|slides}}. 
  
-{{cours:upload:dm-2-9-1-2018.pdf|The homework assignment and midterm exam}}, to turn in either to Philippe Schnoebelen or by email to [[mailto:goubault@lsv.fr|Jean Goubault-Larrecq]], by October 22nd201816h15 sharp. +{{cours:upload:dm-2-9-1-2019.pdf|The homework assignment and midterm exam}}, to turn in either to Philippe Schnoebelen or by email to [[mailto:goubault@lsv.fr|Jean Goubault-Larrecq]], by October 18th20198h30am CEST sharp. 
-A {{cours:upload:dm-2-9-1-2018-ans.pdf|possible solution}}. +A {{cours:upload:dm-2-9-1-2019-ans.pdf|possible solution}}.
-<html> +
-<!-- +
-A [[http://www.lsv.ens-cachan.fr/~goubault/Wqo/dm2018_ans.pdf|possible solution]]. +
- +
-The homework assignment/midterm exam will be given at this time. +
---> +
-</html>+
  
-5. 15 Oct. 2018 (Ph. Schnoebelen): Lossy channel systems and decidability (Sections 1.9 and 3.1). See also [[http://www.lsv.fr/~phs/publis-phs.php?onlykey=phs-rp10|this paper]].+5. 11 Oct. 2019 (Ph. Schnoebelen): Lossy channel systems and decidability (Sections 1.9 and 3.1). See also [[http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf|this paper]]. NB: Students interested in Presburger arithmetic will learn a lot by reading [[https://dl.acm.org/citation.cfm?id=3242964|this recent survival guide]].
  
-6. Lossy counters are hard (Section 3): existence of Büchi runs is undecidable, reachability is Ackermann-hard.+6. 18 Oct. 2019: Lossy counters are hard (Section 3): existence of Büchi runs is undecidable, reachability is Ackermann-hard.
      
-7. Complexity Upper Bounds for WSTS (Section 2): Normed wqos and controlled bad sequences. The Length Function Theorem for polynomials nwqos.+7. 25 Oct. 2019: Complexity Upper Bounds for WSTS (Section 2): Normed wqos and controlled bad sequences. The Length Function Theorem for polynomials nwqos.
  
 <html><!-- <html><!--
Line 71: Line 64:
 --></html> --></html>
  
-8. Ideals in wqos and symbolic algorithms + Revisions before the exam.+**No class on Nov 1st** (holidays). 
 + 
 + 
 +8. 8 Nov. 2019: Revisions before the exam: (1) An application of König's Lemma: prove that a counter machine is unbounded iff it has an unbounded run; (2) exercise 1.7 and application to Integral Relational Automata; (3) exercise 1.18.
  
 <html><!-- <html><!--
Line 112: Line 108:
 --></html> --></html>
  
-===== Final exam =====+===== Evaluation ===== 
 + 
 +The evaluation is in two parts : a homework assignment serving as midterm exam, and a final 2h45-hour written exam on 22 Nov, from 9h to 11h45. Documents & computers are not allowed. 
 + 
 +<html> 
 +<!-- 
 +The {{cours:upload:dm-2-9-1-2019.pdf|homework assignment}} for this year, to be turned it by October 18th, 2019, to Jean Goubault-Larrecq or to Philippe Schnoebelen. 
 +--> 
 +</html> 
 + 
 +Here are {{cours:upload:dm-2-9-1-2018.pdf|last year's homework assignment}} 
 +and 
 +[[http://www.lsv.fr/~phs/exam-M2-9-1-2018.pdf|last year's final exam]]. Versions with solutions are available on request.
  
-[[http://www.lsv.fr/~phs/exam-wanswers-M2-9-1-2018.pdf|Here is the 3-hour final exam with corrections.]]+This year exam with corrections is 
 +[[http://www.lsv.fr/~phs/exam-M2-9-1-2019.pdf|available here]].
  
 <html> <html>
 
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