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: 17 Sep. 2025: 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: 24 Sep. 2025: 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: 30 Sep. 2025: 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: 1st Oct. 2025: 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: The homework assignment, given on this page on 8th Oct. 2025.
  → Deadline for the homework assignment: 22 Oct. 2025

(Ph. Schnoebelen)

• lecture 5: 15 Oct. 2025: Verifying Lossy Counter Machines and WSTSes.
  Minsky Counter machines (Section 3.1). Their definitions and operational semantics. Minsky machines are Turing-powerful, even when restricted to 2-counter machines (a classic result, see wikipedia).
  Lossy Counter machines (LCMs) are Counter machines with a modified operational semantics (section 3.1.3). They are WSTS. For LCMS, Termination is decidable (Thm 4.2 of cheat sheet) as well as General_Reachability, i.e., X –^*→ Y for X,Y semilinear sets of configurations (Thm 3.3 of cheat sheet).
  See wikipedia for classic recalls on semilinear sets and Presburger logic.

• lecture 6: 22 Oct. 2025: Hardness of WSTS verification. For Lossy Counter Machines (LCMs) the existence of a Büchi run is undecidable. The proof relies on a useful gadget: putting counter machines on a budget.
  The boundedness property, i.e., the finiteness of the reachability set Post^*(𝜎₀), is undecidable too (Section 7.3 & 7.4 of cheat sheet). Coro: there is no method to compute Post^*(𝜎₀) for LCMs, contrasting the fact that we can compute Pre^*(𝜎_f).
  The Grzegorczyk hierarchy (F_k:ℕ→ℕ)_k∊ℕ of primitive recursive functions (Section 2.1.3) and the Ackermann function A(n)≝F_n(n).
  For LCMs, Reachability and Termination are decidable but Ackermann-hard (see details in hardness paper).
  → Suggested exercises: 2.2, 2.3.

• 29 Oct. 2025: holidays.

• lecture 7: 5 Nov. 2025: 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: 12 Nov. 2025: Length Function Theorems and complexity upper bounds.

• Exam: 19 Nov. 2025: final written exam. Duration: 2 hours, from 9h45 to 11h45. Documents: at most 2 sheet of papers, with your name on both. Please tell me in advance (or email me) if you require special exam conditions, e.g. extra time or isolated room, so that I can organize in consequence.
  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.

• The final written exam took place on November 19, 2025. Duration: 2:15.

Here are a past homework assignment, another one; the 2019 final exam, the 2023 final exam, and the 2024 final 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
• [GRAPHTH] Advanced Graph Theory (suspended this year): 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.