|
|
<WRAP box info round center 85%>
Où, quand ? / Where, when?: In 2024, the course takes place on Fridays from 8h45 to 11h45, starting on September 20 2024, building Sophie Germain in room 1004.
-
Prérequis / Prequisites: Elementary notions from logic (ordinals, …), from complexity, and from recursion theory.
-
-
-
</WRAP>
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
the basic notions of wqo theory, motivated and illustrated by algorithmic applications in various areas, with a particular focus on well-structured transition systems;
-
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;
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.
(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 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).
(S. Schmitz)
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).
<wrap important> exam:</wrap> 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.
Main related courses:
Other related courses:
-
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.
|