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, 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;
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: 15 Sep. 2026: 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: 22 Sep. 2026: 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.5, 1.7, 1.12, 1.29 (warning: this one is still a bit buggy, sorry); in advance, you may try 1.15 (you will need to understand the wqo on multisets), 1.8 (warning: particularly long, and you will need to know about Rado's structure near the end, which we will see next time), 1.10 (same comment).

• lecture 3: 29 Sep. 2026: 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.8, 1.10, 1.11 (beware: 1.8 is particularly long).

• lecture 4: 6 Oct. 2026: 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).

There will be a homework assignment at this point. The homework assignment will be given on this page on 6 Oct. 2026.

(S. Schmitz)

The following programme is provisional. The final programme should contain essentially the same material, up to some form of reordering possibly.

• 13 Oct. 2026: no lecture.

• lecture 5: 20 Oct. 2026: 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.

• 27 Oct. 2026: holidays

• lecture 6: 3 Nov. 2026: 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: 10 Nov. 2026: Complexity upper bounds. What is the maximal length of bad sequences?
  Normed wqos and controlled bad sequences (Section 2.1.1).
  The length function L_g,A(n) and the descent equation, based on residuals A_/a.
  Polynomial and elementary nwqos (Section 2.1.2), analysis of their controlled bad sequences (Section 2.3).
  → Suggested exercises: 2.1, 2.12.

• lecture 8: 17 Nov. 2026: Length Function Theorems and complexity upper bounds (Section 2.4).
  Application: reachability and coverability in lossy counter machines are in the ACKERMANN complexity class (Section 2.4).

• Exam: 24 Nov. 2026 or 1 Dec. 2026: final written exam.

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 are a past homework assignment, another one, and the homework assignment for 2024 with a possible solution.

Here are the exam questions (sometimes with answers) of the 2021 exam, the 2022 exam, the 2023 exam, and the 2024 exam.

Main related courses:

• [ADVERIF] Advanced Techniques of Verification, where wqos are being used, too
• [VCP] Verification of Concurrent Programs, where wqos are being used, too
• [PARAMALG] 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:

• [COMPALG] Efficient Algorithms in Computer Algebra: the computation of Gröbner bases is based on Dickson's Lemma, one of the first results we will see.