Well-quasi-orderings, or wqos, play a fundamental role in important results in multiple areas of computer science: formal language theory, rewriting, program verification, algorithmic graph theory, automated deduction, etc., and they are still intensively used nowadays. At their very core, a wqo is a tool to prove finiteness statements; a major use is to show the termination of algorithms—where wqos provide a generalisation of well-founded linear orders. In particular, this has led to the definition of an abstract class of systems, called well-structured transition systems (WSTS), for which generic algorithms for various decision problems can be provided (in particular verification problems), and the termination of those algorithms relies on wqos.

The objective of this course is to present

1. the basic notions of wqo theory, motivated and illustrated by algorithmic applications in various areas, with a particular focus on well-structured transition systems and their automated verification;
2. a glimpse at the limitations of wqos, along with the possible solutions through better quasi orders (bqos) or Noetherian topological spaces;
3. beyond proofs of termination, how to instrument wqos in order to extract complexity upper bounds, and how these match the lower bounds for some natural decision problems;
4. as required by the previous point, an introduction to subrecursive hierarchies, i.e., ordinal-indexed hierarchies of recursive functions, and the associated complexity classes for very high complexity problems;

An application of these techniques is the proof of the ACKERMANN-completeness of the reachability problem for Petri nets—which is not covered in this course, as this would be a topic for an entire course on its own.

The course is usually split into two parts, corresponding roughly to points 1–2 and 3–4 above.

The section/chapter/exercise numbers refer to the lecture notes.

(J. Goubault-Larrecq)

• lecture 1: 20 Sep. 2024: Introduction. Definition, a few characterisations of wqos (Section 1.1).
  A library of well quasi-ordered data types: announcement, and proofs for the simplest cases (Section 1.2). All the other cases will be seen in later lectures.
  Our first wqo: Dickson's Lemma (Section 1.3).
  Application to coverability of WSTS (Section 1.9), and of Petri nets in particular.
  → The slides (with animations), and the short slides (without animations).
  → Exercises for next time: 1.1, 1.2, 1.3, 1.22, 1.13, 1.14.

• lecture 2: 27 Sep. 2024: Petri nets continued.
  Dickson's original application (section 1.10.7).
  Our second operation on wqos: Higman's Lemma (Section 1.4).
  Applications: lossy channel systems.
  → The slides (with animations), and the short slides (without animations).
  → Exercises for next time: 1.6, 1.9, 1.29.

• lecture 3: 04 Oct. 2024: Multisets, finite sets, Rado's counterexample (Section 1.5).
  Van der Meyden's algorithm for satisfiability of disjunctive queries on indefinite databases (Section 1.10.5).
  A quick word on parameterised complexity (Section 1.10.6).
  Kruskal's Tree Theorem (Section 1.6).
  Application to the termination of rewriting systems (Section 1.10.4).
  → The slides (with animations), and the short slides (without animations).
  → Exercises for next time: 1.15, 1.5, 1.7, 1.8, 1.10, 1.11, 1.12 (beware: 1.8 is particularly long).

• lecture 4: 11 Oct. 2024: Return of Dickson: Application to polynomial systems, Gröbner bases, and Buchberger's algorithm (Sections 1.10.8 & 1.10.9).
  → The slides (with animations), and the short slides (without animations).
  Beyond trees: graph minors, and Robertson and Seymour's Graph Minor Theorem (no proof). Applications to algorithmic graph theory (Section 1.7).
  If time permits: beyond wqos: bqos, Noetherian spaces (Section 1.11); (order) ideals and irreducible (downwards-)closed subsets (Section 1.8).
  → The slides (with animations), and the short slides (without animations).

• homework: 25 Oct. 2024: deadline for the homework assignment, to be sent to Jean Goubault-Larrecq in electronic form (LaTeX or scanned). No late submissions allowed.
  Here is a possible solution.

(S. Schmitz)

• lecture 5: 18 Oct. 2024: Long bad sequences (intro to Chapter 2).
  Ordinals and ordinal notations, subrecursive functions: the Hardy functions (Appendix A).
  Complexity classes beyond ELEMENTARY (Appendix B and article).
  → Suggested exercises: 2.2, 2.3, 2.13, 2.11, 2.15.

• lecture 6: 25 Oct. 2024: Lossy counter machines (Section 3.1.3, cheat sheet).
  Hardness: boundedness is undecidable (exercise), reachability and coverability are ACKERMANN-hard (Chapter 3, article).
  → Suggested exercises: 3.1, 3.2, 3.3, 3.4.

• lecture 7: 08 Nov. 2024: Complexity upper bounds: motivation from the backward coverability algorithm (Section 2.2.2)
  Normed wqos and controlled bad sequences (Section 2.1.1).
  The Cichoń functions (Section 2.4.2) and the Length Function Theorem for ordinals in ε₀ (article, habilitation).
  Polynomial wqos (Section 2.1.2), analysis of their controlled bad sequences (Section 2.3).
  → Suggested exercises: 2.1, 2.12

• lecture 8: 15 Nov. 2024: An overview of the Length Function Theorem for polynomial normed wqos, using maximal order types and natural ordinal operations (Section 2.4).
  Application: reachability and coverability in lossy counter machines are in the ACKERMANN complexity class (Section 2.4, article).
  Quick reminder on ideals of wqos (Section 4.1)
  Effective representations of ideals (Section 4.2): the example of Idl(ℕᵈ) (Sections 4.3.1 & 4.3.2).
  Quick overview of a few applications of ideals: forward coverability (Section 4.4.1), mention of dual backward coverability (Section 4.4.2, article).

• exam: 22 Nov. 2024: final written exam. Duration: 2:15 hours. Documents: at most 2 sheet of papers, with your name on both. Here are possible answers.
  See below for examples of past final exams.

The evaluation is in two parts: a homework assignment serving as midterm exam, and a final written exam.

• Here is the homework assignment for 2024, to be turned in by email to Jean Goubault-Larrecq at or before Friday, October 25th, 2024. Here is a possible solution.

• The final written exam took place on November 22, 2024. Duration: 2:15.

Here are a past homework assignment, the 2019 final exam, the 2023 final exam, and the 2024 final exam.

Main related courses:

• Advanced techniques of verification, where wqos are being used, too
• Algorithmic Verification of Programs, where wqos are being used, too
• Parameterized algorithms and complexity: the algorithms we will see in database theory and in graph theory are a natural introduction to the notion of parameterised complexity.

Other related courses:

• Polynomial systems, computer algebra, and applications: the computation of Gröbner bases is based on Dickson's Lemma, one of the first results we will see
• Advanced Graph Theory: we will mention Robertson and Seymour's Theorem, on well-quasi-ordering graphs by minors, and it will be important in the advanced graph theory course.