Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Beaux préordres et algorithmes / Well-Quasi-Orders for Algorithms (24h, 3 ECTS)

Où, quand ? / Where, when?: The course takes place on Monday in the evening slot (from 16h15 to 19h15), building Sophie Germain room 1003 (not 2035, as previously advertised).

Poly / Lecture notes: can be found at this link Algorithmic Aspects of WQO Theory.

Prérequis / Prequisites: Elementary notions from logic (ordinals, ..), from complexity, and from recursion theory.

Intervenants / Lecturers (2017-18): Jean Goubault-Larrecq (LSV, ENS Paris-Saclay & CNRS) Ph. Schnoebelen, (LSV, ENS Paris-Saclay & CNRS)

Responsable / In charge (2017-18): Alain Finkel, (LSV, ENS Paris-Saclay & CNRS)

Motivations & Abstract

Well-quasi-orderings, or WQOs, play a fundamental role in important results in several areas of computer science : formal language theory, rewriting, program verification, algorithmic graph theory, automated deduction, etc. and they are still intensively used nowadays (see e.g. Separability via Piecewise-Testable Languages by Goubault-Larrecq & Schmitz, or Ordinal-Recursive Complexity by Schmitz & Schnoebelen).

The objective of this course is to teach the basic notions of WQO Theory, motivated and illustrated by algorithmic applications in various areas.

Outline of the course

1. 17 Sep. 2018 (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. The slides. 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 slides. Exercises for next time: 1.6, 1.9, 1.15 (oops, sorry, no: next time), 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 slides. 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 slides.

The homework assignment and midterm exam, to turn in either to Philippe Schnoebelen or by email to Jean Goubault-Larrecq, by October 22nd, 2018, 16h15 sharp.

5. 15 Oct. 2018 (Ph. Schnoebelen): Lossy channel systems and decidability (Sections 1.9 and 3.1). See also this paper.

6. Lossy counters are hard (Section 3): existence of Büchi runs is undecidable, reachability is Ackermann-hard.

7. Ideals in wqos and associated algorithms (Section 4).

8. Revisions before the exam.

Final exam

In 2016 and 2017, the final exam took the form of an oral presentation of research papers linked to the course.

The four previous years, the contents of the course was centered on program verification and well-structured systems, with a final exam in the form of a written exam. Here are the corresponding exam questions (and solutions): exam-2015, exam-2014, exam-2013, exam-2012.

M2 Internships

Here are listed the internship projects that are in direct linked to the topic of MPRI course 2-9-1. M2 students interested in one of these projects should contact the listed adviser.

TitleAdviser(s)LocationFull text
Deciding the Logic of SubsequencesPhilippe SchnoebelenLSV, ENS Paris-Saclaypdf
Model Checking Well Structured Transition SystemsAlain FinkelLSV, ENS Paris-Saclaypdf
Comparing counter machines (with Stefan Göller)Alain FinkelLSV, ENS Paris-Saclaypdf
WQO Finitary Powersets: Complexity and AlgorithmsPhilippe Schnoebelen and Sylvain SchmitzLSV, ENS Paris-Saclaypdf
Well-Structured FIFO AutomataAlain FinkelLSV, ENS Paris-Saclaypdf
Longest chains in Noetherian spaces Jean Goubault-Larrecq and Sylvain SchmitzLSV, ENS Paris-Saclaypdf
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA