My first thanks go to all the people I have worked along with at the Laboratoire Spécification et Vérification in Cachan over the nine years I have spent there since 2008: to the administrative and technical staff for their kindness and availability, to my current students Simon Halfon and Anthony Lick and my former intern and visiting students for thought-provoking discussions, and to all my colleagues for creating such a supportive and stimulating environment-it has been an incredibly formative experience, I have learned so much from all of you. Special thanks go to Alain Finkel, Jean Goubault-Larrecq, and Philippe Schnoebelen, who introduced me to the theory of well-quasi-orders when I arrived in Cachan.

Let me thank more generally all my co-authors over the years: it has been a privilege to work by your side. My lasting collaborations with Ranko Lazić and Philippe Schnoebelen have been especially influential: little of the work described in this habilitation would have existed without you.

I also thank the members of the jury for their excellent comments and corrections on the manuscript, and for their patience and goodwill during the entire process.

I have also benefited from the fantastic opportunity to teach at École Normale Supérieure Paris-Saclay all over these nine years; the demands of tutoring and lecturing to such an exacting audience have had a deep influence. I thank my students and everyone I shared a course with, and in particular Paul Gastin for his guidance as head of the computer science department when I started on the job, at what was then called ENS Cachan.

To end on a personal note, I give my heartful thanks to Marie Antczak, Claire David, Laure Daviaud, Mahsa Shirmohammadi, and everyone else who joined in the nudging and encouraged me to complete this habilitation thesis.

Thank you! Introduction 1.1. General Context

The main motivations for this thesis are rooted in formal verification, and in particular in model-checking techniques. This might come as a surprise, because the title seems centred on well-quasi-orders, which are a rather abstract concept, whose invention can be tracked back to the early 1910s and whose theory was developed by mathematicians like [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF], [START_REF] Kruskal | The theory of well-quasi-ordering: A frequently discovered concept[END_REF], [START_REF] De Jongh | Well-partial orderings and hierarchies[END_REF], and many others. Model-checking on the other hand, while certainly grounded on sound mathematical concepts [e.g. [START_REF] Vardi | From philosophical to industrial logics[END_REF], is an eminently practical field of computer science with a widespread adoption in the hardware industry. At its core, it consists of a fully automated, algorithmic check that a model of a system-like a concrete sequential circuit-satisfies its specificationlike a safety check that no bad configuration can ever be reached in the model.

Verification of Infinite-state Systems.

Once the general underpinnings of model-checking for finite-state systems were well-understood, the focus of the formal verification community turned in the 1990s to infinite-state systems. Indeed, many critical systems worth the time and effort required by formal verification are infinite, due to unbounded variables: integer counters, number of active threads in concurrent settings, real-time clocks, stacks, nonces, communication channels, etc. In some specific instances, these infinite-state systems are 'essentially finite-state' and can be faithfully abstracted into finite ones by finite partitioning, i.e. by quotienting them using a bisimulation equivalence of finite index-this method was notably behind the success of timed automata [START_REF] Alur | A theory of timed automata[END_REF]. But at that time this research area was lacking common methods and general principles to cope with cases where finite partitioning failed.

A Game Changer:

Well-Structured Systems. This situation was remedied by [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF] and [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], who popularised the notion of well-structured systems. Their approach can be understood as a generalisation of the finite partitioning method, using instead simulation quasi-orders. The finiteness condition on the equivalence's index was accordingly replaced by a much more flexible condition: this quasi-order should be a well-quasi-order (a wqo).

The two landmark papers by Abdulla et al. and Finkel and Schnoebelen identified two generic algorithmic constructions, backward coverability and finite reachability trees, which terminate in well-structured systems and allow to check properties like safety (through the coverability problem), inevitability, termination, boundedness, simulation relations, etc. This provided a unifying explanation of several existing decidability results, and guidelines for discovering similar results in future classes of systems.

INTRODUCTION

Already in 2000, this simple abstract framework had been shown to capture varied concrete formalisms, including extensions of vector addition systems, communicating finite-state machines, process algebra, or timed systems. Twenty years later, this catalogue of applications still keeps growing, with unforeseen farreaching theoretical applications, like the decidability of logics-including metric temporal logics [START_REF] Ouaknine | On the decidability and complexity of Metric Temporal Logic over finite words[END_REF], data logics [START_REF] Figueira | Alternating register automata on finite words and trees[END_REF], interval temporal logics [START_REF] Bresolin | Interval temporal logics over finite linear orders: The complete picture[END_REF], and substructural logics [J1; J4]. Thus the title 'Well-Structured Transition Systems Everywhere!' of Finkel and Schnoebelen's article has turned out to be a self-fulfilling prophecy.

1.1.3. Tools and Practical Applications. Well-structured systems are also at the origin of numerous practical applications, which target among others the automatic verification of parametric systems and of multi-threaded programs. Infinite-state models like vector addition systems and their extensions are indeed necessary in order to analyse systems where correctness should hold for any number of components, or where dynamic creation of processes or execution threads can occur. These tools typically implement highly optimised versions of the backward coverability principle, sometimes alongside forward pruning of the state space, and are able to cope with practical instances extracted from multi-threaded programs, cache coherence protocols, communication protocols, memory managers, etc. [Blondin et al., 2017b;[START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF][START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF][START_REF] Geffroy | Occam's Razor applied to the Petri net coverability problem[END_REF][START_REF] Geffroy | Backward coverability with pruning for lossy channel systems[END_REF][START_REF] Geeraerts | Reasoning about systems with many processes[END_REF][START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF][START_REF] Kaiser | Lost in abstraction: Monotonicity in multi-threaded programs[END_REF].

1.1.4. The Complexity Question. Although the theory of well-structured systems provides generic algorithms for numerous verification problems, it might seem rather unclear, what the computational cost of running these generic algorithms might be. Indeed, the underlying well-quasi-orders ensure that the algorithm will eventually terminate, but the usual proofs of this fact are not constructive and do not provide any information as to when that will happen.

What was however known thanks to [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF] was that the worstcase complexity could be considerable. Indeed, Schnoebelen showed that checking safety in two of the main well-structured formalisms, namely lossy counter systems and lossy channel systems, is not primitive-recursive. Thus the worstcase complexity of checking even small systems exceeds the known estimates for physical quantities like the number of atoms in the observable universe or the number of nanoseconds since the Big Bang, and these problems might be better labelled as 'not undecidable. ' We could stop there on the question of the complexity of algorithms on wellstructured systems. Such lower bounds indicate that, as far as practical verification goes, the problems are not that different from undecidable ones. That is, we should not be deterred because those are worst-case bounds that say little about the difficulty of solving practical instances, which presumably do not attempt to implement complex computations of Turing or Minsky machines.

I can easily argue here that the point of complexity theory is very rarely to estimate the running times observed on implementations over realistic inputs. 1 The interest rather lies in finely understanding the computational problem at hand, in 1 The exception being average-case complexity analysis for a suitable probability distribution on the inputs, which is fiendishly difficult even for simple algorithms, not to mention how hard it is to invent a 'realistic' probability distribution.

having at least a crude notion of optimality for it, in identifying its main sources of complexity, in comparing the complexity of its different algorithms.

Additionally, in the context of well-structured systems where there are many different families of systems using various wqos, computational complexity also serves as a proxy for expressiveness, where algorithmic lower bounds allow to prove that some classes of models cannot be efficiently encoded into others. From this expressiveness perspective, a highly expressive but nevertheless not undecidable formalism also indicates an interesting modelling trade-off.

Contributions

In this thesis, I present a comprehensive assortment of results answering the 'complexity question' for algorithms that rely on well-quasi-orders for their termination, like the briefly mentioned backward coverability algorithm in wellstructured systems. I cover both upper bounds and lower bounds techniques, the definition of suitable complexity classes, and provide applications in verification (prominently for well-structured systems). Because wqos are in such wide use, this topic is of relevance to a broad community with interests in complexity theory and decision procedures for logical theories. As a testimony to this wide applicability, I refer the reader to [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Section 6], which contains a surprisingly large catalogue of decision problems shown complete for the complexity classes described herein.

After a brief overview of the algorithmic applications of well-quasi-orders in Chapter 2, I present some of my contributions to this recent research direction in Chapters 3 to 5, which I summarise next.

Techniques for Upper Bounds.

As shown in Chapter 2, many algorithms rely on well-quasi-orderings for their proof of termination. Although the classical proofs of Dickson's Lemma, Higman's Lemma, and other wqos, are of non-constructive nature, the way they are typically applied in algorithms lends itself to constructive proofs, from which complexity upper bounds can be extracted and applied to evaluate algorithmic complexities. The resulting combinatorial statements are dubbed length function theorems, as they allow to bound the length of so-called 'controlled bad sequences' over the wqo at hand. 1.2.1.1. Length Function Theorems. I present in Chapter 3 how one can derive complexity upper bounds for algorithms relying for their termination on ordinals below ε 0 [I3] or Dickson's Lemma over tuples of natural numbers [C19]. The techniques are however quite generic and apply to more complex wqos [START_REF] Rosa-Velardo | Ordinal recursive complexity of unordered data nets[END_REF]C18]. Contribution (I3; C18; C19). Length function theorems for several wellquasi-orders: Dickson's Lemma, Higman's Lemma, ordinals below ε 0 , and their combinations.

This topic had already been explored in research communities centred on proof theory and rewriting theory [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF][START_REF] Ketonen | Rapidly growing Ramsey functions[END_REF][START_REF] Mcaloon | Petri nets and large finite sets[END_REF][START_REF] Weiermann | Complexity bounds for some finite forms of Kruskal's Theorem[END_REF], and my results with Figueira, Figueira, and Schnoebelen rely on the same mathematical tools-broadly speaking, maximal order types and subrecursive functions [e.g. [START_REF] Buchholz | A uniform approach to fundamental sequences and hierarchies[END_REF]-, but provide refined bounds and more general statements on the wqos we consider. Importantly, we showed how to apply these techniques to the algorithms 1. INTRODUCTION employed in the literature on well-structured systems, making them accessible to the infinite-state verification community and fostering their adoption. 1.2.1.2. Monotone Descending Sequences. Length function theorems on controlled bad sequences are however not able to account for some results. A case in point is the coverability problem in vector addition systems, where length function theorems only provide Ackermannian upper bounds, although coverability witnesses were shown to be of double exponential length by [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. In joint work with Lazić [W1], we showed how a dual view of the usual backward coverability algorithm, that builds a descending sequence of downwards-closed sets instead of an ascending sequence of upwards-closed sets, exhibits a monotonicity invariant yielding the desired double exponential bound. The same approach has since been used to obtain tight bounds in ν-Petri nets [C5] and polynomial automata [START_REF] Benedikt | Polynomial automata: Zeroness and applications[END_REF]. I touch this subject in Section 6.3.2. Contribution (C5; W1). Length function theorems for monotone descending sequences of downwards-closed sets over tuples of natural numbers and finite multisets of such tuples.

Techniques for Lower Bounds.

The complexity upper bounds provided by length function theorems are typically not primitive-recursive, and one is bound to wonder whether they are useful at all, i.e. whether there exist natural decision problems that require Ackermannian resources for their resolution. As shown in pioneering works by [START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF], [START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF], and [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF], such gigantic complexities are actually tight for problems on counter machines. 1.2.2.1. Hardy Computations. I illustrate these lower bound techniques in Section 4.2 in the case of coverability in lossy counter machines. While the general pattern of these lower bound proofs relies on weak computer implementations of fast-growing functions and their inverses as in [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF][START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF][START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]2010a;[START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF], my contribution lies in the implementation of Hardy computations using robust encodings of ordinals. This allows to considerably simplify the proofs, which quickly become horrendously involved in more expressive formalisms like priority channel systems [J5], lossy channel systems [C14], ordered data nets [C16], nested counter systems [START_REF] Decker | On freeze LTL with ordered attributes[END_REF], or unordered data nets [START_REF] Rosa-Velardo | Ordinal recursive complexity of unordered data nets[END_REF].

Contribution (Theorem 4.9; J5; C14; C16; L1). Hardy-like computations for proving complexity lower bounds in well-structured systems.

The particular lower bound statement in Theorem 4.9 of this thesis is an original contribution: it slightly improves over the known lower bounds for the coverability problem in lossy counter machines with a fixed number of counters [Schnoebelen, 2010a], and thus in other extensions of vector addition systems where these bounds apply: reset Petri nets, transfer Petri nets, broadcast protocols, … 1.2.2.2. Counter Objects. The approach through weak computers fails to provide tight lower bounds in some cases, including prominently vector addition systems. For the sake of completeness, I briefly discuss in Section 4.3.1 another approach introduced by [START_REF] Lipton | The reachability problem requires exponential space[END_REF] to show the EXPSPACE-hardness of coverability in vector addition systems. This has been instrumental in obtaining lower bounds for several classes of well-structured systems [J4; C5; C9; C21].

Complexity Classes.

Complexity classes, along with the associated notions of reductions and completeness, allow us to classify and compare computational problems. 1.2.3.1. Non-Elementary Problems. The complexity literature does not provide any intermediate stops where well-known non-elementary problems-like WS1S, the satisfiability problem for the weak monadic theory of one successor [START_REF] Meyer | Weak monadic second order theory of successor is not elementary-recursive[END_REF]-would fit adequately. Indeed, WS1S is not in ELEMENTARY, but the next class is PRIMITIVE-RECURSIVE, which is far too big: WS1S is not hard for PRIMITIVE-RECURSIVE under any reasonable notion of reduction. In other words, we seem to be missing a 'TOWER' complexity class, which ought to sit somewhere between ELEMENTARY and PRIMITIVE-RECURSIVE. Going higher, we find a similar uncharted area between PRIMITIVE-RECURSIVE and RECURSIVE, where all the decision problems considered in this thesis should fit. 21.2.3.2. Fast-Growing Complexity. In Section 4.1, I present a proposal for complexity classes above ELEMENTARY, which has already proven suitable for many decision problems [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Section 6].

Contribution (J3). The definition of fast-growing complexity classes (F α ) α suitable for non-elementary complexity.

The classes F α are related to the hierarchy (E k ) k of Grzegorczyk [1953] and the extended Grzegorczyk hierarchy (F α ) α of [START_REF] Löb | Hierarchies of number theoretic functions[END_REF], which have been used in most older complexity statements involving non-elementary bounds in the literature. The (F α ) α classes are well-suited for characterising various classes of functions, for instance computed by forms of 'for' programs [START_REF] Meyer | The complexity of loop programs[END_REF] or terminating 'while' programs [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF], or provably total in fragments of Peano arithmetic [e.g. [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF]], and they characterise some important milestones like the classes of elementary or primitive-recursive decision problems. They are however too large to classify decision problems arising from the use of wqos in algorithms: they do not lead to completeness statements-in fact, one can show that there are no 'ELEMENTARYcomplete' nor 'PRIMITIVE-RECURSIVE-complete' problems.

A Challenge: the Complexity of VASS Reachability.

Vector addition systems (VASS), or equivalently Petri nets, find a wide range of applications in the modelling of concurrent, chemical, biological, or business processes. Their algorithmics, and in particular the decidability of their reachability problem, is a central component to many decidability results spanning from the verification of asynchronous programs [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF] to the decidability of data logics [START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Demri | Reasoning about data repetitions with counter systems[END_REF].

Considered as one of the great achievements of theoretical computer science, the original 1981 decidability proof of Mayr is the culmination of more than a decade of research into the topic, and builds notably on an incomplete proof by [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems[END_REF]. The proof was simplified a year later by [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]. In spite of this success, as put by Lambert in his 1992 article presenting his own simplification of the proof,

INTRODUCTION

'the complexity of the two proofs (especially in [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF]) wrapped the result in mystery, ' and no complexity upper bound was known for the general VASS reachability problem, while the best known lower bound is EXPSPACE-hardness [START_REF] Lipton | The reachability problem requires exponential space[END_REF]. The only known tight bounds pertain to the case of 2-dimensional VASS, which were recently shown to have a PSPACE-complete reachability problem when using binary encodings [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF], and even an NL-complete one with unary encodings [START_REF] Englert | Reachability in two-dimensional unary vector addition systems with states is NL-complete[END_REF]. 1.2.4.1. Upper Bound. I present in Chapter 5 the first known complexity upper bounds for the reachability problem, by analysing the algorithm of Mayr, Kosaraju, and Lambert using the length function theorems presented in Chapter 3.

Contribution (Theorem 5.1;[START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF]. The first complexity upper bounds for reachability in vector addition systems.

More precisely, the result in Theorem 5.1 is a small improvement over the 'cubic Ackermann' upper bound obtained with Leroux in [C8]: I show a 'quadratic Ackermann' upper bound, in F ω 2 in terms of the complexity classes of Chapter 4. This bound is not expected to be tight. However, as observed e.g. by [START_REF] Müller | The reachability problem for VAS[END_REF] the algorithms of Mayr, Kosaraju, and Lambert are not primitive-recursive. Thus the complexity gap for these particular algorithms, between F ω and F ω 2 , is not that wide. 1.2.4.2. Ideal Decompositions. At the heart of these decidability proofs lies a decomposition technique, which is dubbed the Kosaraju-Lambert-Mayr-Sacerdote-Tenney (KLMST) decomposition after its inventors. In a nutshell, the KLMST decomposition defines both a structure and a condition for this structure to represent in some way the set of all runs witnessing reachability. The algorithms advanced by Mayr, Kosaraju, and Lambert compute this decomposition by successive refinements of the structure until the condition is fulfilled.

The 'mystery' that shrouds the KLMST decomposition algorithm does not relate to how these structures and conditions are used in the algorithms themselves, nor to the fact that they indeed yield the decidability of VASS reachability. Rather, the issue is to explain how these structures and conditions can be derived in a principled manner. This is what Leroux and I attempt to address in [C8]; I give a quick overview of this result in Section 6.4.2. Using a well-quasi-ordering on VASS runs studied by [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF] and [START_REF] Leroux | Vector addition system reachability problem: a short selfcontained proof[END_REF], we showed a Decomposition Theorem (Theorem 6.3): the KLMST algorithm computes the ideal decomposition of the set of runs, i.e. a decomposition into irreducible downward-closed sets (see Section 6.3.1). The effective representation of those ideals through finite structures turns out to match exactly the structures and conditions expressed by [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF].

Contribution (C8). Explain the KLMST decomposition algorithm in terms of ideal decompositions of a well-quasi-order. This provides a full formal framework in which the reachability problem in various VASS extensions might be cast, offering some hope to see progress on those open issues.

Other Contributions.

Although it is the main focus of this document, my work does not revolve exclusively around the complexity of wqo algorithms. I would like to mention here a few significant contributions that could not be presented in the remainder of this thesis.

1.2.5.1. Substructural Logics. One of the applications of counter systems is to provide algorithmic techniques for other formalisms. For instance, strong connections can be drawn between branching and alternating extensions of vector addition systems on the one hand, and proof systems for substructural logics like linear logic or relevance logic on the other hand. By reducing logic problems to reachability problems in such extensions, I have been able to solve two longstanding open problems.

Contribution (J1). The implicational implicational fragment of relevance logic is 2-EXP-complete.

This fragment had been proven decidable by Kripke in 1959, and no progress had been made since Urquhart's 1990 EXPSPACE lower bound and 1999 ACKERMANN upper bound. The problem is also equivalent to simple type inhabitation in the λI-calculus.

Contribution (J4). Propositional affine linear logic is TOWER-complete.

This logic had been shown decidable by [START_REF] Kopylov | Decidability of linear affine logic[END_REF] no known upper bound. This work with Lazić further provides the best known lower bound for multiplicative exponential linear logic (MELL), whose decidability is a major open problem since the 1990s [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF]-see Section 6.4. 1.2.5.2. Energy Games. Alternating vector addition systems also capture a class of 'resource-conscious' games called multi-dimensional energy parity games, employed for the synthesis of reactive systems. The motivation here is to generate automatically a correct system against some functional requirements, that furthermore guarantees that several discrete resources (e.g., available funds, items in stock, units of fuel or time, …) will never get depleted. Contribution (C1; C7; C9). Multi-dimensional energy parity games are This series of articles, first with Courtois, and later in collaborations with Jurdziński, Lazić, and Colcombet, also shows the problem to be in pseudo-polynomial time in fixed dimension. Our results are based on geometric intuitions, which we formalise by introducing perfect half-space games. They answer open problems for multi-dimensional energy games [START_REF] Velner | The complexity of multi-mean-payoff and multi-energy games[END_REF], extended games on vector addition systems [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF], simulation games in basic parallel processes [START_REF] Lasota | EXPSPACE lower bounds for the simulation preorder between a communication-free Petri net and a finite-state system[END_REF], multi-agent resource logics [START_REF] Alechina | On the complexity of resource-bounded logics[END_REF], an affine variant of (⊕, !)-Horn linear logic [START_REF] Kanovich | Petri nets, Horn programs, linear logic and vector games[END_REF], and single-sided µ-calculus model-checking on vector addition systems [START_REF] Abdulla | Solving parity games on integer vectors[END_REF].

CHAPTER 2

Well-Quasi-Orders & Applications

A quasi order (qo) ⟨A, ≤⟩ consists of a support set A along with a transitive reflexive relation ≤ ⊆ A × A. We call a finite or infinite sequence x 0 , x 1 , x 2 , . . . over A good if there exist two indices i < j such that x i ≤ x j , and bad otherwise. A well-quasi-order (wqo) is a qo ⟨A, ≤⟩ such that any infinite sequence x 0 , x 1 , x 2 , . . . of elements over A is good. Equivalently, any bad sequence over A is finite.

Thus well-quasi-orders are a means to proving finiteness statements. A typical application is program termination, which can be shown by mapping any execution sequence of a program to a bad sequence of longer or equal length: as bad sequences are finite, so are executions, and this shows that the program terminates (see Section 2.2). A second application is found in well-structured transition systems (see Section 2.3), where configurations are ordered with a wqo compatible with the transitions: a large portfolio of algorithms relying on wqos for termination is available on these systems [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], with applications in verification, logic, distributed computing, etc.

The material in this chapter is mostly standard. The presentation is based chiefly on the lecture notes [L1] and the invited papers [I4

Basic Definitions

The upward-closure ↑B of some B ⊆ A in a qo ⟨A, ≤⟩ is defined as ↑B def = {x ∈ A | ∃y ∈ B, x ≥ y}. We write ↑x instead of ↑{x} for singletons. When B = ↑B, we say that B is upwards-closed. The downward-closure ↓B of B and the notion of downwards-closed sets are defined symmetrically.

2.1.1.

Well-Quasi-Orders. The definition of a wqo as enforcing finite bad sequences is just one among many equivalent ones [START_REF] Kruskal | The theory of well-quasi-ordering: A frequently discovered concept[END_REF]. Notably, ⟨A, ≤⟩ is a wqo if and only if

(1) ≤ is well-founded, i.e. there does not exist any infinite decreasing sequence

x 0 > x 1 > x 2 > • • • of elements in A, where < def = ≤ \ ≥,
0 ⊆ U 1 ⊆ U 2 ⊆ • • • of upwards-closed subsets of A eventually stabilises, i.e., ∪ i∈N U i = U k = U k+1 = U k+2 = • • • for some k. Indeed, for the 'only if' direction, in a strictly increasing sequence U 0 ⊊ U 1 ⊊ U 2 ⊊ • • • of upwards-closed subsets of A, we can extract at each step an element x i ∈ U i+1 \ U i . If i < j, then x i ≤ x j would imply x j ∈ U i+1 since U i+1 is upwards-closed, but this contradicts x j ̸ ∈ U j .
Hence the sequence of elements x 0 , x 1 , x 2 , . . . is bad and the strictly increasing sequence U 0 ⊊ U 1 ⊊ U 2 ⊊ • • • is finite. Note that we can assume each x i to be a minimal element of U i+1 in the previous argument: if every minimal element of U i+1 were in U i , then U i ⊇ U i+1 .

2.1.1.2. Finite Basis Property. Upwards-and downwards-closed sets of wqos are important algorithmic tools: they are subsets of A that can be finitely represented and handled. The simplest generic representation is by minimal elements. Indeed, the finite antichain condition ensures that, in any subset of A, there are finitely many minimal elements up to the equivalence ≡ def = ≤ ∩ ≥. Thus any upwards-closed U ⊆ A can be written as the upward-closure of finitely many elements, i.e. U = ↑{x 1 , . . . , x n } for some x 1 , . . . , x n ∈ A. One can see how, using this representation, the comparison of possibly infinite (but upwards-closed) sets can be reduced to finitely many comparisons of elements.

The complement of a downwards-closed set D is upwards-closed. Hence downwards-closed subsets of a wqo can be characterised by so-called excluded minors. That is, every downwards-closed D can be associated with a finite set

{x 1 , . . . , x n } such that x ∈ D if and only if x 1 ̸ ≤ x ∧ • • • ∧ x n ̸ ≤ x.
Here the x i s are the excluded minors and D is 'everything that does not have one of them as a minor'. We will see another representation of downwards-closed sets in Section 6. -Orders. A wqo where ≤ is antisymmetric is called a well-partial-order (wpo). Note that quotienting a wqo by the equivalence ≡ def = ≤ ∩ ≥, i.e. equating elements x and y whenever x ≤ y and y ≤ x, yields a wpo.

A wpo ⟨A, ≤⟩ where ≤ is linear (aka total), is a well-order (wo). Because a wo has antichains of cardinal at most 1, this coincides with the usual definition as a well-founded linear order. Finally, any linearisation of a wpo ⟨A, ≤⟩, i.e. any linear order ⪯ ⊇ ≤, defines a wo ⟨A, ⪯⟩. One can think of the linearisation process as one of 'orienting' pairs of incomparable elements; such a linearisation always exists thanks to the order-extension principle. Note that, over a linear order, a bad sequence x 0 , x 1 , . . . is actually a decreasing sequence

x 0 > x 1 > • • • . 2.1.2.
Examples. For a basic example, consider any finite set Q along with the equality relation, which is a wqo ⟨Q, =⟩ by the pigeonhole principle. As explained above, any wo is a wqo, which provides us with another basic example: the set of natural numbers along with its natural ordering ⟨N, ≤⟩.

Many more examples can be constructed using algebraic operations: for instance, if ⟨A, ≤ A ⟩ and ⟨B, ≤ B ⟩ are wqos, then so are:

• their disjoint sum ⟨A ⊔ B, ≤ ⊔ ⟩ with the sum ordering: A ⊔ B def = {(x, 0) | x ∈ A} ∪ {(y, 1) | y ∈ B} and (z, i) ≤ ⊔ (z ′ , j) if and only if i = j and z ≤ C z ′ where C def = A if i = 0 and C def = B otherwise, • their Cartesian product ⟨A×B, ≤ × ⟩ with the product ordering: (x, y) ≤ × (x ′ , y ′ ) if and only if x ≤ A x ′ and y ≤ B y ′ ; in the case of ⟨N d , ≤ × ⟩ this
result is also known as Dickson's Lemma [START_REF] Dickson | Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors[END_REF],

• ⟨A * , ≤ * ⟩, the set of finite sequences over A along with subword embedding:

x 1 • • • x m ≤ * y 1 • • • y n if and only if there exists an increasing f : {1, . . . , m} → {1, . . . , n} such that x i ≤ A y f (i) for all 1 ≤ i ≤ m;
this result is better known as Higman's Lemma [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF],

• the set of finite trees labelled by A with the homeomorphic embedding, aka Kruskal's Tree Theorem [START_REF] Kruskal | Well-quasi-ordering, the Tree Theorem, and Vazsonyi's Conjecture[END_REF][START_REF] Nash-Williams | On well-quasi-ordering finite trees[END_REF], and • the set of finite graphs labelled by A with the minor ordering, aka the Graph Minor Theorem [START_REF] Robertson | Graph minors. XXIII. Nash-Williams' immersion conjecture[END_REF]. Turning to well orders, an operation that preserves wos is the lexicographic product ⟨A × B, ≤ lex ⟩ where (x, y) ≤ lex (x ′ , y ′ ) if and only if x < A x ′ , or x = x ′ and y ≤ B y ′ . This is typically employed in d-tuples of natural numbers ordered lexicographically ⟨N d , ≤ lex ⟩: observe that this is a linearisation of ⟨N d , ≤ × ⟩.

Another classical well order employed in termination proofs is the multiset order ⟨M(A), ≤ m ⟩ of [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]. There, M(A) denotes the set of finite multisets over the wo ⟨A, ≤⟩, i.e. of functions m: A → N with finitely many x in A such that m(x) > 0, and m ≤ m m ′ if and only if for all x in A, if m(x) > m ′ (x), then there exists y > A x such that m(y) < m ′ (y) [see also [START_REF] Jouannaud | On multiset orderings[END_REF].

Application: Program Termination

A first application of well-quasi-orders and well-orders is to prove program termination. The basic principle is to associate a decreasing sequence (over a wo) or a bad sequence (over a wqo) to any sequence of execution steps of the program, thereby showing that the execution must eventually terminate. This is hardly a new idea: using a ranking function into a wo was already put forth by Turing in 1949 (see Section 2.2.1). From there, it is natural to generalise to quasi-ranking functions into wqos [I3], which provide a different viewpoint on termination proofs by disjunctive termination arguments promoted by [START_REF] Podelski | Transition invariants[END_REF] (see Section 2.2.2).

We illustrate the main ideas in this section using a very simple program, given in pseudo-code in Figure 2.1a. Formally, we see the operational semantics of a

(ℓ 0 , 3, 1, 4) a -→ (ℓ 0 , 2, 1, 8)
using transition a in Figure 2.1b.

Ranking Functions.

We say that a transition system S = ⟨S, →⟩ terminates if every execution s 0 → s 1 → • • • is finite. The standard method in order to prove that a program terminates for all inputs is to exhibit a ranking function f into some well-order, such that →-related configurations have decreasing rank [START_REF] Floyd | Assigning meaning to programs[END_REF][START_REF] Turing | Checking a large routine[END_REF] 2.2.1.1. Monolithic Ranking Functions. Observe that any deterministic terminating program can be associated to a ranking function into N, which maps each configuration to the number of steps before termination. We leave it as an exercise to the reader to figure out such a ranking function for Figure 2.1-the answer can be found in Remark 3.3. There are at least two motivations for considering other wqos:

: s → s ′ must imply f (s) > f (s ′ ).
• Programs can be nondeterministic, for instance due to abstractions or interactions with an environment. Then the supremum of the number of steps along all the possible paths can be used as the range for a ranking function; this is in general a countable well-order. • Whether by automated means or by manual means, monolithic ranking functions into N are often hard to synthesise, and hard to check once found or guessed-note that the canonical 'number of steps' function is not recursive in general. This motivates employing more complex well (quasi-)orders in exchange for simpler ranking functions, as explained in the following.

2.2.1.2. Lexicographic Ranking Functions. In order to prove the termination of the program of Figure 2.1 by a ranking function, consider some (possibly infinite) execution (2.2) (ℓ 0 , x 0 , y 0 , n 0 ) → (ℓ 0 , x 1 , y 1 , n 1 ) → (ℓ 0 , x 2 , y 2 , n 2 ) → • • • over S. Because a negative value for x or y would lead to immediate termination, the associated sequence of pairs (2.3) (x 0 , y 0 ), (x 1 , y 1 ), (x 2 , y 2 ), . . . is actually over N 2 , and the successive pairs satisfy (y i , x i ) > lex (y i+1 , x i+1 ). This shows that f (ℓ 0 , x, y, n) def = (y, x) ranging over the wo ⟨N 2 , ≤ lex ⟩ is a ranking function. [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF] and Ben-Amram and Genaim [2014] consider for instance the automatic synthesis of such lexicographic affine ranking functions for integer loops like Figure 2.1a. Ranking functions into ⟨N d , ≤ lex ⟩ are described there by

d functions f 1 , f 2 , . . . , f d : S → N such that, whenever s → s ′ , then (f 1 (s), f 2 (s), . . . , f d (s)) > lex (f 1 (s ′ ), f 2 (s ′ ), . . . , f d (s ′ )); in our example f 1 (s) def
= y and f 2 (s) def = x; each function f i is an affine function of the values of the program variables. This technique is implemented in automated termination provers like FuncTion [START_REF] Courant | Precise widening operators for proving termination by abstract interpretation[END_REF] or T2 [START_REF] Brockschmidt | T2: temporal property verification[END_REF].

2.2.1.3. Ordinal Ranking Functions. Beyond ⟨N d , ≤ lex ⟩, we can consider more generally ranking functions into an ordinal [START_REF] Turing | Checking a large routine[END_REF]. For instance, write ⟨[k], ≤⟩ for the initial segment [k] def = {0, . . . , k -1} of the naturals; this is a finite linear order for each k. We can then replace our previous lexicographic ranking function for Figure 2.1 with a multiset ranking function into ⟨M( [2]), ≤ m ⟩: the ranking function f (ℓ 0 , x, y, m) def = {1 y , 0 x } associates a multiset containing y copies of the element '1' and x copies of '0' to the configuration (ℓ 0 , x, y, n).

This might seem like a rather artificial example of a multiset ranking function, and indeed more generally ⟨N d , ≤ lex ⟩ and ⟨M ([d]), ≤ m ⟩ are order-isomorphic for every d:

indeed, r(n 1 , . . . , n d ) def = {(d -1) n 1 , . . . , 0 n d } is a bijection such that (n 1 , . . . , n d ) ≤ lex (n ′ 1 , . . . , n ′ d ) in ⟨N d , ≤ lex ⟩ if and only if r(n 1 , . . . , n d ) ≤ m r(n ′ 1 , . . . , n ′ d ) in ⟨M([d]), ≤ m ⟩.
In order to pick a unique representative for each isomorphism class of well orders, one can employ their order types, presented when they fall below ε 0 as ordinal terms in Cantor normal form. Using the order type computations recalled in Appendix A.1.1.2, ω d is the order type of both ⟨N d , ≤ lex ⟩ and ⟨M ([d]), ≤ m ⟩, and our ranking function can also be defined as

f (ℓ 0 , x, y, m) def = o((y, x), ≤ lex ) = ω • y + x.

Quasi-Ranking Functions.

We introduce now a generalisation of ranking functions to work over wqos. Consider two indices i < j in a putative infinite execution like (2.3) and observe that:

• either b is never fired throughout the execution between steps i and j, and then y i = • • • = y j and x i > x j , • or b is fired at least once, and y i > y j . In both cases (x i , y i ) ̸ ≤ × (x j , y j ), i.e. the sequence (2.3) is bad for the product ordering. Since ⟨N 2 , ≤ × ⟩ is a wqo, this sequence is necessarily finite, and so is the original sequence (2.2): the program of Figure 2.1 terminates on all inputs. This termination argument for our example program easily generalises: Definition 2.1. Given a transition system S = ⟨S, →⟩, a quasi-ranking function is a map f : S → A into a wqo ⟨A, ≤⟩ such that, whenever s → + s ′ is a non-empty sequence of transitions of S, f (s) ̸ ≤ f (s ′ ).

In our treatment of the program of Figure 2.1 above, we picked f (ℓ 0 , x, y, z) def = (x, y) and ⟨A, ≤⟩ def = ⟨N 2 , ≤ × ⟩. Note that a ranking function can be seen as a quasi-ranking function into a wo ⟨A, ≤⟩. Indeed, if s → s ′ , then the condition Geser [1990, Section 3.1] and [START_REF] Podelski | Transition invariants[END_REF] show that it suffices to exhibit a finite set of well-founded relations T 1 , . . . , T d ⊆ S × S and prove that the transitive closure → + is included in the union T 1 ∪ • • • ∪ T d . This is also known as a Ramsey-based termination proof, as the original arguments relied on Ramsey's Theorem. Such termination arguments are employed in automated termination provers like Terminator [START_REF] Cook | Termination proofs for systems code[END_REF] or CProver [START_REF] Kroening | Termination analysis with compositional transition invariants[END_REF]]. An advantage of the technique over ranking functions is that synthesising the termination arguments for each T j can be easier than finding a global ranking function over S; a disadvantage is that checking the inclusion

f (s) ̸ ≤ f (s ′ ) of Definition 2.
→ + ⊆ T 1 ∪ • • • ∪ T d ,
which is typically encoded as an assertion passed to a safety checker, can be costly.

In practice, we can assume each of the T j for 1 ≤ j ≤ d to be proved wellfounded through a quasi-ranking function f j into a wqo ⟨A j , ≤ j ⟩. In the case of the program in Figure 2.1, choosing

T 1 def = {((ℓ 0 , x, y, n), (ℓ 0 , x ′ , y ′ , n ′ )) | x > 0 ∧ x ′ < x} (2.4) T 2 def = {((ℓ 0 , x, y, n), (ℓ 0 , x ′ , y ′ , n ′ )) | y > 0 ∧ y ′ < y} (2.5) yields such a disjunctive termination argument, with A 1 = A 2 = N.
Another way of understanding disjunctive termination arguments is that they define a quasi-ranking function f into the product wqo ⟨A 1 ו • •×A d , ≤ × ⟩, which maps a configuration s to the tuple ⟨f 1 (s), . . . , f d (s)⟩, c.f. [C19, Section 7.1].

Application: Well-Structured Transition Systems

Well-structured transition systems (WSTS) form a family of computational models where the (usually infinite) set of configurations is equipped with a wellquasi-ordering that is 'compatible' with the computation steps. The existence of this well-quasi-ordering allows for the decidability of some important behavioural properties like termination (from a given initial configuration) or coverability.

Historically, the idea can be traced back to [START_REF] Finkel | A generalization of the procedure of Karp and Miller to well structured transition systems[END_REF] who gave a first definition for WSTS abstracting from Petri nets and fifo nets, and who showed the decidability of termination from an initial configuration and of finiteness of the set of reachable configurations (aka boundedness). Then [START_REF] Finkel | Decidability of the termination problem for completely specificied protocols[END_REF] applied the WSTS idea to decide termination from a given initial configuration in lossy channel systems, while [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF] introduced the backward-chaining algorithm for coverability. One will find a good survey of these early results, and a score of WSTS examples, in [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF][START_REF] Abdulla | Well (and better) quasi-ordered transition systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]Finkel and Goubault-Larrecq, 2012b]. Many new WSTS models have been introduced since (in distributed computing, software verification, logic, and other fields), using well-quasi-orderings based on trees, sequences of vectors, or graphs, rather than the more traditional vectors of natural numbers or words with the subword embedding.

Formal Definition.

A transition system S = ⟨S, →⟩ is ordered when it is further equipped with a quasi-ordering ≤ of its configurations. An ordered transition system S = ⟨S, →, ≤⟩ is well-structured if ⟨S, ≤⟩ is a wqo and (2.6)

∀s 1 , s 2 , t 1 ∈ S, ( s 1 → s 2 and s 1 ≤ t 1 ) implies ∃t 2 ∈ S, ( t 1 → t 2 and s 2 ≤ t 2 ) .
This last property is also called 'compatibility' (of the ordering with the transitions). Formally, it just means that ≤ is a simulation relation for S, in precisely the classical sense of [START_REF] Milner | Operational and algebraic semantics of concurrent processes[END_REF]. The point of (2.6) is to ensure that a larger configuration can do at least as much as a smaller configuration.

Remark 2.3. Equation (2.6) comes in many variants. For example, [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] consider strict compatibility (when <, the strict ordering underlying ≤, is a simulation), transitive compatibility (when ≤ is a weak simulation), and the definition can further extend to labelled transition systems. These are all inessential variations of the main idea.

Example: Lossy Counter Machines.

Let us consider lossy counter machines (LCM) [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF] as an example of a family of WSTSs. Such counter machines are syntactically identical to Minsky machines ⟨Q, C, δ, q 0 ⟩, where the transitions in δ ⊆ Q × C × {=0?, ++, --} × Q operate on a finite set C of counters through zero-tests c=0?, increments c++ and decrements c--. The semantics of an LCM differ however from the usual, 'reliable' semantics of a counter machine in that the counter values can decrease in an uncontrolled manner at any point of the execution. These unreliable behaviours make several problems decidable on LCMs, contrasting with the situation with Minsky machines [Schnoebelen, 2010b], the intuition being that, in order to compute anything, LCMs must introduce considerable redundancy and robustness to losses, which makes their analysis possible. These positive decidability results should however be taken with a grain of salt: as we will see in Section 4.2, LCMs and related models like reset Petri nets are the main source of decision problems with provably Ackermannian complexity [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF][Schnoebelen, , 2010a;;[START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF].

Formally, a configuration q, v associates a control location q in Q with a counter valuation v in N C , i.e. counter values can never go negative. Observe that the set of configurations Q × N C is well-quasi-ordered by the product ordering: q, v ≤ q ′ , v ′ if and only if q = q ′ and v(c) ≤ v ′ (c) for all c ∈ C. Let the initial configuration be q 0 , 0. A transition of the form (q, c, op, q ′ ) defines a reliable computation step q, v → q ′ , v ′ , where v(c

′ ) = v ′ (c ′ ) for all c ̸ = c ′ in C and • if op = =0?, then v(c) = v ′ (c) = 0, • if op = ++, then v(c) + 1 = v ′ (c), and • if op = --, then v(c) = v ′ (c) + 1.
A lossy computation step is then defined by allowing counter values to decrease arbitrarily between reliable steps: (q, v) → ℓ (q ′ , v ′ ) if and only if there exist w ≤ v and w ′ ≥ v ′ such that (q, w) → (q ′ , w ′ ). Now, lossy steps are visibly compatible with ≤ according to (2.6), and thus the transition system ⟨Q×N C , → ℓ , ≤⟩ defined by the lossy operational semantics is a WSTS. Example 2.4 (Weak Inverse of Figure 2.1). Figure 2.2b displays a counter machine with counters C def = {x, y, n, n ′ }. Figure 2.2a shows the pseudo-code for the computation performed by the machine, where an auxiliary counter n ′ is used to perform division by two. If started in configuration (ℓ 0 , 0, 0, N, 0) and assuming reliable semantics, then this machine enumerates, each time it reaches the state ℓ 0 with n ′ empty, the values of x, y, n such that the program of Figure 2.1 terminates on input x, y, n and returns N . With lossy semantics, it might also reach smaller values of x, y, n; as will be recalled more formally in Section 4.2, the LCM of Figure 2.2b is a weak computer for the function defined by Figure 2.1.

Verifying WSTS.

A number of decision problems can be solved in WSTS using generic algorithms relying on the underlying wqo for termination and on variants of compatibility (2.6) for correctness, including termination (from a given initial configuration), inevitability, boundedness, regular simulations, etc.

2.3.3.1. Coverability. We focus here on the coverability problem.

Problem (Coverability).

instance: An ordered transition system ⟨S, →, ≤⟩ and two configurations s, t in S. question: Is t coverable from s, i.e. is there a run s = s 0 → * s n ≥ t?

This problem corresponds to the verification of safety properties, i.e. that no bad configuration can ever be reached: here t models an error configuration, and we assume that any configuration larger than t is also an error.

In the particular case of a WSTS over configuration space Q × A for some finite set of control configurations Q and some wqo domain ⟨A, ≤ A ⟩, controlstate reachability asks whether some state q can be reached, regardless of the associated element of A. This immediately reduces to coverability of the finitely many minimal elements of {q} × A for the product ordering over Q × A, i.e. (q, x) ≤ × (q ′ , x ′ ) if and only if q = q ′ and x ≤ A x ′ .

2.3.3.2. Backward Coverability. The decidability of WSTS Coverability uses a set-saturation method, whose termination relies on the Ascending Chain Condition mentioned in §2. 1.1.1. This (↑t) in order to answer the coverability instance. This idea is also at the heart of the algorithms for many other properties defined by fixpoints, see [START_REF] Bertrand | Computable fixpoints in well-structured symbolic model checking[END_REF]. The first known published instance of backward coverability seems to be due to [START_REF] Arnold | Récursivité et cones rationnels fermés par intersection[END_REF] for reset Petri nets, but the algorithm was independently rediscovered by [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF] for lossy channel systems and its abstract formulation was popularised in the surveys [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

For a set of configurations U ⊆ S, define its (existential) predecessor set as

(2.8) Pre ∃ (U ) def = {s ∈ S | ∃s ′ ∈ U, s → s ′ } .
The backward coverability algorithm computes the limit of the sequence

↑t = U 0 ⊆ U 1 ⊆ • • • where U n+1 def = U n ∪ Pre ∃ (U n ) (2.9) where U n = {s ′ ∈ S | ∃t ′ ≥ t, s ′ → ≤n t ′ }
is the set of configurations that cover t in at most n steps.

Termination and Effectiveness of the Algorithm.

There is no reason for the chain in (2.9) to converge in general, but it does in the case of a WSTS. Lemma 2.5. If U ⊆ S is an upwards-closed set of configurations, then Pre ∃ (U ) is upwards-closed.

Proof. Assume s ∈ Pre ∃ (U ). Then s → t for some t ∈ U . By (2.6), if s ′ ≥ s, then s ′ → t ′ for some t ′ ≥ t. Thus t ′ ∈ U and s ′ ∈ Pre ∃ (U ). □
A corollary is that sequence (2.9) stabilises to ∪ i∈N U i = Pre * ∃ (↑t) after a finite amount of time thanks to the Ascending Chain Condition.

Moreover, as seen in §2.1.1.2, the Finite Basis Property ensures that all the sets U i can be finitely represented using their minimal elements, and the union or inclusion of two upwards-closed sets can be computed. The last ingredient is an effectiveness assumption:

• ⟨S, ≤⟩ should be effective, meaning that S is recursive and the ordering ≤ is decidable, and • there exists an algorithm accepting any configuration s ∈ S and returning pb(s), a finite basis for Pre ∃ (↑s); this is known as the effective pred-basis assumption.

Remark 2.6 (Coverability Pseudo-Witnesses). For future reference, it is worth detailing again the argument for the Ascending Chain Condition in the particular setting of backward coverability: we can extract a sequence of minimal elements

t 0 , t 1 , . . . from U 0 ⊊ U 1 ⊊ • • • such that t 0 def = t and t i+1 ∈ U i+1 \ U i for all i,
which entails that the sequence t 0 , t 1 , . . . is bad and therefore finite.

In fact, we can be more precise, and pick t i+1 at each step among the minimal elements of Pre ∃ (↑t i ). Indeed, we can picture the computation in (2.9) as a tree rooted in t, where each node t ′ has an edge to each minimal element of Pre ∃ (↑t ′ ): for each level i of this tree, the upward closure of the set of nodes at levels at most i is exactly U i . The tree is finitely branching by the Finite Basis Property, and finite depth since every branch is a bad sequence, hence is finite by Kőnig's Lemma, and its height is exactly the number of steps before termination of the backward coverability algorithm. We call such a bad sequence t 0 , t 1 , . . . , t n with

t 0 def = t , t i+1 ∈ min Pre ∃ (↑t i ) , t n ≤ s (2.10)
a pseudo-witness of the coverability of t from s.

Example 2.7 (Predecessors in Lossy Counter Machines). The previous two effectiveness assumptions hold in all the 'natural' families of WSTS. In the case of LCMs, ⟨Q × N C , ≤⟩ is certainly effective, and a finite basis of predecessors of a configuration q ′ , v ′ can be computed by

pb(q ′ , v ′ ) = min{q, pre c op (v ′ ) | (q, c, op, q ′ ) ∈ δ and v ′ (c) = 0 if op = =0?} where pre c op (v ′ ) is a vector in N C with pre c op (v ′ )(c ′ ) def = v ′ (c ′ ) for all c ′ ̸ = c in C, and pre c=0? (v ′ )(c) def = v ′ (c) = 0 , pre c++ (v ′ )(c) def = max{0, v ′ (c) -1} , pre c--(v ′ )(c) def = v ′ (c) + 1 .
Example 2.8 (Weak Inverse Computer and Coverability). Let us consider once more Example 2.4 and Figure 2.2b with initial configuration s def = (ℓ 0 , 0, 0, N, 0). Because it is a weak computer for inversing the program of Figure 2.1, the configuration t def = (ℓ 0 , x, y, n, 0) can be covered if and only if the program of Figure 2.1 would have returned at least N when started with x, y, n as inputs. Now, the backward coverability algorithm with t as target is essentially simulating an execution of the program on input x, y, n, and will require at least as many steps as it took the program to terminate.

CHAPTER 3

Length Function Theorems

This chapter presents some contributions to the complexity analysis of wqobased termination arguments published jointly with Figueira,Figueira,and Schnoebelen [C19;[START_REF] Schmitz | Multiply-recursive upper bounds with Higman's Lemma[END_REF][START_REF] Schmitz | Complexity bounds for ordinal-based termination[END_REF]. We aim to extract complexity upper bounds on the running time of algorithms from their termination proof.

It turns out that, by suitably controlling how 'large' the elements can grow in bad sequences (see Section 3.1), we can derive upper bounds on the time and space required by the algorithms presented in Sections 2.2 and 2.3. I present two length function theorems, which are combinatorial statements on the length of controlled bad sequences: one for sequences of ordinals below ε 0 in Section 3.3 and one for tuples of natural numbers in Section 3.4, and how to apply them to the examples from Chapter 2.

A major drawback of all these complexity bounds is that they are very highi.e., non-elementary except in trivial cases-, whereas practitioners are mostly interested in polynomial bounds. This is the price to pay for the generality of the approach: the class of programs terminating thanks to a quasi-ranking function encompasses programs of high complexity.

Example 3.1. For instance, simple integer loops can already be deceivingly simple: recall that the program of Figure 2.1 terminated using a straightforward ranking function into ω 2 . Although this is just one notch above a ranking function into ω, we can already witness fairly complex computations. Observe indeed that the following steps can be executed in our program:

(ℓ 0 , x, y, 1) a x b --→ (ℓ 0 , 2 x , y -1, 2 x+1 ) a 2 x b ---→ (ℓ 0 , 2 2 x +x+1 , y -2, 2 2 x +x+2 ) a 2 2 x +x+1 b ------→ (ℓ 0 , 2 2 2 x +x+1 +2 x +x+2 , y -3, 2 2 2 x +x+1 +2 x +x+3 ) .
Continuing this execution, we see that our simple program exhibits executions of length greater than a tower of exponentials in y, i.e. it is non-elementary. As shown by Example 2.8, this non-elementary lower bound also applies to the number of steps required by the backward coverability algorithm to terminate on the LCM of Figure 2.2b with target configuration (ℓ 0 , x, y, 1, 0). Such high complexities justify the use of ordinal-indexed subrecursive functions in order to denote non-elementary growths. We will recall the definitions of two families of such functions in Section 3.2.

The presentation in this chapter is based chiefly on the lecture notes [L1]

Controlling Bad Sequences

Both in the case of quasi-ranking functions of Section 2.2.2 and in that of the backward coverability algorithm of Section 2.3.3, the running time of the algorithm is essentially bounded by the length of the bad sequences constructed by the termination argument. By definition, bad sequences in a wqo are always finite, but no statement is made regarding how long they can be. This is for a very good reason: they can be arbitrarily long.

For instance, over the wo ⟨N, ≤⟩,

(3.1) n, n -1, . . . , 1
, 0 is a bad sequence of length n + 1 for every n. Arguably, this is not so much of an issue, since what we are really interested in is the length as a function of the initial configuration-which includes the inputs to the program. Thus (3.1) is the maximal bad sequence over ⟨N, ≤⟩ with initial element of 'size n. ' However, as soon as we move to more complex wqos, we can exhibit arbitrary bad sequence lengths even with fixed initial configurations. For instance, over

⟨N 2 , ≤ lex ⟩, (3.2)
(1, 0), (0, n), (0, n -1), . . . , (0, 1), (0, 0) is a bad sequence of length n + 2 for every n starting from the fixed (1, 0). Nonetheless, the behaviour of a program exhibiting such a sequence of ranks is rather unusual: such a sudden 'jump' from (1,0) to an arbitrary (0, n) is not possible in a deterministic program once the user inputs have been provided.

In the following, we will assume that no such arbitrary jump can occur. This comes at the price of some loss of generality in the context of termination analysis, where nondeterministic assignments of arbitrary values are typically employed to model values provided by the environment-for instance interactive user inputs or concurrently running programs-, or because of abstracted operations. Thankfully, in most cases it is easy to control how large the program variables can grow during the course of an execution.

Normed wqos. Given a wqo ⟨A, ≤ A ⟩, we posit a norm function |.|

A from A to N on the elements of A. In order to be able to derive combinatorial statements, we require

(3.3) A ≤n def = {x ∈ A | |x| A ≤ n} to be finite for every n. We call the resulting structure ⟨A, ≤ A , | • | A ⟩ a normed wqo (nqo).
We will use the following norms on some of the wqos defined earlier:

• in a finite Q, all the elements have the same norm 0;

• in N or [d], n has norm |n| N = n; • in disjoint sums A 0 ⊔ A 1 , (x, i) uses the norm |x| A i of the underlying set; • in Cartesian or lexicographic products with support A × B, (x, y) has the infinity norm max(|x| A , |y| B ); finally, • in multisets M(A), m has norm max x∈A,m(x)>0 (max(m(x), |x| A )).
Regarding ordinals, recall that ε 0 is the smallest fixed point of the equation ω x = x, and consider some γ < ε 0 . We define the norm of an ordinal α < γ as the maximal coefficient that appears in its associated Cantor normal form: if

α = ω α 1 • c 1 + • • • + ω αp • c p < γ with α 1 > • • • > α p and c 1 , . . . , c p > 0, then (3.4) N α def = max{c 1 , . . . , c p , N α 1 , . . . , N α p } .
Observe that this definition essentially matches the previously defined norms over multisets and tuples of vectors: in ⟨N d , ≤ lex ⟩, we have

N o((n 1 , . . . , n d ), ≤ lex ) = N (ω d-1 • n 1 + • • • + ω 0 • n d ) = max(d -1, |(n 1 , . . . , n d )| N d ) , and in ⟨M(N d ), ≤ m ⟩ for multisets of lexicographically-ordered tuples, N o(m, ≤ m ) = max(d -1, |m| M(N d ) ) .

Controlled Sequences.

Let g: N → N be a monotone and inflationary function: for all x, x ′ , x ≤ x ′ implies g(x) ≤ g(x ′ ) and x ≤ g(x). Definition 3.2 (Controlled Sequence; [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF]. We say that a sequence

x 0 , x 1 , x 2 , . . . of elements in A is amortised controlled by (g, n 0 ) for some n 0 in N if (3.5) |x i | A ≤ g i (n 0
) for all i, where g i denotes the ith iterate of g. We say that it is strongly controlled by (g, n 0 ) for some n 0 in N if

(3.6) |x 0 | A ≤ n 0 and |x i+1 | A ≤ g(|x i |) A for all i.
Observe that by definition a strongly controlled sequence is also amortised controlled: |x 0 | A ≤ g 0 (n 0 ) = n 0 , which prompts the name of initial norm for n 0 , and amortised steps cannot grow faster than g the control function. In the following we simply write '(g, n 0 )-controlled' instead of 'amortised controlled by (g, n 0 )'.

3. The notion of control can be lifted to the level of the quasi-ranking functions that generate them. Let us posit a configuration norm ι: S → N. Then a quasi-ranking function f : S → A for a transition system S = ⟨S, →⟩ and a normed wqo

⟨A, ≤ A , |.| A ⟩ is (g, ι)-controlled if, for any execution s 0 → s 1 → • • • of S, for all i, (3.7) |f (s i )| A ≤ g i (ι(s 0 )) .
This ensures that any sequence f (s 0 ), f (s 1 ), . . . of ranks associated to the execution is (g, ι(s 0 ))-controlled.

For instance, our ranking function

f (ℓ 0 , x, y, n) def = (y, x) for the program of Figure 2.1 into ⟨N 2 , ≤ lex ⟩ is g-controlled for g(x) def = 2x and ι(ℓ 0 , x, y, n) def = max(x, y, n).
Observe that having a configuration norm ι(s 0 ) rather than simply using the norm of the initial rank |f (s 0 )| A gives us some extra flexibility: in our example, the latter equals max(x, y), and the sequences of ranks f (s 0 ), f (s 1 ), . . . are in general not (g, |f (s 0 )| A )-controlled because the value of n has been lost.

Example: Controlled Minimal Predecessors.

Let us see how this setting applies to the backward coverability algorithm of §2.3.3.2. In order to control the bad sequence of configurations extracted from the Ascending Chain Condition applied to (2.9), observe that the initial norm n 0 can be taken as |t| S . Regarding the control function g, the ith iterate g i (n 0 ) of control function should then bound the norm of the minimal elements of U i .

In the case of lossy counter machines, the computation of minimal predecessors in Example 2.7 shows that a strong control by H(x) def = x + 1 suffices.

Length Functions.

The point of controlled sequences is that their length can be bounded. Consider for this the tree one obtains by sharing the common prefixes of all the (g, n 0 )-controlled bad sequences over a normed wqo ⟨A, ≤ A , |.| A ⟩. This tree has

• finite branching by (3.3) and (3.5), more precisely of branching degree bounded by the cardinal of A ≤g i (n 0 ) for a node at depth i, and • no infinite branches thanks to the wqo property. By Kőnig's Lemma, this tree of bad sequences is therefore finite, of some height L g,n 0 ,A representing the length of the maximal (g, n 0 )-controlled bad sequence(s) over A. In the following, since we are mostly interested in this length as a function of the initial norm n 0 , we will see this as a length function L g,A (n 0 ).

Observe that L g,A bounds the asymptotic execution length in a program endowed with a g-controlled quasi-ranking function into ⟨A, ≤ A , |.| A ⟩. It similarly bounds the number of steps required by the backward coverability algorithm for a WSTS over ⟨A, ≤ A , |.| A ⟩ with a target configuration of norm |t| A ≤ n 0 when minimal elements in U i are of norm at most g i (n 0 ).

Our purpose will thus be to obtain explicit complexity bounds on L g,A depending on g and A. We call such combinatorial statements length function theorems. But first we need to make a detour via subrecursive functions, which we employ in order to express those explicit upper bounds.

Subrecursive Hierarchies

As we saw with the example of Figure 2.1, even simple terminating programs can have a very high complexity. In order to express such high bounds, a convenient tool is found in subrecursive hierarchies, which employ induction over ordinal indices to define faster and faster growing functions. We recall the definition of two such hierarchies [see e.g. [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF][START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF][START_REF] Schwichtenberg | Proofs and Computation[END_REF][START_REF] Wainer | Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy[END_REF]. We shall strive to employ notations compatible with those of Schwichtenberg and Wainer [2012, Chapter 4], and refer the interested reader to their monograph for proofs and additional material.

Fundamental Sequences and Predecessors.

Let us first introduce some notions on ordinal terms. Consider an ordinal term α in Cantor normal form ω α1 + • • • + ω αp . In this representation, α = 0 if and only if p = 0. An ordinal α of the form α ′ + 1 (i.e. with p > 0 and α p = 0) is called a successor ordinal, and otherwise if α > 0 it is called a limit ordinal, and can be written as γ + ω β by setting γ = ω α 1 + • • • + ω α p-1 and β = α p . We usually write 'λ' to denote a limit ordinal.

A fundamental sequence for a limit ordinal λ is a sequence (λ(x)) x<ω of ordinal terms with supremum λ. We use the standard assignment of fundamental sequences to limit ordinals in Cantor normal form, defined inductively by

(γ + ω β+1 )(x) def = γ + ω β • (x + 1) , (γ + ω λ )(x) def = γ + ω λ(x) . (3.8)
This particular assignment satisfies e.g. 0 < λ(x) < λ(y) for all x < y. For instance, ω( x+1) . We also define a fundamental sequence for ε 0 itself, so that we may be able to use it in our hierarchies:

x) = x + 1, (ω ω 4 + ω ω 3 +ω 2 )(x) = ω ω 4 + ω ω 3 +ω•(
ε 0 (0) def = ω and ε 0 (i + 1) def = ω ε 0 (i) , so that ε 0 (i) is a tower of ω's of height i + 1.
The predecessor P x (α) of an ordinal term α > 0 at a value x in N is defined inductively by

P x (α + 1) def = α , P x (λ) def = P x (λ(x)) . (3.9)
In essence, the predecessor of an ordinal is obtained by repeatedly taking the xth element in the fundamental sequence of limit ordinals, until we finally reach a successor ordinal and remove 1. For instance,

P x (ω 2 ) = P x (ω • (x + 1)) = P x (ω • x + x + 1) = ω • x + x.

Hardy and Cichoń Hierarchies.

In the context of controlled sequences, the hierarchies of Hardy and Cichoń turn out to be especially well-suited [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF]]. Let h: N → N be a function. The Hardy hierarchy (h α ) α∈ε 0 is defined for all 0 < α < ε 0 by 1

h 0 (x) def = x , h α (x) def = h Px(α) (h(x)) , (3.10)
and the Cichoń hierarchy (h α ) α∈ε 0 is similarly defined for all 0 < α < ε 0 by

h 0 (x) def = 0 , h α (x) def = 1 + h Px(α) (h(x)) . (3.11)
Observe that h k for some finite k is the kth iterate of h. This intuition carries over: h α is a transfinite iteration of the function h, using diagonalisation in the fundamental sequences to handle limit ordinals.

We should emphasise that h α and h α are defined for any function h; thus later we will see g α meaning 'the αth Cichoń function based on g. ' This provides quite some flexibility, but one standard choice for the initial function is the successor function, noted H(x) def = x + 1. In that case, we see that a first diagonalisation yields

H ω (x) = H x (x + 1) = 2x + 1. The next diagonalisation occurs at H ω•2 (x) = H ω+x (x + 1) = H ω (2x + 1) = 4x + 3.
Fast-forwarding a bit, we get for instance a function of exponential growth H ω 2 (x) = 2 x+1 (x + 1) -1, and later a non-elementary function H ω 3 (x) akin to a tower of exponentials of height x, an 'Ackermannian' non primitive-recursive function H ω ω , and a 'hyper-Ackermannian' non multiply recursive-function H ω ω ω .

The Hardy functions also enjoy some nice identities: for all h, α, β, and [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF][START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF]]; this will always be the case in our applications of these identities.

x h α • h β (x) = h α+β (x) , (h α ) β (x) = h α•β (x) , (3.12) provided α + β (resp. α • β) satisfies specific conditions like being tree-structured [see, e.g.,
Regarding the Cichoń functions, an induction on α shows that H α (x) = H α (x) + x. More generally, if h is strictly inflationary, i.e. if h(x) > x for all x, then (3.13)

h α (x) ≥ h α (x) + x .
Remark 3.3 (Measuring Control and Length). On the one hand, Hardy functions are well-suited for expressing large iterates of a control function, and therefore for bounding the norms of elements in a controlled sequence. For instance, the program in Figure 2.1 computes g ω•y+x (n) for the function g(x) def = 2x when run on non-negative inputs x, y, n. Note that g x (n) = 2 x n and g ω•y (n) is greater than a tower of exponentials of height y.

On the other hand, Cichoń functions are well-suited for expressing the length of controlled sequences. For instance, g ω•y+x (n) is the length of the execution of the program. This relation is a general one: we can compute how many times we should iterate h in order to compute h α (x) using the corresponding Cichoń function [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF]]:

(3.14) h α (x) = h hα(x) (x) .

Length Functions for Ordinals Below ε 0

Our first length function theorem, which was proven in [I3], relies on two main ingredients: a descent equation established in [C18] for all normed wqos, and an alternative characterisation of the Cichoń hierarchy in terms of maximisations as observed in [START_REF] Buchholz | A uniform approach to fundamental sequences and hierarchies[END_REF][START_REF] Cichoń | Termination orderings and complexity characterisations[END_REF].

Residuals and a Descent Equation.

Let ⟨A, ≤, |.| A ⟩ be a normed wqo and x be an element of A. We write

(3.15) A/x def = {y ∈ A | x ̸ ≤ y} for the residual of A in x.
Observe that by the wqo property, there cannot be infinite sequences of residuations A/x 0 /x 1 /x 2 / • • • because x i ̸ ≤ x j for all i < j.

Consider now a (g, n)-controlled bad sequence x 0 , x 1 , x 2 , . . . over A. Assuming the sequence is not empty, then because this is a bad sequence we see that for all i > 0, x 0 ̸ ≤ x i , i.e. that the suffix x 1 , x 2 , . . . is actually a bad sequence over A/x 0 . This suffix is now (g, g(n))-controlled, and thus of length bounded by L g,A/x 0 (g(n)). This yields the following descent equation when considering all the possible (g, n)-controlled bad sequences [C18]:

(3.16) L g,A (n) = max x∈A ≤n 1 + L g,A/x (g(n)) .
In the case of a wo ⟨α, ≤, N ⟩, residuals can be expressed more simply for

β ∈ α, because α/β = {γ ∈ α | β > γ} = β . (3.17)
Thus in this case the descent equation simplifies into

L g,α (n) = max β<α,N β≤n 1 + L g,β (g(n)) . (3.18)

Upper Bounds.

We are now equipped to prove a length function theorem for all ordinals α below ε 0 , i.e. an explicit expression for L g,α for the wo ⟨α, ≤, N ⟩. The reader might have noticed a resemblance between the ordinal descent equation (3.18) and the definition of the Cichoń hierarchy (3.11). It turns out that they are essentially the same functions: indeed, we are going to see in Proposition 3.4 that a fundamental insight of [START_REF] Cichoń | Termination orderings and complexity characterisations[END_REF] and [START_REF] Buchholz | A uniform approach to fundamental sequences and hierarchies[END_REF] applies perfectly to our particular setting: if N α ≤ x, then choosing

β = P x (α) maximises h β (h(x)) among those β < α with N β ≤ x. Proposition 3.4 (I3). Let α < ε 0 and x ≥ N α. Then h α (x) = max β<α,N β≤x 1 + h β (h(x)) .
Theorem 3.5 (Length Function Theorem for Ordinals). Let α < ε 0 and x ≥ N α. Then L g,α (x) = g α (x).

Proof. We use the ordinal descent equation (3.18) and Proposition 3.4. □

As an immediate corollary, we can bound the asymptotic complexity of programs proven to terminate through a (g, ι)-controlled ranking function:

Corollary 3.6. Given a transition system S = ⟨S, →⟩ with initial configuration s 0 , if there exists a (g, ι)-controlled ranking function into α < ε 0 , then S runs in time O(g α (ι(s 0 ))).

Example 3.7 (Lexicographic Ranking Functions). As an illustration, a program proven to terminate thanks to a (g, ι)-controlled ranking function ranging over ⟨N d , ≤ lex , |.| N d ⟩ has therefore an O(g ω d (n)) bound on its worst-case asymptotic time complexity for n = ι(s 0 ).

In the case of the program of Figure 2.1, Corollary 3.6 yields an upper bound on its time complexity in y, n). This is very close to its actual complexity, which is exactly g ω•y+x (n). Regarding its space complexity, by (3.14) it is in

O(g ω 2 (m)) = O(g ω•m+m (m)), where g(x) def = 2x and m = ι(ℓ 0 , x, y, n) def = max(x,
O(log(g ω 2 (m))).
Remark 3.8 (Abstractions). The bound g ω d (n) provided by Corollary 3.6 in the case of lexicographic ranking functions into N d is primitive-recursive (in the control function g). This might be taken to imply that non-primitive recursive programs are beyond the reach of the current automated termination methods, which usually rely on the synthesis of affine ranking functions. This is not the case, as for instance the Ackermann function is correctly analysed as terminating by termination checkers. We can better understand this apparent paradox with the example of size-change termination proofs: Lee, Jones, and Ben-Amram [2001] They construct a size-change graph on two variables to prove its termination. The longest decreasing sequence in such a graph is of length O(n 2 ); more generally, [START_REF] Colcombet | Size-change abstraction and max-plus automata[END_REF] showed that the asymptotic worst-case complexity in a size-change graph is Θ(n r ) for a computable rational r. Here we witness a large gap between the actual program complexity and the complexity derived from its termination argument: the Ackermann function vs. an O(n 2 ) bound.

The source of this apparent paradox is abstraction: the size-change graph for a(m, k) terminates if and only if the original program does, but the time complexity is not preserved by this abstraction. In the example of the Ackermann function, the call stack is abstracted away, whereas we should include it in order for Theorem 3.5 to apply. This is done by Dershowitz and Manna [1979, Example 3], who prove the termination of the Ackermann function by exhibiting an H-controlled ranking function into ⟨M(N 2 ), ≤ m ⟩, for which Theorem 3.5 yields an O(H ω ω 2 (max(m, k))) complexity upper bound-where a more accurate bound would be O(H ω m (k)). More generally, Ben-Amram [2002] showed that the programs that can be proven to terminate by size change abstraction are multiply recursive in the complexity of the basic operations.

Length Functions for Dickson's Lemma

Our second length function theorem pertains to the length of bad sequences over ⟨N d , ≤ × ⟩, which is relevant to both the disjunctive termination arguments from §2.2.2.2 and coverability in LCMs as seen in Example 2.7.

The starting point for the analysis is again the descent equation (3.16). However, we are no longer in the comfortable situation of ordinals, where we could work with the residual α/β directly as the ordinal β. In the case of N d , it is not immediately clear how to analyse the length L g,N d /(n 1 ,...,n d ) (g(n)) of controlled bad sequences in the residual of N d by a tuple (n 1 , . . . , n d ).

The key idea introduced in [C19] is to 'over-approximate' N d /(n 1 , . . . , n d ) as a disjoint sum of tuples of lower dimension. Thus, instead of working just with tuples in N d , we shall consider more generally polynomial nwqos, where disjoint sums are also allowed (see Section 3.4.1). Then, the notion of 'over-approximation' of residuals of polynomial nwqos is captured formally by showing the existence of a normed reflection into another polynomial nwqo (see Section 3.4.2). The final step lifts this analysis to ordinals through the maximal order types of polynomial nwqos, allowing to relate L g,N d (n) with functions in the Cichoń hierarchy (see Section 3.4.3). We follow the presentation from [C18], where the arguments were cleaned-up and generalised to obtain a length function theorem for Higman's Lemma.

Polynomial Normed wqos.

We shall use the empty nwqo 0 def = ∅, and a singleton nwqo 1 with equality and constant norm 0. The exact element found in this singleton is actually irrelevant; it could be for instance a letter in an alphabet, or a configuration in a finite configuration set. Definition 3.9. The set of polynomial nwqos is the smallest set of normed wqos containing 0, 1, and N and closed under the ⊔ and × operations.

We shall work up to isomorphism: we write A ≡ B when the two nwqos A and B are isomorphic structures. Let us stress that, in particular, norm functions must be preserved by nwqo isomorphisms. For all practical purposes, isomorphic nwqos can be identified; in particular, the length functions L g,A and L g,B are the same for isomorphic nwqos. Observe that the definitions are such that all the expected identities of ⊔ and × hold up to isomorphism: the class of all normed wqos when considered up to isomorphism forms a commutative semiring with 0 as zero and 1 as one.

We write A • k for k times

A ⊔ • • • ⊔ A; then, any finite normed wqo with k elements equipped with equality is isomorphic to 1 • k; also, A • 0 ≡ 0 is the empty normed wqo.

We also write A d for

d times A × • • • × A the d-fold
Cartesian product of a normed wqo A with itself; in particular A 0 ≡ 1 is a singleton set containing only the empty tuple '()'. Remark 3.10 (Polynomial Normal Form). Any polynomial normed wqo A can be put in a polynomial normal form (PNF)

(3.19) A ≡ N d 1 ⊔ • • • ⊔ N dm for m, d 1 , • • • , d m ≥ 0.
In the following we will deal exclusively with normed wqos in PNF; since A ≡ A ′ implies L g,A = L g,A ′ this will be at no loss of generality.

Example 3.11 (LCMs Configurations). The set of configurations Q × N C of an LCM with |Q| = p control states and |C| = d counters, along with its ordering and infinity norm, is isomorphic to the polynomial nwqo N d • p in PNF.

Reflecting Normed wqos.

We may now tackle our main problem: computing residuals A/x. The descent equation (3.16), though it offers a way of computing the length function, quickly leads to complex expressions: the nwqos A/x 0 /x 1 / • • • /x n become 'unstructured', i.e. have no nice definition in terms of ⊔ and ×. As we are going to see, residuation allows us to approximate these sets, so that the computation can be carried out without leaving the realm of polynomial nwqos, leading to an inductive computation of A/x over the structure of the polynomial nwqo A. Definition 3.12. A nwqo reflection is a mapping r: A → B between two nwqos that satisfies the two following properties:

∀x, x ′ ∈ A : r(x) ≤ B r(x ′ ) implies x ≤ A x ′ , (3.20) ∀x ∈ A : |r(x)| B ≤ |x| A . (3.21)
In other words, a nwqo reflection is an order reflection that is not norm-increasing.

We write r: A → B when r is a nwqo reflection and say that B reflects A. This induces a quasi-ordering between nwqos, written A → B. Any nwqo reflects its induced substructures since Id: X → A when X is a substructure of A. Thus 0 → A for any A, and 1 → A for any non-empty A. Remark that reflections are compatible with products and sums:

A → A ′ and B → B ′ imply A ⊔ B → A ′ ⊔ B ′ and A × B → A ′ × B ′ . (3.22)
Crucially, reflections preserve controlled bad sequences. Indeed, let r: A → B, and consider a sequence x 0 , x 1 , . . . over A. Then by (3.20), r(x 0 ), r(x 1 ), . . . is bad when x 0 , x 1 , . . . is, and by (3.21), it is (g, n)-controlled when x 0 , x 1 , . . . is. Hence

(3.23) A → B implies L g,A (n) ≤ L g,B (n) for all g, n .
3.4.2.1. Inductive Reflection of Residuals. The base cases of the inductive reflection of A/x over the structure of the polynomial nwqo A are

N 0 /() → 0 , (3.24) N/k → N 0 • k , (3.25) because N/k = [k] by the ordinal descent equation (3.18), and then [k] → N 0 • k. Regarding disjoint sums A ⊔ B, it is plain that (3.26) (A ⊔ B)/(x, A) = (A/x) ⊔ B , (A ⊔ B)/(y, B) = A ⊔ (B/y) ,
and reflections are not required.

Turning to Cartesian products, the key insight is that any element

(x ′ , y ′ ) in (A × B)/(x, y) is by definition (3.15) such that (x, y) ̸ ≤ × (x ′ , y ′ ), hence x ̸ ≤ A x ′ or y ̸ ≤ B y ′ : (3.27) (A × B)/(x, y) → ( (A/x) × B ) ⊔ ( A × (B/y) ) .
3.4.2.2. Derivation Relation. We finally combine the inductive residuation and reflection operations into a derivation relation ∂ n : intuitively, the relation A ∂ n A ′ is included in the relation 'A/x → A ′ for some x ∈ A ≤n ' (see Lemma 3.13 for the formal statement). More to the point, the derivation relation captures a particular way of reflecting residuals, which enjoys some good properties: for every n, given A a nwqo in polynomial normal form (recall Remark 3.10), ∂ n A is a finite set of polynomial nwqos also in PNF, defined inductively by

∂ n 0 def = ∅ , (3.28) ∂ n N 0 def = {0} , (3.29) ∂ n N d def = {N d-1 • nd} , (3.30) ∂ n (A ⊔ B) def = ( (∂ n A) ⊔ B ) ∪ ( A ⊔ (∂ n B) ) , (3.31)
for d > 0 and A, B in PNF; in these definitions the ⊔ operations are lifted to act upon nwqo sets S by A ⊔ S def = {A ⊔ A ′ | A ′ ∈ S} and symmetrically.

Lemma 3.13 (C18). Let A be a polynomial nwqo in PNF and x ∈ A ≤n for some n. Then there exists

A ′ in ∂ n A such that A/x → A ′ .

Maximal Order Types.

As it is more convenient to reason with ordinal arithmetic rather than with polynomial nwqos, we map polynomial nwqos ⟨A, ≤, |.| A ⟩ to ordinals in ω ω using the maximal order type o(A) of the underlying wqo ⟨A, ≤⟩ [START_REF] De Jongh | Well-partial orderings and hierarchies[END_REF]; see Appendix A.1.2 for details. The map o is a bijection (but not an order isomorphism) between polynomial (n)wqos and ω ω :

o(0) = 0 , o(1) = 1 , o(N) = ω , o(A ⊔ B) = o(A) ⊕ o(B) , o(A × B) = o(A) ⊗ o(B) ,
where '⊕' and '⊗' denote the natural sum and natural product on ordinals (see Appendix A. 1.1.1). Thus, given a polynomial nwqo in PNF

A ≡ ⊔ m i=1 N d i , its associated maximal order type is o(A) = ⊕ m i=1 ω d i . Let us accordingly lift the definition of ∂ n to ordinals in ω ω , so that o(A ′ ) ∈ ∂ n o(A) if and only if A ′ ∈ ∂ n A.
We restate equations (3.29) to (3.31) using maximal order types: for all α > 0 in ω ω and all d, n in N

∂ n α def = { γ ⊕ ∂ n ω d | α = γ ⊕ ω d } , ∂ n ω d def = { 0 if d = 0, ω d-1 • (nd) otherwise. Observe that α ′ ∈ ∂ n α implies α ′ < α, thus ∪ n ∂ n is a well-founded relation.
This leads to the definition of an over-approximation of the length function L g,A (n):

(3.32) M g,α (n) def = max α ′ ∈∂nα { 1 + M g,α ′ (g(n)) } .
Proposition 3.14 (C18). For any polynomial nwqo A, any control function g, and any initial control n,

L g,A (n) ≤ M g,o(A) (n) . Proof. Either A ≤n is empty and then L g,A (n) = 0 ≤ M g,o(A) (n), or there exists some x ∈ A ≤n that maximises L g,A/x (g(n)) in the descent equation (3.16): L g,A (n) = 1 + L g,A/x (g(n)) . By Lemma 3.13 there exists A ′ ∈ ∂ n A such that A/x → A ′ , thus by (3.23) L g,A (n) ≤ 1 + L g,A ′ (g(n)) . By well-founded induction on A ′ ∈ ∂ n A, L g,A ′ (g(n)) ≤ M g,o(A ′ ) (g(n)) .
Thus by definition of M ,

L g,A (n) ≤ 1 + M g,o(A ′ ) (g(n)) ≤ M g,o(A) (n) □
3.4.4. Upper Bounds. As M g,α (n) is a subrecursive function, it only remains to compare it with more 'standard' functions like the Cichoń functions. We refer the reader to [L1] for the details of these finishing touches. To summarise those, we use the resemblance between ∂ n α and P dn (α) to show that, for α < ω d+1 [L1, Corollary 2.33]:

(3.33) M g,α (n) ≤ g α (n) assuming (γ + ω β+1 )(x) def = γ + ω β • (dx + 1)
. This extra twist of using an assignment of fundamental sequences different from the standard one of (3.8) can be avoided: (3.33) can be converted to the standard assignment of fundamental sequences at the price of some contortions, yielding [L1, Theorem 2.34]: Theorem 3.15 (Length Function Theorem for Polynomial nwqos). Let d > 0, g be a control function and select a monotone function

h such that h(x•d) ≥ g(x)•d for all x. If A is a polynomial nwqo with o(A) < ω d+1 , then L g,A (n) ≤ h o(A) (nd).

Setting h(x) def

= g(x)d always satisfies the conditions of the theorem. There are however examples where setting h def = g suffices: e.g., g(x Recall from §3.1.2.2 that we can use n as initial norm and H(x) def = x + 1 as control function on the bad sequences extracted from the Ascending Chain Condition on Equation (2.9). Setting h(x) def = x + d = H d (x) satisfies the conditions of Theorem 3.15. Hence the backward coverability computation on this instance converges after at most h ω d •p (nd) steps. We will analyse the complexity of the algorithm itself in Section 4.1.3 in the next chapter.

) def = 2x, g(x) def = x 2 , or g(x) def = 2 x ; more generally, Theorem 3.15 can use h def = g whenever g is super-homogeneous, i.e. satisfies g(dx) ≥ g(x)d for all d, x ≥ 1-then L g,A (n) ≤ g o(A) (nd).
Example 3.17 (Disjunctive Termination Arguments into N d ). Let us consider disjunctive termination arguments as in §2.2.2.2, where each of the d relations T j has a ranking function f j into N, i.e. the argument defines a quasi-ranking function f (s

) def = (f 1 (s), . . . , f d (s)) into ⟨N d , ≤ × ⟩. Assume f to be (g, ι)-controlled and let h(x) def = g(x)
• d. By Theorem 3.15, the program will terminate in time

h ω d (ι(s 0 )d) from configuration s 0 .
For the program of Figure 2.1, the invariants in equations (2.4) and (2.5) are shown well-founded by f 1 (ℓ 0 , x, y, n) def = x and f 2 (ℓ 0 , x, y, n) def = y respectively. Then g(x) def = 2x and ι(ℓ 0 , x, y, n) def = max(x, y, n) can be used to control the sequence of ranks

(f 1 (s 0 ), f 2 (s 0 )), (f 1 (s 1 ), f 2 (s 1 )), . . . As g is super-homogeneous, the program terminates in time g ω 2 (d•max(x, y, n)).
Note that this is nearly the same bound as in Example 3.7, which used lexicographic ranking functions instead. Remark 3.18 (Comparison with the Lexicographic Ordering). Examples 3.7 and 3.17 show that the bounds we obtain by applying Theorem 3.5 to lexicographic ranking functions into ⟨N d , ≤ lex ⟩ and Theorem 3.15 to disjunctive termination arguments into ⟨N d , ≤ × ⟩ are quite similar. Furthermore, as noted by [START_REF] Blass | Program termination and well partial orderings[END_REF], attempting to differentiate the two approaches through their maximal order types is inconclusive, since ω d is both the order type of ⟨N d , ≤ lex ⟩ and the maximal order type of ⟨N d , ≤ × ⟩. As Theorem 3.5 gives an exact measure of the length function but Theorem 3.15 only provides an upper bound, one might wonder whether there is a difference between the two length functions.

It turns out that the two length functions are different: since

⟨N d , ≤ lex ⟩ → ⟨N d , ≤ × ⟩, by (3.23) controlled bad sequences are at most as long in ⟨N d , ≤ lex ⟩ as in ⟨N d , ≤ × ⟩.
The following example taken from [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF]Remark 6.2] shows that they can be strictly shorter: the following sequence is a (g, 1)-controlled bad sequence over ⟨N 2 , ≤ × ⟩, which is good for ⟨N 2 , ≤ lex ⟩, where g(x) def = x + 2: (3.34)

(1, 1), (3, 0), (2, 0), (1, 0), (0, 9), (0, 8), . . . , (0, 1), (0, 0)

This sequence has length 14 whereas the maximal (g, 1)-controlled bad sequence for ⟨N 2 , ≤ lex ⟩ is of length g ω 2 (1) = 8:

(3.35) (1, 1), (1, 0), (0, 5), (0, 4), . . . , (0, 1), (0, 0) .

Related Work & Perspectives

The length function theorems we proved in this chapter are instances of a more general concern: whenever we prove the termination of a procedure using a wqo, we might also expect to gain some information about its complexity.

Put more abstractly, we seek to answer Kreisel's question 'What more than its truth do we know if we have a proof of a theorem in a given formal system?' in the particular setting of termination proofs and complexity analysis. This question can be understood in a strict sense, as requiring the termination proof to be carried in a proof system. For instance, [START_REF] Buchholz | Proof-theoretic analysis of termination proofs[END_REF] derives complexity bounds for term rewriting systems terminating using the multiset and lexicographic path orderings by showing that such termination proofs can be carried into 'small' fragments of Peano arithmetic, for which complexity bounds have long been known to exist [START_REF] Kreisel | On the interpretation of non-finitist proofs-Part II[END_REF]; [START_REF] Steila | Terminating via Ramsey's Theorem[END_REF] similarly analyses the Ramsey-based proof of termination by disjunctive termination arguments in several systems of arithmetic. More generally, the same question can be asked without necessarily referring to a precise proof system, e.g. for termination orderings [START_REF] Buchholz | Proof-theoretic analysis of termination proofs[END_REF][START_REF] Hofbauer | Termination proofs by multiset path orderings imply primitive recursive derivation lengths[END_REF]Lepper, 2001;[START_REF] Weiermann | Complexity bounds for some finite forms of Kruskal's Theorem[END_REF][START_REF] Weiermann | Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths[END_REF], polynomial interpretations [START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF], dependency pairs [START_REF] Hirokawa | Automated complexity analysis based on the dependency pair method[END_REF], size-change abstractions [START_REF] Ben-Amram | General size-change termination and lexicographic descent[END_REF], abstract interpretation [START_REF] Gulwani | SPEED: Symbolic complexity bound analysis[END_REF], disjunctive termination invariants [START_REF] Steila | Terminating via Ramsey's Theorem[END_REF], or ranking functions [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF] to cite a few.

Length Functions for Ordinals.

When focusing on ordinals below ε 0 , Theorem 3.5 will probably not surprise anyone familiar with ordinal recursive functions. In particular, Proposition 3.4 is a particular case of a connection established more generally by [START_REF] Cichoń | Termination orderings and complexity characterisations[END_REF] and [START_REF] Buchholz | A uniform approach to fundamental sequences and hierarchies[END_REF] between the definition of Hardy functions through fundamental sequences on the one hand, and through maximisation over ordinals of bounded norm on the other hand.

Nevertheless, the fact that we obtain an exact equality-not up to a primitiverecursive function-is worth mentioning, especially since the applications to program termination and coverability in LCMs require such a fine-grained statement if we wish to distinguish e.g. the d-dimensional case from the d + 1-dimensional one.

Two specific cases of Theorem 3.5 are also considered in the literature: the lexicographic ordering ⟨N d , ≤ lex ⟩ is analysed in [C19], and an upper bound for the multiset ordering over the lexicographic ordering ⟨M(N d ), ≤ m ⟩ is shown by Abriola, [START_REF] Abriola | Linearizing well-quasi orders and bounding the length of bad sequences[END_REF].

Length Functions for

Well-Quasi-Orders. The first upper bounds for bad sequences over ⟨N d , ≤ × ⟩ were proven by [START_REF] Mcaloon | Petri nets and large finite sets[END_REF] using an arguably complex combinatorial argument on large intervals. [START_REF] Clote | On the finite containment problem for Petri nets[END_REF] later published a simpler proof based on an analysis by [START_REF] Ketonen | Rapidly growing Ramsey functions[END_REF], but with coarser bounds than McAloon's and no parametricity in the control function. 2 In the context of commutative algebra, Moreno Socías [1992] shows similar bounds for chains of polynomial ideals. Friedman [2001, Theorem 6.2] also shows that the length functions for fixed d are primitive-recursive. Since the publication of [C19], [START_REF] Abriola | Linearizing well-quasi orders and bounding the length of bad sequences[END_REF] have obtained bounds similar to those of Theorem 3.15 by relating directly the product ordering with the lexicographic ordering.

Regarding other wqos, [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF] proved upper bounds for Higman's Lemma and arbitrary control functions. The presentation in Section 3.4 follows the framework of [C18], where tight bounds for Higman's Lemma are proven. The same framework has also been employed by [START_REF] Rosa-Velardo | Ordinal recursive complexity of unordered data nets[END_REF] to derive a length function theorem for finite multisets of tuples in ⟨N d , ≤ × ⟩, where multisets are ordered by multiset embedding. [START_REF] Weiermann | Complexity bounds for some finite forms of Kruskal's Theorem[END_REF] proved a length function theorem for Kruskal's Tree Theorem when using affine control functions. Weiermann's result encompasses many wqos, and it might be interesting to develop specialised versions for simpler wqos and to allow arbitrary control functions. As Kruskal's Tree Theorem is seldom needed in its full generality, to my knowledge this very general result has never been applied in the WSTS literature: indeed, this literature rather focuses on bounded-depth trees [e.g., D'Osualdo et al., 2017;[START_REF] Genest | Tree pattern rewriting systems[END_REF][START_REF] Meyer | On boundedness in depth in the π-calculus[END_REF][START_REF] Wies | Forward analysis of depth-bounded processes[END_REF], which are within the reach of the techniques of this chapter using nested applications of Higman's Lemma [C18], with F ε 0 upper bounds [J5].

Further Applications.

As wqos are pervasive in termination proofs, the upper bounds offered by length function theorems find applications in many fields. Besides the verification of infinite-state systems, the bounds in Sections 3.3 and 3.4 have been applied for instance to obtain small (inverse Ackermann) certificates in distributed decision systems [START_REF] Fraigniaud | Minimizing the number of opinions for fault-tolerant distributed decision using well-quasi orderings[END_REF], and sharp bounds for instance for the reverse mathematics of disjunctive termination arguments [START_REF] Steila | Terminating via Ramsey's Theorem[END_REF], for proof search in sequent calculi for substructural logics like relevance logic or contractive linear logic [START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF]J4], or for algorithms relying on Hilbert's Basis Theorem in algebraic geometry [START_REF] Benedikt | Polynomial automata: Zeroness and applications[END_REF][START_REF] León Sánchez | Derivation lengths and order types of Knuth-Bendix orders[END_REF]. This is only a small sample, as length function theorems have a surprisingly large number of applications, and rather than attempting to list them here, we refer the reader to the catalog of problems in [J3, Section 6].

Perspectives.

A natural direction to extend the results presented in this chapter is to attempt to prove length function theorems for other wqos and to refine the existing bounds when possible.

Trees and Graphs. Among the little-known consequences of Weiermann's 1994 result, it might for instance be worthwhile re-visiting the case of binary trees (with ε 0 as maximal order type [START_REF] Schmidt | Well-partial orderings and their maximal order types[END_REF]) and of series-parallel partial orders (with the Schütte-Feferman ordinal Γ 0 as maximal order type [START_REF] Pouzet | The order type of the collection of finite series-parallel posets[END_REF]).

A contrario, one could attempt to go beyond Kruskal's Tree Theorem and to investigate more general wqos, like graph minors; here, computing the maximal order type is already an issue [ [START_REF] Van Der Meeren | Connecting the Two Worlds: Well-partial-orders and Ordinal Notation Systems[END_REF]. Note however that the WSTS literature seems to consider the graph minor ordering as too permissive [e.g. [START_REF] König | Well-structured graph transformation systems[END_REF], and rather considers the subgraph or induced subgraph orderings on restricted classes of graphs [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF][START_REF] König | Well-structured graph transformation systems[END_REF], for instance with bounded path lengths [START_REF] Ding | Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes[END_REF] or bounded shrub-depth [START_REF] Ganian | When trees grow low: Shrubs and fast MSO 1[END_REF]-which can again be analysed using nested applications of Higman's Lemma.

Genericity. A systematic way of relating maximal order types with the length of controlled bad sequences is also missing. The work of [START_REF] Abriola | Linearizing well-quasi orders and bounding the length of bad sequences[END_REF] on N d , which analyses the combinatorics of controlled reifications-one of the main techniques for proving upper bounds on maximal order types-might be a first step in that direction.

Refinements. Finally, the length function theorems in this chapter all deal with amortised controlled sequences. It would be interesting to obtain tighter bounds for strongly controlled sequences. Recall for instance that the sequences arising in LCMs were in fact strongly controlled (see §3. 1.2.2), and this could be a way of closing the complexity gap for their coverability problem in fixed dimension (see the next chapter). CHAPTER 4

Fast-Growing Complexity

The previous chapter has shown how to derive complexity upper bounds for algorithms relying on wqos for their termination. For instance, for the backward coverability algorithm for LCMs, Example 3.16 extracted primitive-recursive upper bounds in terms of Cichoń functions when the number of counters was fixed, but only an upper bound of Ackermannian growth in general. We also saw with Example 3.1 that these bounds were rather tight.

However, when considering decision problems like Coverability rather than algorithms like Backward Coverability, the analysed algorithm itself might not be optimal. The standard tools to tackle such questions are complexity classes, along with the associated notions of reductions and completeness. This chapter first summarises [J3] and proposes in Section 4.1 a suitable definition for the non-elementary complexities often encountered when working with wqos. As an application, I show in Section 4.1.3 how the length function theorem of the previous chapter entail that the Backward Coverability algorithm for LCMs yields an upper bound in 'ACKERMANN', a complexity class for decision problems of Ackermannian complexity.

The point of these fast-growing complexity classes is however to be able to prove completeness statements. I therefore present in Section 4.2 a proof that LCM Coverability is ACKERMANN-hard, meaning that the Backward Coverability algorithm is essentially optimal for this model.

This hardness proof follows essentially the proof using weak computations due to Schnoebelen [2010a]. The presentation in this chapter uses a clearer, tail recursive formulation using Hardy functions, which I introduced in joint publications with Haase,Haddad,and Schnoebelen [C16;[START_REF] Schmitz | Algorithmic aspects of wqo theory[END_REF][START_REF] Schmitz | The power of well-structured systems[END_REF][START_REF] Haase | The power of priority channel systems[END_REF]. This formulation is easier to adapt to more complex settings, and has been successfully employed for proving lower bounds for Coverability in several families of WSTS (c.f. Table 4.1 on page 49). Furthermore, I introduce here a variant of the Hardy functions, which allows to derive slightly tighter lower bounds in fixed dimension than the original hardness proofs of [START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF] and [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]Schnoebelen [ , 2010a]] We define in this section an ordinal-indexed hierarchy (F α ) α<ε 0 of complexity classes. We rely for this on the Hardy functions (H ω α ) α<ε 0 from Section 3.2.2 as a standard against which we can measure high complexities.

In logic and recursion theory, the functions (H ω α ) α<ε 0 are used to generate the extended Grzegorczyk hierarchy (F α ) α<ε 0 [START_REF] Löb | Hierarchies of number theoretic functions[END_REF], when closed under substitution and limited primitive recursion. We shall start by recalling the definition of this hierarchy and some of it main properties in Section 4.1.1. As we shall argue, the classes in the extended Grzegorczyk hierarchy are however not suitable for our complexity classification objectives.

We define instead in Section 4.1.2 another hierarchy (F α ) α<ε 0 , where each F α class is the class of problems decidable within time bounded by a single application of H ω α composed with any function p already defined in the lower levels F β for β < α. We succinctly describe the main properties of these classes here, but the main argument in their favour is the catalogue of complete problems for several levels of the hierarchy, arising from the literature, and compiled in Section 6 of [J3].

The Extended Grzegorczyk

Hierarchy is an ordinal-indexed infinite hierarchy of classes (F α ) α<ε 0 of functions with argument(s) and images in N and was defined by [START_REF] Löb | Hierarchies of number theoretic functions[END_REF]. It has multiple natural characterisations: for instance via loop programs for α < ω [START_REF] Meyer | The complexity of loop programs[END_REF], via ordinal-recursive functions with bounded growth [START_REF] Wainer | A classification of the ordinal recursive functions[END_REF], via functions computable with restricted resources as we will see in Equation (4.2), via functions that can be proven total in fragments of Peano arithmetic [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF]], etc. 4.1.1.1. Computational Characterisation. The extended Grzegorczyk hierarchy itself is defined by means of recursion schemes with the (H ω α ) α as generators. Nevertheless, for α ≥ 2, each of its levels F α is also characterised as a class of functions computable with bounded resources [START_REF] Wainer | A classification of the ordinal recursive functions[END_REF].

Formally, it is arguably more natural to first define a slight variant (F <α ) α of the extended Grzegorczyk hierarchy. Each class F <α for α > 2 is the class of functions computable by deterministic Turing machines in time bounded by O(H γ (n)) for some ordinal γ < ω α , when given an input of size n. Using standard notations for complexity classes (where 'F' denotes as usual a class of functions, 'D' that we use deterministic Turing machines, and 'TIME' that we consider time-bounded computations), this translates as (4.1)

F <α def = ∪ γ<ω α FDTIME (H γ (n)) .
Note that the choice between deterministic and nondeterministic, or between time-and space-bounded computations in (4.1) is irrelevant, because α > 2 and

H ω 2 is already a function of exponential growth. We find among others in this hierarchy F <3 = FELEMENTARY the set of Kalmar-elementary functions, F <ω = FPRIMITIVE-RECURSIVE the set of primitiverecursive functions, and F <ω ω = FMULTIPLY-RECURSIVE the set of multiplyrecursive functions. 4.1.1.2. Main Properties. The classes F α are then simply defined for α ≥ 2 as

F α def = F <α+1 = ∪ γ<ω α+1 FDTIME (H γ (n)) . (4.2)
This is equivalent to the computational characterisation of [START_REF] Wainer | A classification of the ordinal recursive functions[END_REF]

F α = ∪ c<ω FDTIME ( (H ω α ) c (n) ) . (4.3)
Indeed, by Equation (3.12), H ω α •c is the same as the cth iterate (H ω α ) c of H ω α , and ω α • c < ω α+1 . Conversely we can rely on the fact that, for each γ < ω α+1 , there exists c < ω such that γ ≤ ω α • c, and then for all large enough n, H γ (n) ≤ H ω α •c (n) (c.f. Lemma A.1). Note that this also yields

F <α = ∪ β<α F β . (4.4)
Each class F α is closed under (finite) composition. Every function f in F α is honest, i.e. can be computed in time bounded by some function also in F α [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF][START_REF] Wainer | A classification of the ordinal recursive functions[END_REF]-this is a relaxation of the time constructible condition, which asks instead for computability in time O(f (n)). Since each f in F α is also bounded by H ω α •c for some c [Löb and Wainer, 1970, Theorem 2.10], this means that (4.5)

F α = ∪ f ∈Fα FDTIME (f (n)) .
In particular, for every α the function H ω α belongs to F α , and therefore, for every c, H ω α •c also belongs to F α . Every f in F β is also eventually bounded by H ω α if β < α [START_REF] Löb | Hierarchies of number theoretic functions[END_REF], i.e. there exists a rank x 0 such that, for all x 1 , . . . , x n , if max i x i ≥ x 0 , then f (x 1 , . . . , x n ) ≤ H ω α (max i x i ). However, for all α > β > 0, H ω α ̸ ∈ F β , and the hierarchy (F α ) α is therefore strict for α > 0. 4.1.1.3. Decision Problems. We have been dealing this far with classes of functions, but writing F * α for the restriction of F α to {0, 1}-valued functions, i.e.

F * <3 = ELEMENTARY F 3 = TOWER F * <ω = PRIMITIVE-RECURSIVE F ω = ACKERMANN F * <ω ω = MULTIPLY-RECURSIVE F ω ω = HYPER-ACKERMANN • • •
F * α = ∪ γ<ω α+1 DTIME (H γ (n)) , F * <α def = ∪ γ<ω α DTIME (H γ (n)) , (4.6)
we obtain the corresponding classes of decision problems F * <3 = ELEMENTARY, F * <ω = PRIMITIVE-RECURSIVE, and F * <ω ω = MULTIPLY-RECURSIVE. 4.1.2. The Fast-Growing Complexity Hierarchy. Unfortunately, the F * α classes in the extended Grzegorczyk hierarchy are not suitable for many interesting decision problems, which are non elementary (or non primitive-recursive, or non multiply-recursive, etc.), but only barely so. The issue is that complexity classes like e.g. F * 3 , which is the first class to contain non elementary problems, are very large: F * 3 contains for instance problems that require space H ω 3 •100 (n), more than a hundred-fold compositions of towers of exponentials. As a result, hardness for F * 3 cannot be obtained for many classical examples of non elementary problems. In fact, as we shall see at the end of §4.1.2.2, there are no complete problems for F * α under reasonable notions of reduction. We therefore introduce smaller classes of decision problems for 3 ≤ α < ε 0 :

(4.7) F α def = ∪ p∈F<α DTIME ( H ω α (p(n))
) .

In contrast with F * α in (4.6), only a single application of H ω α is possible, composed with some 'lower' reduction function p from F <α . This definition is intended to be used with reductions from F <α in hardness or completeness statements.

As previously, because we assume α ≥ 3 and F <α contains all the elementary functions, we can derive the robustness of the F α classes under changes in the model of computation-e.g. RAM vs. Turing machines vs. Minsky machines, deterministic or nondeterministic or alternating-or the type of resources under consideration-time or space; e.g. (4.8)

F α = ∪ p∈F<α NTIME ( H ω α (p(n)) ) = ∪ p∈F<α SPACE ( H ω α (p(n)) ) .
4.1.2.1. Milestones. The definition of the (F α ) α complexity classes yields for instance a class

TOWER def = F 3 = ∪ p∈FELEMENTARY DTIME ( H ω 3 (p(n))
) closed under elementary reductions (i.e., reductions from F 2 ), a class

ACKERMANN def = F ω = ∪ p∈FPRIMITVE-RECURSIVE DTIME ( H ω ω (p(n))
)

of Ackermannian problems closed under primitive-recursive reductions (i.e., reductions from F <ω ), and a class

HYPER-ACKERMANN def = F ω ω = ∪ p∈FMULTIPLY-RECURSIVE DTIME ( H ω ω ω (p(n))
)

of hyper-Ackermannian problems closed under multiply-recursive reductions (i.e., reductions from F <ω ω ), etc. In each case, we can think of F α as the class of problems not solvable with resources in F <α , but barely so: non elementary problems for F 3 , non primitive-recursive ones for F ω , non multiply-recursive ones for F ω ω , and so on. As a consequence of Corollary 4.2 below, the classes (F α ) α also yield another definition of the primitive-recursive and multiply-recursive problems:

PRIMITIVE-RECURSIVE = F * <ω = ∪ k F k , MULTIPLY-RECURSIVE = F * <ω ω = ∪ k F ω k .
See Figure 4.1 for the first main stops of the hierarchy.

4.1.2.2. Strictness. For an ordinal α > 2 and a finite k, let us define the class of decision problems

(4.9) k-F α def = ∪ γ<ω α •(k+1) DTIME ( H γ (n) ) .
By arguments similar to those sketched for (4.3), we see that (4.10)

F α = 1-F α ,
and the hierarchy (k-F α ) k,α is thus a generalisation of the (F α ) α one. The hierarchy (k-F α ) k,α captures the decision problems in the extended Grzegorczyk hierarchy: by definition of F * α and F * <α in (4.6),

F * α = ∪ k k-F α , F * <α = 0-F α . (4.11)
The (k-F α ) k,α hierarchy is proven to be strict in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Theorem 5.3] by a standard diagonalisation argument.

< β < α, k-F β ⊊ (k + 1)-F β ⊊ F * β ⊊ F α .
A consequence of Theorem 4.1 is that (F α ) α 'catches up' with (F * α ) α at every limit ordinal.

Corollary 4.2. Let λ be a limit ordinal, then

F * <λ = ∪ β<λ F β ⊊ F λ .
Proof. The equality F * <λ = ∪ β<λ F β and the inclusion F * <λ ⊆ F λ can be checked by considering a problem in some F * β for β < λ: it is in k-F β for some k > 0 by Equation (4.11), hence in F β+1 by Theorem 4.1, where β + 1 < λ since λ is a limit ordinal and therefore the problem is in F λ , again by Theorem 4.1. The strictness of the inclusion follows from (4.11) and Theorem 4.1 with k = 0. □ Note that strictness implies that there are no 'F * α -complete' problems under F <α reductions, since by Equation (4.11) such a problem would necessarily belong to some k-F α level, which would in turn entail the collapse of the (k-F α ) k hierarchy at the k-F α level and contradict Theorem 4.1.

Similarly, fix a limit ordinal λ and some reduction class F α for some α < λ: there cannot be any meaningful 'F * <λ -complete' problem under F α reductions, since such a problem would be in F * β for some α < β < λ, hence would contradict the strictness of the (F * β ) β<α hierarchy. Just like the Time Hierarchy Theorem entails that there are no 'ELEMENTARY-complete' problems, there are no 'PRIMITIVE-RECURSIVE-complete' nor 'MULTIPLY-RECURSIVE-complete' problems either.

4.1.2.3. Reduction Classes. In order to be used together with reductions in F <α , the classes F α need to be closed under such functions. Formally, for a function f : N → N and two languages A and B, we say that A many-one reduces to

B in time f (n), written A ≤ f m B,
∈ F α . If A ≤ F<α m B or A ≤ F<α T B, then A ∈ F α .
Of course, we could replace in (4.7) the class of reductions F <α by a more traditional one, like logarithmic space (FL) or polynomial time (FP) functions. We feel however that our definition in (4.7) better captures the intuition we have of a problem being 'complete for H ω α . ' Moreover, using at least F 2 as our class of reductions allows to efficiently compute H ω α itself within F α bounds, leading to interesting combinatorial algorithms (see §4.1.3.2 for an example).

We always assume many-one F <α reductions when discussing hardness for F α in the remainder of this manuscript.

4.1.2.4. Basic Complete Problem. By (4.7), F α -hardness proofs for many-one F <α reductions can reduce from the acceptance problem of some input string x by some deterministic Turing machine M working in time H ω α (p(n)) for some p in F <α . This can be simplified to a machine M ′ working in time H ω α (n) by a basic padding argument. Indeed, because p in F <α is honest, p(n) can be computed in F <α . Thus the acceptance of x by M can be reduced to the acceptance problem of a #-padded input string x ′ def = x# p(|x|)-|x| of length p(|x|) by a machine M ′ that simulates M , and treats # as a blank symbol-now M ′ works in time H ω α (n).

To sum up, we have by definition of the (F α ) α classes the following basic F α -complete problem.

Problem (Acceptance of H ω α -Bounded Turing Machines). instance: A deterministic Turing machine M working in time H ω α and an input x. question: Does M accept x?

This problem or slight variations of it has been used in most of the master reductions in the literature in order to prove non primitive-recursiveness, non multiple-recursiveness, and other hardness results [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF][START_REF] Jančar | Nonprimitive recursive complexity and undecidability for Petri net equivalences[END_REF]Lazić et al., 2016;[START_REF] Rosa-Velardo | Ordinal recursive complexity of unordered data nets[END_REF]Schnoebelen, 2010a;[START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF]C16;J5]. Section 6 in [J3] presents a catalogue of 'natural' complete problems at various levels of the (F α ) α hierarchy, which should be easier to employ in reductions.

4.1.2.5. Robustness. In the applications of fast-growing classes, one often relies on their 'robustness' to minor changes in their definition. More precisely, we can employ alternative generative functions; there are indeed many variants for the definition of the Hardy functions (H ω α ) α , but they are all known to generate essentially the same hierarchy (F α ) α . 1 The same holds for the hierarchy (F α ) α , as shown in Section 4 of [J3]; we shall see an example of this behaviour in §4.1.2.6.

The main rationale for this robustness is that each fast growing function class F α features enough 'wiggle room' to accommodate small computational overheads, where 'small' means 'in F <α '. A possible formal translation of this intuition is proven in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Lemma 4.6].

Lemma 4.4. Let f and f ′ be two functions in F <α . Then there exists p in

F <α such that f • H ω α • f ′ ≤ H ω α • p.
Lemma 4.4 justifies for instance Equation (4.8), since the overhead of working with different models of computation is elementary (hence in F <3 ) and α is always assumed to be at least 3.

Another application of Lemma 4.4 pertains to the computational resources required to compute H ω α itself. The functions H ω α are known to be honest, i.e. to be computable in time F α [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF][START_REF] Wainer | A classification of the ordinal recursive functions[END_REF]. This is however not tight enough to allow us to compute H ω α as part of an algorithm and retain an upper bound in F α . We use the following refinement instead: let us call a function f elementarily constructible if there exists an elementary function e in FELEMENTARY = F <3 such that f (n) can be computed in time e(f (n)) for all n.

Theorem 4.5 (J3). Let h: N → N be an elementarily constructible strictly increasing function and α be an ordinal, then h α is also elementarily constructible.

Together with Lemma 4.4, Theorem 4.5 shows that algorithms can afford to compute H γ for γ < ω α • 2 and still end with a complexity in F α .

1 See [START_REF] Ritchie | Classes of recursive functions based on Ackermann's function[END_REF] and [Löb and Wainer, 1970, pp. 48-51] for such results-and the works of Weiermann et al. on phase transitions for investigations of when changes do have an impact [e.g. [START_REF] Omri | Classifying the phase transition threshold for Ackermannian functions[END_REF]. 4.1.2.6. Relativised Hierarchies. One means of defining a variant of the fastgrowing complexity classes is to pick a base function h different from H(x) def = x + 1 for the Hardy hierarchy. The corresponding relativised complexity classes are then defined by (4.12)

F h,α def = ∪ γ<ω α •2 DTIME (h γ (n)) .
It is easy to check that, if g ≤ h, then g α ≤ h α for all α. Because we assumed h to be strictly increasing, this entails H α ≤ h α , and we have the inclusion F α ⊆ F h,α for all strictly increasing h. The converse inclusion does not hold, since for instance h ω is non elementary for h(x) = 2 x . Observe however that, in this instance, h ≤ H ω 2 and (H ω 2 ) ω = H ω 3 by Equation (3.12). This entails that F h,1 ⊆ F 3 when h(x) = 2 x . Thus, when working with relativised classes, one should somehow 'offset' the ordinal index by an appropriate amount. This idea is formalised in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Theorem 4.2] and allows to show: Theorem 4.6. Let h: N → N be a strictly increasing function and α, β be two ordinals.

(

i) If h ∈ F β , then F h,α ⊆ F β+1+α . (ii) If h ≤ H ω β , then F h,α ⊆ F β+α .
The statement of Theorem 4.6 is somewhat technical, but easy to apply to concrete situations; for instance: Corollary 4.7. Let h: N → N be a strictly increasing primitive recursive function and α ≥ ω. Then F h,α = F α .

Proof. The function h is in F k for some k < ω, thus F h,α ⊆ F k+1+α = F α by Theorem 4.6. Conversely, since h is strictly increasing, F α ⊆ F h,α . □

Example: LCM Coverability is in ACKERMANN.

As an application of the fast growing complexity classes, let us consider again the Coverability problem for lossy counter machines (c.f. Example 2.7). We have seen in Example 3.16 that the backward coverability algorithm terminates after at most L def = h ω d •p (nd) steps for an LCM with d counters and p states and a target configuration q, v with max c∈C v(c) = n, where h(x) def = x + d = H d (x). 4.1.3.1. Analysis of Backward Coverability. At this point, we can analyse more closely the computational cost of each step of the backward algorithm. By Equation (3.14), each of the vectors in the minimal bases for U i has norm at most (4.13)

N def = h ω d •p (nd) ≤ H ω d •dp (nd) ≤ H ω d+1 (ndp)
, and U i contains therefore at most p • (N + 1) d minimal configurations. As seen in Example 2.7, the computation of the minimal elements of U i+1 can therefore be performed in time e(N ) for some elementary function e ∈ F <3 . Hence the total time of the computation is bounded by e(N ) • L, which is an elementary function of N since L ≤ N by Equation (3.13). By Lemma 4.4, this is in F d+1 when the dimension d = |C| is fixed, and in F ω when d is part of the input. Theorem 4.8 (C19, Sec. VII-B). LCM Coverability is in F ω , and in F |C|+1 if the number of counters is fixed.

A Combinatorial Algorithm.

Another way of obtaining the bound of Theorem 4.8 is to rely on the existence of pseudo-witnesses pointed out in Remark 2.6. Indeed, instead of the backward coverability algorithm, we can leverage pseudo-witnesses to obtain a non-deterministic forward algorithm. The argument is that a pseudo-witness must have length bounded by the same N defined just before in Equation (4.13). The algorithm therefore (1) computes N in a first phase: as seen with Theorem 4.5, this can be performed in time (and space) H ω d+1 (e(ndp)) for some elementary function e, (2) then nondeterministically explores the reachable configurations, starting from the initial configuration q 0 , 0 and attempting to reach the target configuration q, v-but aborts if the upper bound on the length is reached. This second phase uses at most N steps, and each step can be performed in space polynomial in the size of the current configuration and of an N -bounded counter, thus in O(d log(N + 1) + log p). The whole phase can thus be performed using space polynomial in N , which is bounded by H ω d+1 (f (ndp)) for some f in F d by Lemma 4.4.

This algorithm thus works in space H ω d+1 (f (ndp)) for some f in F d , which by Equation (4.8) yields again Theorem 4.8.

Lower Bounds Through Hardy Computations

The main purpose of the fast-growing complexity classes (F α ) α is to provide the means to prove completeness statements. As an illustration, first of the fact that such high complexities can arise naturally in computer science, and second of how such lower bounds can be proven, we show here that Coverability is ACKERMANN-hard in lossy counter machines, thus matching the upper bound of Theorem 4.8. Theorem 4.9. LCM Coverability is F ω -hard, and F |C| -hard if the number of counters |C| ≥ 3 is fixed.

This result was first shown by [START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF] for a related model of expansive alternating counter machines, and independently by [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF] for lossy counter machines. The proof in this section follows the same general principle of implementing weak computers for fast-growing functions and their inverses (see Section 4.2.2), but works in the arguably more elegant setting of Hardy computations developed in [C16; L1; I4; J5]. Furthermore, we employ a variant of the Hardy functions (H α ) α defined Section 4.2.1, which allows to slightly improve over the F |C|-2 lower bound proven by Schnoebelen [2010a] when the number of counters is fixed. Remark 4.10 (Reset VASS). As explained by Schnoebelen [2010a], the bounds of Theorem 4.9 apply directly to reset vector addition systems with states, which are Minsky machines where the zero test operation is replaced by a reset operation that assigns zero to the counter; this is true even with a fixed number of counters. The F ω lower bound holds more generally for transfer vector addition systems [Schnoebelen, 2010a] and broadcast protocols [I4].

Hardy-like Computations.

We start with a variant of the Hardy hierarchy, that differs from the definition of (H α ) α in (3.10) on several counts:

• in successor cases, the argument is incremented by two instead of one, and • in limit cases, the argument is reset to 2 and the index descends slightly faster through the fundamental sequence, with an update of ω to x -1 instead of x + 1.

We define the a α function for α < ω ω and x > 0 by

a 0 (x) def = x , a α+1 (x) def = a α (x + 2) , a λ (x) def = a λ(x-2) (2) . (4.14)
The last two cases of (4.14) read left-to-right define a rewriting system over pairs (α, n) where 0 ≤ α < ω ω is an ordinal and n > 0 is a natural number:

(α + 1, n) → (α, n + 2) (4.15) (λ, n) → (λ(n -2), 2) (4.16) We call a rewriting sequence (α 0 , n 0 ) → (α 1 , n 1 ) → • • • → (α ℓ , n ℓ ) a Hardy-like computation. It enforces the invariant a α i (n i ) = a α 0 (n 0 ) for all i. Observe that α 0 > α 1 > • • • > α ℓ ,
thus such a computation must terminate, and that if α ℓ = 0 (in which case we say that the computation is complete), then n ℓ = a α 0 (n 0 ). 4.2.1.1. Basic Properties. The point of using superscripts for the ordinal indices in the (a α ) α hierarchy is that these functions satisfy the same identity for composition as the Hardy hierarchy (c.f. Equation (3.12)). Lemma 4.11 (Composition). Let α + β < ω ω be an ordinal term in Cantor normal form and x > 0. Then a α ( a β (x) ) = a α+β (x).

Proof. By transfinite induction over β. For the zero case, a α (a 0 (x)) = a α (x). For the successor case, a α ( a β+1 (x) 2) (2) = a α+λ (x). □ They also enjoy similar monotonicity properties.

) = a α ( a β (x + 2) ) = a α+β (x + 2) = a α+β+1 (x). For the limit case, a α ( a λ (x) ) = a α ( a λ(x-2) (2) ) = a α+λ(x-
Lemma 4.12 (Inflationary). For all 0 < x and 0 < α < ω ω , x < a α (x).

Proof. By transfinite induction over α. For the base case, a 1 (x) = x+2 > x. For the successor case, a α+1 (x) = a α (x+2) > x+2 ≥ x by induction hypothesis. For the limit case a λ (x) = a λ(x-2) (x) > x by induction hypothesis. □ Lemma 4.13 (Monotone). For all 0 < x < y and 0 ≤ α < ω ω , a α (x) < a α (y).

Proof. By transfinite induction over α. For the base case, a 0 (y) = y > x = a 0 (x). For the successor case, a α+1 (y) = a α (y + 2) > a α (x + 2) = a α+1 (x) by induction hypothesis. For the limit case, define z def = y -x > 0 and write the limit ordinal λ as γ + ω d+1 for some d and γ ≥ ω d+1 ; then a λ (y) = 1) (2) = a λ (x), where we applied Lemma 4.11, followed by Lemma 4.12 to show that a ω d •z is strictly inflationary and the induction hypothesis to show that a γ+ω d •(x-1) is strictly monotone. □ 4.2.1.2. Connection with the Ackermann Hierarchy. The hierarchy (a α ) α yields in the case of the ordinal indices (ω d ) d>0 a hierarchy of 'hyper-operations' that appears quite often in the literature, with multiplication by two appearing as the base case for d = 1 and the higher levels defined through iteration. Lemma 4.14 (Ackermann Hierarchy). For all x > 0, a ω (x) = 2x, and for all x, d > 0, a ω d+1 (x) = (a ω d ) x (1).

a λ(y-2) (2) = a γ+ω d •(y-1) (2) = a γ+ω d •(x-1)+ω d •z (2) = a γ+ω d •(x-1) ( a ω d •z (2) ) > a γ+ω d •(x-
Proof. Indeed, regarding the first equation,

a ω (x) = a x-1 (2) = 2 + 2(x -1) = 2x .
Let us also note that, for all d > 0, a ω d (1) = 2; indeed by definition (4.14),

a ω d+1 (1) = a ω d •0 (2) = a 0 (2) = 2 .
Thus, regarding the second equation, and using Lemma 4.11

a ω d+1 (x) = a ω d •(x-1) (2) = a ω d •(x-1) ( a ω d (1) ) = (a ω d ) x (1) . □
The definition in (4.14) thus results for instance in a ω 2 (x) = 2 x and a ω 3 (x) = tower(x), and is typically used in lower bound proofs. Nevertheless, the definition in (4.14) offers a tail-recursive viewpoint instead of an iterative viewpoint, which makes it easier to handle for our proofs.

We can define a hierarchy of classes of decision problems generated by the (a ω d ) d>2 functions by analogy with (4.7):

A d def = ∪ p∈F <d DTIME ( a ω d (p(n)) ) , A ω def = ∪ p∈F<ω DTIME ( a ω p(n)+1 (p(n))
) . (4.17) It turns out that this defines the same class of problems as F d , and thus that the halting problem of a ω d -bounded Minsky machines suffices to prove F d -hardness. Theorem 4.15 [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Theorem 4.1). For all 2 < α ≤ ω, A α = F α .

Therefore, using a padding argument as in §4.1.2.4, a basic F d -complete problem is the halting problem for Minsky machines where the sum of the counter values is bounded by a ω d (n) along the execution. Two counters suffice here, as the halting problem of 2-counters Minsky machines with counters bounded by [START_REF] Fischer | Counter machines and counter languages[END_REF], and the double exponential can be dealt with padding as we always assume d ≥ 3.

2 2 s(n) is hard for SPACE(s(n))

Problem (Halting of a ω d -Bounded Minsky Machines).

instance: A deterministic 2-counters Minsky machine M where the sum of counters is bounded by

a ω d (|M |). question: Does M halt?
Finally, the version of the problem with

d = |M | + 1 is F ω -complete.

Weak Computation in Lossy Counter

Machines. Let us fix some d > 0. We are going to implement Hardy-like computations and their inverses in Minsky machines, using an encoding of ordinals below ω d in a subset of their counters. The implementations in these Minsky machines will be perfect, in that they will compute a ω d and its inverse exactly. When the same machines are run as lossy counter machines, we will see that the lossy behaviour can only yield smaller or equal results: the implementations are weak computers for the functions. . . . . . .

ℓ a c2=0? c d-2 =0? c d-1 -- n-- c d-2 ++ n=0? c d-1 =0?

Codes. We construct Minsky machines with counters C

d def = {c d-1 , . . . , c 0 , n}. A valuation v = (c d-1 , . . . , c 0 , n) in N C d encodes a pair (α, n) from ω d × ω with α(v) def = ω d-1 • c d-1 + • • • + ω 0 • c 0 . (4.18)
Direct Computations. We translate the rewriting rules of (4.15) in terms of valuations (c d-1 , . . . , c 0 , n) in N C d , and unwrap the definition of the assignment of fundamental sequences from Equation (3.8):

(c d-1 , . . . , c 0 + 1, n) → a (c d-1 , . . . , c 0 , n + 2) (4.19) (c d-1 , . . . , c j + 1, 0, 0, . . . , 0, n) → a (c d-1 , . . . , c j , n -1, 0, . . . , 0, 2) (4.20)
for 0 < j ≤ d -1. These rules are straightforward to implement in a Minsky machine M a shown in Figure 4.2. Starting in ℓ in with valuation v = (c d-1 , . . . , c 0 , n) with n > 0, M a reaches ℓ a exactly when it has performed the complete Hardylike computation starting from the pair (α(v), n), and thus with a final resulting valuation (0, . . . , 0, a α(v) (n)).

Inverse Computations. We also need to translate the inverse rewriting rules of (4.15) in terms of valuations (c d-1 , . . . , c 0 , n) in N C d . This now yields the rules

(c d-1 , . . . , c 0 , n + 2) → a -1 (c d-1 , . . . , c 0 + 1, n) (4.21) (c d-1 , . . . , c j , n, 0, . . . , 0, 2) → a -1 (c d-1 , . . . , c j + 1, 0, 0, . . . , 0, n + 1) (4.22)
for 0 < j ≤ d -1. Note that the inverse rules are not deterministic, as for a given N there exist many pairs (α, n) such that a α (n) = N . However, for each fixed α, a α is injective since it is strictly monotone by Lemma 4.13.

The rules are again implemented in a Minsky machine

M a -1 depicted in Fig- ure 4.3. Starting in ℓ a -1 with valuation v = (c d-1 , . . . , c 0 , n) with n > 0, M a -1
performs inverse Hardy-like computation steps, and when reaching ℓ out must have found a valuation

(c ′ d-1 , 0, . . . , 0, n ′ ) such that a ω d-1 •c ′ d-1 (n ′ ) = a α(v) (n). ℓ a -1 n-- n=0? n++ c0-- c0=0? c1++ n-- c 0++ c0=0? n++ c1-- c1=0? c2++ . . . . . . ℓ out c1=0? c d-3 =0? n++ c d-2 -- c d-2 =0? c d-1 ++
a α(v) (v(n)) ≤ a α(v ′ ) (v ′ (n))
. By Lemmas 4.11 to 4.13, (4.23) holds. We say that our codes are robust; they ensure that losses can only yield results smaller than the perfect results we would have obtained with reliable semantics. Claim 4.16 (Weak Hardy-like Computations). In an LCM, the systems M a and M a -1 are such that, for all valuations

v 1 , v 2 , v 3 , v 4 in N C d , (1) if (ℓ in , v 1 ) → * ℓ (ℓ a , v 2 ), then a α(v 1 ) (v 1 (n)) ≥ v 2 (n) and v 2 (c j ) = 0 for all 0 ≤ j < d; (2) if a α(v 1 ) (v 1 (n)) = v 2 (n) with v 2 (c j ) = 0 for all 0 ≤ j < d, then an execution (ℓ in , v 1 ) → * ℓ (ℓ a , v 2 ) is possible; (3) if (ℓ a -1 , v 3 ) → * ℓ (ℓ out , v 4 ), then v 4 (c j ) = 0 for all 0 ≤ j < d -1 and a α(v 3 ) (v 3 (n)) ≥ a α(v 4 ) (v 4 (n)); (4) if (α(v 4 ), v 4 (n)) → * (α(v 3 ), v 3 (n)) is a Hardy-like computation with v 4 (c j ) = 0 for all 0 ≤ j < d -1, then an execution (ℓ a -1 , v 3 ) → * ℓ (ℓ out , v 4 ) is possible.

Lower Bound.

We prove now Theorem 4.9 for a number of counters d = |C| > 2. We start from an instance M = ⟨Q, {c 0 , c 1 }, δ, ℓ 0 ⟩ of the halting problem for a ω d -bounded Minsky machines, where we further assume the counters are initially valued to 0, and are zero-tested right before reaching the halting state ℓ h .

Counter Machine on a Budget. We modify M by adding a new counter n and by splitting transitions (introducing new intermediary states) so that any increment c i ++ for i ∈ {0, 1} is preceded by a decrement n--, and any decrement c i -for i ∈ {0, 1} is followed by an increment n++. The resulting machine M ′ is thus put on a budget; its sum of counters is bounded by the initial value of n, and any losses along a halting execution will result in a smaller valuation for n upon reaching q h . Claim 4.17 (Minsky Machine on a Budget). For all

ℓ in ℓ a ℓ 0 ℓ h ℓ a -1 ℓ out M a M ′ M a -1
N, N ′ , c 0 , c 1 in N, (1) if (ℓ 0 , 0, 0, N ) → * ℓ (ℓ h , c 0 , c 1 , N ′ ) in M ′ , then c 0 = c 1 = 0 and N ′ ≤ N ; (2) if (ℓ 0 , 0, 0) → * (ℓ h , 0, 0) in M and N ≥ a ω d (|M |), then (ℓ 0 , 0, 0, N ) → * ℓ (ℓ h , 0, 0, N ) in M ′ ; (3) if (ℓ 0 , 0, 0, N ) → * ℓ (ℓ h , 0, 0, N ) in M ′ , then (ℓ 0 , 0, 0) → * (ℓ h , 0, 0) in M . Reduction.
We finally plug M ′ with M a as an initialisation phase and M a -1 as a finalisation phase, resulting in the machine M d depicted in Figure 4.4. This machine uses d + 1 counters, but we will see later that we can remove one of its counters.

We define the source configuration for our instance of the Coverability problem to be (ℓ in , v) where v(c d-1

) def = |M | -1, v(c j ) def = 0 for 0 ≤ j < d -1, and v(n) def = 2. This satisfies α(v) = ω d-1 • (|M | -1), hence a ω d (|M |) = a α(v) (v(n))
. We define the target configuration for our instance to be (ℓ out , v). The LCM for our instance is M d .

Let us first check the correctness of our reduction. First assume that M halts, i.e. that it reaches (ℓ h , 0, 0) from (ℓ 0 , 0, 0) with sum of counters bounded by a ω d (|M |). Then by Claim 4.16.( 2), there is a (reliable) execution in M d from the source (ℓ in , |M | -1, 0, . . . , 0, 2) to (ℓ a , 0, 0, . . . , 0, a ω d (|M |)). Since this budget is sufficient by hypothesis on M , by Claim 4.17.( 2) there is a (reliable) execution of M ′ that reaches the configuration (ℓ a -1 , 0, 0, . . . , 0, a ω d (|M |)). By Claim 4.16.( 4), there is a (reliable) execution in M a -1 to the target (ℓ out , |M | -1, 0, . . . , 0, 2), which is therefore covered.

Conversely, assume the target is covered from the source in M d , i.e. that (ℓ in , v) → * ℓ (ℓ out , v ′′′ ) with v ′′′ ≥ v. By Claim 4.16.

(3) and the robustness of our encoding (4.23), this means that we entered

M a -1 in a configuration (ℓ a -1 , v ′′ ) such that a α(v ′′ ) (v ′′ (n)) ≥ a ω d (|M |)
. By Claim 4.17.( 1), this implies that v ′′ (c j ) = 0 for all 0 ≤ j < d and that we entered

M ′ with a configuration (ℓ a , v ′ ) with a α(v ′ ) (v ′ (n)) ≥ a α(v ′′ ) (v ′′ (n))
. By Claim 4.16.( 1), this entails that v ′ (c j ) = 0 for all 0 ≤ j < d and that (4.24)

a ω d (|M |) ≥ a α(v ′ ) (v ′ (n)) ≥ a α(v ′′ ) (v ′′ (n)) ≥ a ω d (|M |) . Thus M ′ had a budget of v ′ (n) = v ′′ (n) = a ω d (|M |)
at both the start and the end of its execution, which therefore had to be reliable: by Claim 4.17.( 3), (ℓ 0 , 0, 0) can reach (ℓ h , 0, 0) in M .

The construction of M d can eschew the use of c d-1 by maintaining its value as part of its state space. Indeed, in any reliable execution that covers the target, this counter value must remain less than |M |. This shows the F d -hardness of LCM Coverability for |C| = d > 2. [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF][Schnoebelen, , 2010a;;[START_REF] Urquhart | The complexity of decision procedures in relevance logic II[END_REF]Th. 4.9] Lossy Channel Systems F ω ω -complete [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF]; C14] Unordered Data nets [START_REF] Decker | On freeze LTL with ordered attributes[END_REF]] Priority Channel Systems F ε 0 -complete [J5] Finally, when the number of counters is not fixed, we can reduce from the halting problem for a ω |M |+1 -bounded Minsky machines; it suffices to set d def = |M | + 1 in the reduction above. This shows the F ω -hardness of coverability and concludes the proof of Theorem 4.9.

F ω ω -complete [Rosa-Velardo, 2017] Ordered Data nets F ω ω ω -complete [C16] Timed-arc Petri nets F ω ω ω -complete [C16] Nested Counter Systems F ε 0 -complete

Related Work & Perspectives

Together with the upper bounds provided by length function theorems such as the ones presented in Chapter 3, we have with the complexity classes (F α ) α from Section 4.1 and the template for proving lower bounds using Hardy computations from Section 4.2 a complete toolbox for pinpointing the exact complexity of many decision problems. Table 4.1 presents the results obtained using this toolbox on the coverability problem for several classes of WSTS.

I would however like to emphasise that many more problems have now been successfully classified with the (F α ) α classes, which can be found in the catalogue of problems in [START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF]Section 6]. While these problems all rely at some point on a wqo for their decidability, many do not explicitly involve WSTS nor coverability at all. In most cases, the lower bounds were obtained through reductions from coverability problems rather than going through the pains of a direct reduction from a halting problem as in Section 4.2.

Lower Bounds Through Counter

Objects. The hardness proof of Section 4.2 using weak implementations of Hardy computations and their inverses is not the only means to prove hardness statements for WSTS Coverability. In several classes of WSTS, weak computers for inverse Hardy computations are not known to exist-and there might even be evidence that they do not exist [START_REF] Leroux | On functions weakly computable by Petri nets and vector addition systems[END_REF].

Hardnesss proofs for coverability can rely instead on the implementation of counter objects. These should really be understood as an 'object-oriented' style of implementing bounded counters in the system at hand. Given a natural number n ∈ N, a counter object allows to manipulate an internal, private representation of a counter in the range [0, n -1] through an interface allowing to init: construct an instance with initial value 0, min: check whether the internal state represents 0, max: check whether the internal state represents n -1, incr: increment the represented counter by 1, decr: decrement the represented counter by 1. These operations deadlock if the check fails or the counter value would go outside the range [0, n-1]. When an implementation of counter objects for n is available, reducing from the halting problem for n-bounded multicounter Minsky machines is straightforward.

Given a counter object for n, one is sometimes able to implement a counter object for f (n) for some specific function f : N → N, using internally references to instances of the counter object for n. This mechanism allows therefore compositions of functions, or even iterations of functions.

This technique was introduced in by Lipton [1976] to prove the EXPSPACEhardness of Coverability in vector addition systems, where one can start with a counter object for 2 2 0 and compose it d times with the squaring function f (n) def = n 2 to implement a counter object for 2 2 d for any d. The more recent uses of counter objects in several hardness proofs are due notably to Lazić [Lazić et al., 2016;[START_REF] Lazić | What makes Petri nets harder to verify: Stack or data? In Concurrency, Security, and Puzzles -Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday[END_REF]J4;C5]. The complexity lower bounds in Table 5.2 on page 65 and in Table 6.1 on page 72 have all been obtained through applications of this idea.

The main difficulty, with both weak Hardy computations and counter objects, lies with the implementation in systems of restricted capabilities, which can quickly become very hard to manage [e.g. C16; C5]. The usage of proof assistants to ensure the correctness of the implementations would sometimes seem warranted.

Provability in Theories of Arithmetic.

We have heavily relied in this chapter and the previous one on definitions and results-including the subrecursive functions like the Hardy functions (H α ) α , the subrecursive hierarchies like the extended Grzegorczyk hierarchy (F α ) α , and more generally ordinal notation systems-that have been studied in mathematical logic and proof theory to analyse the strength of logical theories and find 'natural' mathematical statements independent from a theory [e.g. [START_REF] Fairtlough | Ordinal complexity of recursive definitions[END_REF][START_REF] Ketonen | Rapidly growing Ramsey functions[END_REF][START_REF] Schwichtenberg | Proofs and Computation[END_REF].

The 'proof-theoretic ordinal' of a logical theory is, very informally, the least ordinal whose notation is not provable in the theory [START_REF] Rathjen | The art of ordinal analysis[END_REF]. For instance, Gentzen's proof of the consistency of Peano arithmetic PA entails that it has prooftheoretic ordinal ε 0 ; similarly, the fragments IΣ i of PA, which are restricted to use the induction scheme on Σ 0 i formulae, have proof-theoretic ordinal ε 0 (i), i.e. a tower of ω's of height i + 1. It turns out that the proof-theoretic ordinal of a theory may also inform us on which qos can be proven to be wqo [START_REF] Simpson | Ordinal numbers and the Hilbert basis theorem[END_REF], and which functions of the Hardy hierarchy (H α ) α can be proven total in the theory: for a well-studied instance, IΣ i can prove the totality of H α if and only if α < ε 0 (i) [e.g. Schwichtenberg and Wainer, 2012, Theorem 4.3.4].

Thus F α -complete problems like the coverability problems in Table 4.1 are a likely source of natural 'decidability statements' independent from various theories: I mean here the statement that there is (an encoding of) a Turing machine that decides the problem, i.e. terminates on all inputs with the correct acceptance or rejection verdict. I conjecture that the decidability of F ω -complete coverability problems like LCM Coverability is independent from IΣ 1 , that the decidability of F ω ω -complete problems like Coverability in Lossy Channel Machines or Unordered Data Nets is independent from IΣ 2 , …, and that the decidability of Coverability in Priority Channel Systems is independent from PA. The consequence would be that, while these problems are decidable, their decidability proofs require strong logical theories. The same conjecture can be made for fragments of second-order arithmetic like RCA 0 (with proof-theoretic ordinal ω ω ) and ACA 0 (with proof-theoretic ordinal ε 0 ). CHAPTER 5

Reachability in Vector Addition Systems

Vector addition systems with states (VASS) are essentially multi-counter Minsky machines without zero tests. These systems are equivalent to Petri nets, and find a wide range of applications in the modelling of concurrent, chemical, biological, or business processes.

A Cornerstone Problem. The decidability of their reachability problem is considered as one of the greatest achievements of theoretical computer science. Its 1981 decidability proof for the reachability problem by Mayr is the culmination of more than a decade of research into the topic, and the algorithm has since been revisited and simplified by [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF] and [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF].

The centrality of the problem was recognised long before it was shown decidable; what is remarkable however is the regularity with which decision problemsin seemingly unrelated areas, in logic [START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Demri | Reasoning about data repetitions with counter systems[END_REF][START_REF] Kanovich | Petri nets, Horn programs, linear logic and vector games[END_REF], automata [START_REF] Crespi-Reghizzi | Petri nets and Szilard languages[END_REF][START_REF] Gischer | Shuffle languages, Petri nets, and context-sensitive grammars[END_REF][START_REF] Render | Rational subsets of polycyclic monoids and valence automata[END_REF], verification [START_REF] Esparza | Verification of population protocols[END_REF][START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]German and Sistla, 1992], etc.-turn out to be interreducible with the reachability problem. In fact, given its importance in many fields, it would be no exaggeration to define a complexity class REACHABILITY for the class of problems inter-reducible with VASS reachability; a representative sample can be found in [I2, Section 5].

Complexity. In spite of its importance, fairly little is known about the computational complexity of the reachability problem. Regarding the general case, the inclusive surveys on the complexity of decision problems on VASS by [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF] could only point to the EXPSPACE lower bound of [START_REF] Lipton | The reachability problem requires exponential space[END_REF] and to the fact that the running time of the known algorithms is not primitive recursive: no complexity upper bound was known, not even a coarse one, besides decidability-Bouziane claimed to have found an algorithm with primitive-recursive complexity in 1998, but it was shown incorrect by Jančar in 2008.

In [C8], I have shown with Leroux that reachability has a 'cubic Ackermann' upper bound, i.e. is in F ω 3 , by analysing the complexity of the classical algorithm developed and refined by Mayr, Kosaraju, and Lambert. Recall from Chapter 4 that F ω 3 is a non primitive-recursive complexity class, but among the lower multiplyrecursive ones; see Figure 5.1. The main ingredients for the analysis performed in [C8] are the fast-growing complexity bounds for termination proofs by wellquasi-orders and ordinal ranking functions from [C19; I3] and presented in Chapter 3.

In this chapter, I present a slightly improved version of the result from [C8], with a 'quadratic Ackermann' upper bound. Theorem 5.1 (Upper Bound Theorem). VASS Reachability is in F ω 2 , and in

F ω•(d+1) if the dimension d is fixed.
I give here a high-level presentation based chiefly on the invited column [I2], with pointers to [C8] for the detailed arguments. The algorithm used by Mayr, Kosaraju, and Lambert for the reachability problem is explained semi-formally on an example in Section 5.2, before we can work out how to apply the length function theorems from Chapter 3 and derive an F ω 2 upper bound. Let us first recall the basic definitions in the upcoming section. and [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF]

is a tuple V = ⟨Q, d, T ⟩ where Q is a finite set of 'control' states, d in N is a non-negative dimension, and T ⊆ Q × Z d × Q is a finite set of transitions.
The operational semantics of such a system is captured by an infinite transition system S V over the set of configurations Confs

V def = Q × N d , with a step (q, u) t -→ V (q ′ ,
u+a) defined whenever t = (q, a, q ′ ) belongs to T ; note that u+a must belong to N d for such a step to be possible. A run from a configuration c 0 to

ELEMENTARY F 3 = TOWER ∪ k F k =PRIMITIVE-RECURSIVE F ω F ω 2 F ω 3 ∪ k F ω k = MULTIPLY-RECURSIVE F ω ω Figure 5.1.
Pinpointing F ω 2 among the complexity classes beyond ELEMENTARY.

q 0 q 1 t 1 : (1, 1, -1)
t 2 : (-1, 0, 1)

t 3 : (1, 0, 0)
t 5 : (0, 0, 0)

t 4 : (0, -1, 0) Figure 5.2. A 3-dimensional VASS.
a configuration c ℓ is a finite sequence of steps c 0

t 1 -→ V c 1 t 2 -→ V c 2 • • • c ℓ-1 t ℓ
-→ V c ℓ , which can also be written c 0

t 1 •••t ℓ ---→ V c ℓ . Finally, let us write c 0 → * V c ℓ if there exists a finite sequence of transitions σ ∈ T * such that c 0 σ -→ V c ℓ .
Note that S V = ⟨Confs V , → V , ≤⟩, where (q, u) ≤ (q ′ , u ′ ) if and only if q = q ′ and u(i) = u ′ (i) for all 1 ≤ i ≤ d, is a WSTS as defined in Section 2.3, and VASS Coverability is decidable. We focus here on a more difficult problem: exact reachability in the infinite system S V .

Problem (VASS Reachability).

instance: A VASS V and two configurations c and c ′ in Confs V , question:

Can c reach c ′ , i.e. does c → * V c ′ ?
Example 5.2. Consider for instance the 3-dimensional VASS of Figure 5.2 with Q def = {q 0 , q 1 } and T def = {t 1 , t 2 , t 3 , t 4 , t 5 }. One can check that (q 0 , 1, 0, 1) reaches (q 1 , 2, 2, 1), for instance by the run (q 0 ,1,0,1) 2,2,1) . This is just one example of a run witnessing reachability; observe that any sequence of transitions in {t 1 t 2 , t 2 t 1 } n+2 t 3 t n 4 for n ≥ 0 would similarly do. Remark 5.3 (Binary Encodings). Regarding complexity, one typically assumes a binary encoding of the integers of a VASS and of the source and target configurations. If we let ∥a∥ def = max 1≤i≤d |a(i)| denote the infinity norm of a vector a in Z d , then the maximal effect ∥T ∥ def = max (q,a,q ′ )∈T ∥a∥ can be exponential in the

t 1 -→ (q 0 ,2,1,0) t 2 -→ (q 0 ,1,1,1) t 1 -→ (q 0 ,2,2,0) t 2 -→ (q 0 ,1,2,1) t 3 -→ (q 1 ,
p 1 p 2 p 3 Q-q q t 1 t 2 t 5 t 4 t 3 Figure 5.3. A Petri net equivalent to the VASS of Figure 5.2.
size of a VASS V = ⟨Q, d, T ⟩. The choice of a binary rather than a unary encoding has no impact in the general case-because there is a LOGSPACE reduction to the case where T ⊆ Q × {-1, 0, 1} d × Q (at the expense of increasing the dimension) and c = (q, 0) and c ′ = (q ′ , 0) for some states q, q ′ -, but is important in fixed dimension, see §5.4.2.2.

Closely Related Models.

Historically, VASS do not seem to have been studied before the works of [START_REF] Greibach | Remarks on blind and partially blind one-way multicounter machines[END_REF] and [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF]. Nevertheless, equivalent models had been investigated before, in particular Petri nets [Petri, 1962] and vector addition systems (VAS) [START_REF] Karp | Parallel program schemata[END_REF]. The absence of explicit control states makes these two classes of models rather convenient for the modelling of concurrent or distributed systems.

Vector Addition Systems.

A VAS is a pair ⟨d, A⟩ where A is a finite subset of actions in Z d [START_REF] Karp | Parallel program schemata[END_REF]. It defines a transition system with configurations u in N d and steps u → u + a for a in A, again implicitly checking that u + a ≥ 0. Put differently, a VAS can be seen as a VASS with a singleton state set. Conversely, the finite control of a d-dimensional VASS can be encoded in an equivalent VAS by increasing the system's dimension to d+3 [Hopcroft and Pansiot, 1979, Lemma 2.1].

The Decomposition Algorithm

The reachability problem was famously shown to be decidable by [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], building notably on an incomplete proof by [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems[END_REF].

Theorem 5.4 (Decidability Theorem; [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF]. VASS Reachability is decidable.

This proof has since been simplified twice: one year later by [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF], and another ten years later by [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF]. At the heart of these proofs lies a decomposition technique, which is called the 'Kosaraju-Lambert-Mayr-Sacerdote-Tenney' (KLMST) decomposition. In a nutshell, the KLMST decomposition defines both

• a structure (resp. regular constraint graphs for Mayr, generalised VASS for Kosaraju, and marked graph-transition sequences for Lambert) and • a condition for this structure to represent in some way the set of all runs witnessing reachability (resp. consistent marking, the θ condition, and the perfect condition).

The algorithms proposed by Mayr, Kosaraju, and Lambert compute this decomposition by successive refinements of the structure until the condition is fulfilled, by which time the existence of a run becomes trivial.

The reader is referred to the original articles of [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF] and Lambert [1992], and to the excellent accounts by [START_REF] Müller | The reachability problem for VAS[END_REF], [START_REF] Reutenauer | The mathematics of Petri nets[END_REF], and [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF] for examples and details on the KLMST decomposition. Here we shall keep the description at an informal level, and see how the decomposition algorithm works in the case of Example 5.2 without entering its details. A witness graph is a finite strongly connected directed graph G = (S, E) with vertices S ⊆ Q × N d ω , and labelled edges E ⊆ S × T × S, such that the edge labels from T are consistent with the vertices from S. This means that, if (s, t, s ′ ) is an edge in E with transition t = (q, a, q ′ ) from T as label, then s = (q, u) for some u in N d ω and s ′ = (q ′ , u + a). Note that these conditions together imply that all the vertices in the graph share the same set I ⊆ {1, . . . , d} of ω-components.

Marked Witness Graph

A marked witness graph M = (G, c in , s in , c out , s out ) is further endowed with distinguished input and output vertices s in and s out from S, along with input and output constraints c in and c out taken from

Q × N d ω , such that for all 1 ≤ i ≤ d, s in (i) ̸ = ω implies c in (i) = s in (i)
, and similarly for the output vertex and constraint. In other words, s in and c in agree on their finite components. This entails that I in the set of ω-components of c in is a subset of I the set of ω-components of s in , and similarly I out ⊆ I.

Finally, a marked witness graph sequence ξ is a sequence

(5.1) ξ = M 0 , t 1 , M 1 , . . . , t k , M k
alternating marked witness graphs M 0 , . . . , M k and transitions t 1 , . . . , t k taken from T . Let us write M j = (G j , c in j , s in j , c out j , s out j ) and t j = (q j , a j , q ′ j ) for all j. It is also required that, for all 1 ≤ j ≤ k, c out j-1 = (q j , u j ) for some u j and c in j = (q ′ j , u ′ j ) for some u ′ j . In such a sequence, c in 0 is the source and c out k is the target. q 0 , ω, ω, ω q 1 , ω, ω, ω q 0 , 1, 0, 1 q 1 , 2, 2, 1

t 1 : (1, 1, -1)
t 2 : (-1, 0, 1)

t 3 : (1, 0, 0)
t 5 : (0, 0, 0) t 4 : (0, -1, 0)

Figure 5.4. The initial marked witness graph sequence ξ 0 = M 0 .

Figure 5.4 displays a marked witness graph for the VASS of Example 5.2, with input constraint (q 0 , 1, 0, 1) on the input vertex (q 0 , ω, ω, ω) and output constraint (q 1 , 2, 2, 1) on the output vertex (q 1 , ω, ω, ω); this is the initial marked witness graph for the decomposition algorithm when attempting to decide whether (q 1 , 2, 2, 1) is reachable from (q 0 , 1, 0, 1).

An Example of a KLMST Decomposition.

The KLMST decomposition algorithm builds a sequence Ξ 0 , Ξ 1 , Ξ 2 , . . . of finite sets of marked witness graph sequences. At step n, it checks whether all the sequences ξ in Ξ n are perfect (in the sense of [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF], or equivalently fulfil the θ-condition of [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]) and stops if this is the case; then either Ξ n is empty and the algorithm answers 'not reachable', or Ξ n is not empty and the algorithm answers 'reachable'.

If however some sequence ξ from Ξ n is not perfect, then it is decomposed into a finite set of marked witness graph sequences dec(ξ)-which is possibly empty. Then we let (5.2)

Ξ n+1 def = (Ξ \ {ξ}) ∪ dec(ξ) and the algorithm proceeds to the next step.

The perfectness condition comprises two sub-conditions, along with the corresponding ways of decomposing marked witness graph sequences when the subconditions are violated. We are going to illustrate these two sub-conditions in the upcoming §5.2.2.1 and §5.2.2.2, in the case of Example 5.2, and starting from Ξ 0 = {ξ 0 }. 5.2.2.1. Flow Constraints. Consider a path from the source to the target in the graph of Figure 5.4: denoting by z j the number of times transition t j is used along this path for j ∈ {1, . . . , 5}, we can see that (5.3)

z 3 = z 5 + 1 .
Consider now a run in the VASS of Figure 5.2, which follows a path in the marked witness graph of Figure 5.4 from (q 0 , 1, 0, 1) to (q 1 , 2, 2, 1), i.e. with overall effect (1,2,0). Then, considering the effect of these transitions for each coordinate i in {1, 2, 3},

(5.4)

z 1 + z 3 = z 2 + 1 , z 1 = z 4 + 2 , z 1 = z 2 .
The system of equations (5.3-5.4) requires z 3 = 1 and z 5 = 0; z 1 , z 2 and z 4 are on the other hand unbounded.

q 0 , ω, ω, ω q 0 , 1, 0, 1 q 0 , ω, ω, ω q 1 , ω, ω, ω q 1 , ω, ω, ω q 1 , 2, 2, 1

t 1 : (1, 1, -1)
t 2 : (-1, 0, 1)

t 3 : (1, 0, 0)
t 4 : (0, -1, 0)

Figure 5.5. The next marked witness graph sequence

ξ 1 = M ′ 0 , t 3 , M ′ 1 .
This shows that the marked witness graph sequence ξ 0 of Figure 5.4 is too permissive, allowing to follow paths that do not bring the source of the sequence to its target. We therefore decompose it, using the fact that t 3 must be employed exactly once and that t 5 is never employed: dec(ξ 0 ) = {ξ 1 } where the new sequence ξ 1 is depicted in Figure 5.5; it contains two marked witness graphs M ′ 0 and M ′ 1 connected by a single occurrence of transition t 3 . In general, flow constraints are expressed using two systems of equations built from the sequence ξ. One system ensures that there exists a solution to Kirchhoff's Laws when considering the finite values in c in j and c out j ; if not, then dec(ξ) = ∅ because no run enforcing these constraints can exist. The second system ignores these finite values and allows to check that there exist solutions with

• unbounded number of occurrences of each transition in ∪ j E j -if not the offending marked graph is unfolded finitely many times up to the bound, as in the example-and • unbounded values can instantiate the ω's in the input and output constraints c in j and c out j -if not we replace these ω's by finite values below the bound.

The checks can be carried in polynomial time in the size of ξ, while the extracted bounds in case of a decomposition are at most exponential in this size. See for instance [Leroux, 2010, Section 3] for a detailed exposition. 5.2.2.2. Pumpability. A marked witness graph M is forward pumpable if there exist runs in the VASS following paths of M and starting from the input vertex which, when applied to the input constraint, allow to 'pump' arbitrarily high values in the (necessarily common) components labelled ω in the vertices of the graph.

On the one hand, M ′ 0 in Figure 5.5 is not forward pumpable: any run of the VASS of Figure 5.2 starting from (q 0 , 1, 0, 1) and using only t 1 and t 2 can indeed reach arbitrarily high values on the second component, but the first and third components are bounded.

On the other hand, M ′ 1 is forward pumpable, but not backward pumpable: starting from (q 1 , 2, 2, 1) and applying t 4 in reverse allows to reach arbitrarily high values on the second component, but the first and third components are again bounded.

Again, the decomposition algorithm will observe that the current marked witness graph sequence over-approximates the possible behaviours of the VASS, and refine M ′ 0 and M ′ 1 using their bounded components. Propagating the flow constraints, we obtain the final marked witness sequence depicted in Figure 5.6. This q 0 , 1, ω, 1 q 0 , 2, ω, 0 q 0 , 0, ω, 2 2,2,1 t 1 : (1,1,0,0,1) t 1 : (1,1,t 3 : (1, 0, 0) t 4 : (0, -1, 0)

q 0 , 1, 0, 1 q 0 , 1, ω, 1 q 1 , 2, ω, 1 q 1 , 2, ω, 1 q 1 ,
Figure 5.6. The final marked witness graph sequence

ξ 2 = M ′′ 0 , t 3 , M ′′ 1 .
sequence is perfect, and captures in some sense 1 all the runs from (q 0 , 1, 0, 1) to (q 1 , 2, 2, 1) in the VASS of Example 5.2.

In general, forward and backward pumpability reduce to instances of the place boundedness problem on the marked witness graph under consideration, which can be solved in EXPSPACE [e.g. C17]. If pumpability fails, the bounded values can be computed in practice using the coverability tree construction of [START_REF] Karp | Parallel program schemata[END_REF], with Ackermannian upper bounds [C19, Section VII-C]. See again [Leroux, 2010, Section 3] for a detailed exposition.

Termination.

The termination of the KLMST decomposition algorithm relies on a ranking function r mapping marked witness graph sequences to elements of a well-order, and ensuring r(ξ) > r(ξ ′ ) whenever ξ ′ belongs to dec(ξ) [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]. More precisely, the ranking function r associates to ξ a multiset of triples of natural numbers, one triple for each marked witness graph in the sequence. These triples consist of (1) |I|, the number of ω-components of the marked witness graph, (2) |E|, the number of transitions of the marked witness graph, and (3) |I in | + |I out |, the number of ω-components in the input and output constraints.

This results for the sequences ξ 0 , ξ 1 , and ξ 2 of our example in the multisets (5.5)

r(ξ 0 ) = {(3, 5, 0)} , r(ξ 1 ) = {(3, 2, 3), (3, 1, 3)} , r(ξ 2 ) = {(1, 4, 1), (1, 1, 1)} .
Let us consider the lexicographic ordering over N 3 ; finite multisets of triples in N 3 are then well-ordered using the ordering of [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF].

We can see the KLMST algorithm as building in general a forest of marked witness graph sequences, with the elements of Ξ 0 as its finitely many roots, and where each imperfect marked witness graph sequence ξ is the parent of the sequences in dec(ξ). The ranking function r then shows that the trees in this forest are of finite height; since dec(ξ) is finite for all ξ, they are also of finite branching degree, hence the trees are finite by Kőnig's Lemma and the algorithm terminates. 1 It represents exactly the downward closure of the set of runs from (q0, 1, 0, 1) to (q1, 2, 2, 1); see the Decomposition Theorem of [C8] and Section 6.4.2, which might also help the reader build an intuition about marked witness graph sequences and the KLMST decomposition algorithm.

Complexity Upper Bound

Hopefully, the reader has now some intuition about the KLMST decomposition algorithm. The key point for complexity considerations is the termination argument by a ranking function explained in Section 5.2.3: we know that any sequence ξ 0 , ξ 1 , ξ 2 , . . . of marked witness graph sequences with ξ n+1 ∈ dec(ξ n ) is finite since (5.6) r(ξ 0 ) > r(ξ 1 ) > r(ξ 2 ) > • • • is a decreasing sequence in the well-order of multisets of triples of naturals. In order to bound the complexity of the KLMST decomposition algorithm, we are going to bound the length L of such sequences. We shall relate this length with the order type of the ranking function.

An Ordinal Ranking Function.

The order type of multisets of triples of natural numbers is ω ω 3 [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF], and we can equivalently see the ranking function r of Section 5.2.3 as ranging over ordinals below ω ω 3 : the ranks in (5.5) then become (5.7)

r(ξ 0 ) = ω ω 2 •3+ω•5 , r(ξ 1 ) = ω ω 2 •3+ω•2+3 + ω ω 2 •3+ω+3 , r(ξ 2 ) = ω ω 2 +ω•4+1 + ω ω 2 +ω+1
. This is where we can refine the results from [C8]. In the ranking function defined in Section 5.2.3, the first component of the triples is bounded by d, and the third by 2d. Thus the order type of the ranking function is actually ω ω•(d+1) . To see this, define the rank of a single marked witness graph M with edge set E, ω-components I, and input and output ω-components I in and I out by

r(M ) def = ω • |I| + (2d + 1) • |E| + |I in | + |I out | (5.8)
and the rank of a marked witness graph sequence by

r(M 0 , t 1 , M 1 , . . . , t k , M k ) def = ⊕ 0≤j≤k ω r(M j ) (5.9)
where '⊕' denotes the natural sum over ordinals (see Appendix A. 1.1.1). This results in the ordinal ranks (5.10)

r(ξ 0 ) = ω ω•3+7•5 = ω ω•3+35 , r(ξ 1 ) = ω ω•3+7•2+3 + ω ω•3+7+3 = ω ω•3+17 + ω ω•3+10 , r(ξ 2 ) = ω ω+12 + ω ω+8
for the multisets of (5.5) instead of the ordinal ranks of (5.7).

Applying the Length Function

Theorems. If we provide an initial norm n ≥ d + 1 and a control function g for sequences like (5.5), we will obtain by Theorem 3.5 on page 25 an (5.11)

L def = g ω ω•(d+1) (n) bound on their lengths. Regarding the initial norm, the maximum of the sizes of the initial sequences in Ξ 0 will do, and is bounded by the size of the reachability instance, which is certainly at least d + 1. For the control function, let us first note that N r(ξ) ≤ ∥ξ∥ for any reasonable definition of the size ∥ξ∥ of a marked witness graph sequence ξ. Thus we will bound the size of the marked witness graph sequences ξ ′ in dec(ξ) compared to that of ξ. This is done formally in [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF], where a control function (5.12) g(x) def = H ω d+1 (e(x)) for an elementary function e is shown. Let us examine how this control function is obtained.

5.3.2.1. Controlling Decompositions for Flow Constraints. In the case of the flow conditions of §5.2.2.1, ∥ξ ′ ∥ ≤ 2 p(∥ξ∥) for some polynomial p, as it is constructed based on the solution to a polynomial-sized system of equations derived from ξ.

5.3.2.2. Controlling Decompositions for Pumpability. In the case of the pumping conditions of §5.2.2.2, the blow-up can be bounded using Theorem 3.15 from page 30. Indeed, the size of ξ ′ can be bounded by ∥ξ∥ • B d where B bounds the maximal finite values in a coverability tree construction à la [START_REF] Karp | Parallel program schemata[END_REF] applied to the marked witness graph M = ((S, E), c in , s in , c out , s out ) under consideration.

As ) also provides a bound g L (n), i.e. of L iterations of the function g, on the size of the marked witness graph sequences constructed by the KLMST decomposition algorithm. Thus we have a bound on the space complexity of a non-deterministic version of the algorithm, which explores the decomposition tree until it finds a perfect marked witness graph. Note that we neglect here the various algorithmic overheads of testing for perfectness-this is in EXPSPACE-and of actually building the decompositions, because Lemma 4.4 allows us to hide all these in the elementary function e of (5.12).

By Equation (3.13) and because n ≥ d + 1, this yields a bound of (5.15)

g L (n) = g ω ω•(d+1) (n) ≤ g ω ω 2
(n) using the Hardy hierarchy on the space complexity of this algorithm. By Theorem 4.6 on page 42, and because g in (5.12) is in F d+1 , or F ω when d is part of the input, we obtain an F ω•(d+1) upper bound when d is fixed, and a 'quadratic Ackermann' F ω 2 upper bound in general, as announced in Theorem 5.1.

Remark 5.5. Recall from Chapter 4 that the following complexity classes are different: 'quadratic Ackermann' complexity F ω 2 , which as we just saw contains VASS reachability, 'double Ackermann' complexity F ω•2 , which is for instance the complexity of coverability in ν-Petri nets [C5], 'Ackermann plus one' complexity F ω+1 , and 'composed Ackermann' complexity 2-F ω , which corresponds to problems solvable in time bounded by the Ackermann function composed with itself once (see §4. 1.2.2). The underlying functions of the Hardy hierarchy that define these complexity classes are respectively

• H ω ω 2 , which eventually dominates H ω ω•k for every k, • H ω ω•2
, which eventually dominates H ω ω+k for every k, • H ω ω+1 , which eventually dominates H ω ω •k for every k, and

• H ω ω •2 = H ω ω • H ω ω ,
which is the composition of the Ackermann function with itself.

There is a considerable complexity jump between each one of these classes, and they should not be confused with each other.

Related Work & Perspectives

There is a considerable literature surrounding the computational complexity of the VASS Reachability Problem and of several related problems, drawing a complex landscape of results. I give here a somewhat partial account of the current literature, summarised in Table 5.1. The main question, about how tight the F ω 2 upper bound of Theorem 5.1 might be is discussed in Section 5.4.1. Given the lack of a definitive answer on the complexity of VASS Reachability, it is also natural to consider simpler problems, which I discuss in Section 5.4.2. The few known results and many open problems related to Reachability in VASS extensions are then quickly mentioned in Section 5.4.3; some of those questions will be further discussed in the next chapter. 5.4.1. Tightness. Facing a galactic upper bound like F ω 2 , it is natural to ask how tight it is. It seems very likely that it is not tight; to the best of our knowledge, the problem might very well be EXPSPACE-complete: the best complexity lower bound is indeed the following 1976 result of Lipton already mentioned in Section 4.3.1 (see also the presentation given by [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]). Theorem 5.6 (Lower Bound Theorem;[START_REF] Lipton | The reachability problem requires exponential space[END_REF]. VASS Reachability is

EXPSPACE-hard.
This leaves a gigantic gap between EXPSPACE and F ω 2 . Nevertheless, the upper bound is obtained with a specific algorithm, the KLMST decomposition algorithm, which-due to its reliance on coverability trees-is known to require at least an Ackermannian time in the worst case [START_REF] Müller | The reachability problem for VAS[END_REF], i.e. there is an F ω lower bound for that particular algorithm. Hence, besides the main open question about the exact complexity of the reachability problem, there is a possibly easier open question about the complexity of the KLMST decomposition algorithm, with a smaller complexity gap between F ω and F ω 2 . 5.4.1.1. Language Inclusion Problems. In fact, the KLMST decomposition algorithm solves much more than just reachability, and we can justify the F ω lower bound. Indeed, the final computed decomposition Ξ n contains a lot of information about the 'set of executions' from c to c ′ ,2 allowing in particular to reason about the set of sequences σ ∈ T * such that c σ -→ V c ′ . An appropriate context here is the one of labelled VASS, i.e. when the VASS V = ⟨Q, d, T, ℓ, Σ⟩ is further equipped with a labelling function ℓ: T → Σ * into some finite alphabet Σ-which is lifted to a homomorphism from T * to Σ * -, and one can define its reachability language (5. 16)

L(V, c, c ′ ) def = {ℓ(σ) ∈ Σ * | c σ -→ V c ′ } .
The language emptiness problem then asks, given V and two configurations c, c ′ , if L(V, c, c ′ ) = ∅; this is the complement of the reachability problem and it is decidable. By contrast, the language inclusion problem asks, given two VASS

V 1 , V 2 and four configurations c 1 , c ′ 1 , c 2 , c ′ 2 , whether L(V 1 , c 1 , c ′ 1 ) ⊆ L(V 2 , c 2 , c ′ 2 )
. Like most behavioural quasi-orders on VASS, it is an undecidable problem [START_REF] Jančar | Nonprimitive recursive complexity and undecidability for Petri net equivalences[END_REF], and this was one of the first VASS problems to be shown undecidable [START_REF] Hack | Decidability questions for Petri nets[END_REF]. [START_REF] Habermehl | The downward-closure of Petri net languages[END_REF] have shown that, once the KLMST decomposition algorithm has terminated, one can compute in polynomial time from the resulting decomposition Ξ n a regular expression E Ξn denoting the downwardclosure of L(V, c, c ′ ) with respect to subword embedding ≤ * (c.f. Section 2.1.2):

(5.17)

L(E Ξn ) = ↓L(V, c, c ′ ) . Thus the following variant of the language inclusion problem is decidable:

Problem (Downward VASS Language Inclusion). instance: Two VASS V 1 , V 2 and four configurations c 1 , c ′ 1 ∈ Confs V 1 and c 2 , c ′ 2 ∈ Confs V 2 . question: Is ↓L(V 1 , c 1 , c ′ 1 ) ⊆ ↓L(V 2 , c 2 , c ′
2 )? While decidable, this problem was proven ACKERMANN-hard by [START_REF] Zetzsche | The complexity of downward closure comparisons[END_REF]; the conclusion is that any algorithm for VASS Reachability that computes a similar decomposition will require at least F ω time. One should therefore look for new algorithms; note that reachability only needs to find some execution witnessing reachability, while downward language inclusion needs to account for all the possible such executions.

5.4.1.2. Inductive Presburger Invariants. Leroux has invented in 2010 a new, very simple algorithm for VASS Reachability based on inductive Presburger invariants. The initial proof relied on the KLMST decomposition, but [START_REF] Leroux | Vector addition system reachability problem: a short selfcontained proof[END_REF] then re-proved the correctness of this new algorithm without referring to it, yielding an compact, and self-contained decidability proof for VASS Reachability.

While the new algorithm is considerably simpler than the KLMST decomposition algorithm, it is also more difficult to analyse, as it consists of two semidecision procedures and its 2011 proof relies on non-constructive arguments. It should however be possible to extract complexity upper bounds from the 2010 proof based on the KLMST decomposition, but as mentioned above this decomposition has at least Ackermannian worst-case size.

Restrictions.

Due to the considerable difficulty of both the decidability proofs themselves and of proving any upper bounds, it is natural to consider 'simpler' variants of the VASS Reachability Problem. [START_REF] Lipton | The reachability problem requires exponential space[END_REF] EXPSPACE [START_REF] Leroux | Vector addition system reversible reachability problem[END_REF] Coverability EXPSPACE [START_REF] Lipton | The reachability problem requires exponential space[END_REF] EXPSPACE [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] Dim-2 Reachability, binary encoding PSPACE [START_REF] Fearnley | Reachability in two-clock timed automata is PSPACE-complete[END_REF]] PSPACE [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] Dim-1 Reachability, binary encoding NP [Subset Sum] NP [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF]] Dim-2 Reachability, unary encoding NL [STCON] NL [START_REF] Englert | Reachability in two-dimensional unary vector addition systems with states is NL-complete[END_REF] Language Inclusion undecidable [START_REF] Hack | Decidability questions for Petri nets[END_REF][START_REF] Jančar | Nonprimitive recursive complexity and undecidability for Petri net equivalences[END_REF] [START_REF] Lipton | The reachability problem requires exponential space[END_REF] decidable [START_REF] Bonnet | Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems[END_REF][START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF] [START_REF] Lazić | What makes Petri nets harder to verify: Stack or data? In Concurrency, Security, and Puzzles -Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday[END_REF] open 5.4.2.1. Related Problems. The best known variant is arguably the Coverability Problem (c.f. Section 2.3.3), where one asks instead for the existence of a configuration c ′′ such that c → V c ′′ and c ′′ ≥ c ′ for the product ordering over configurations. The proof of [START_REF] Lipton | The reachability problem requires exponential space[END_REF] for the EXPSPACE-hardness of reachability in Theorem 5.6 already applies to coverability, and the problem was shown to be in EXPSPACE by [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. Coverability suffices for many algorithmic applications, and unlike the reachability, there are several implementations, with increasing success at solving it on large practical instances [e.g. Blondin et al., 2017b;[START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF][START_REF] Geffroy | Occam's Razor applied to the Petri net coverability problem[END_REF][START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF].

Many more decision problems on VASS have been shown EXPSPACE-complete based on the techniques of Rackoff [e.g. [START_REF] Atig | On Yen's path logic for Petri nets[END_REF][START_REF] Demri | On selective unboundedness of VASS[END_REF][START_REF] Leroux | A relational trace logic for vector addition systems with application to context-freeness[END_REF][START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF]C17]. Notably, the following reversible reachability problem is also EXPSPACE-complete [START_REF] Leroux | Vector addition system reversible reachability problem[END_REF].

Problem (Reversible VASS Reachability).

instance: A VASS V and two configurations c and c ′ in Confs V , question: Can both c → * V c ′ and c ′ → * V c? The proof for the EXPSPACE upper bound by [START_REF] Leroux | Vector addition system reversible reachability problem[END_REF] combines insights from both [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] and the KLMST decomposition algorithm. Adapting these ideas to prove tighter upper bounds for the KLMST decomposition algorithm seems promising, but has not been successful so far.

Fixed Dimension.

A natural way of restricting the reachability problem is to fix the dimension. The F ω•(d+1) upper bound of Theorem 5.1 in dimension d is rather unsatisfactory, as it assumes d ≥ 2, and is hopelessly high: for instance, in dimension one with a binary encoding of weights, VASS Reachability is NP-complete [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF]-this is a subcase of reachability in one-counter automata.

In the 2-dimensional case, [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF] were the first to show decidability by proving that the reachability set from a given initial configuration c was effectively semilinear, i.e. that one could compute for each state q a representation of the set of vectors u such that c → * V (q, u) as a finite union of linear sets

(5.18) L(b, {p 1 , . . . , p n }) def = {b + λ 1 p 1 + • • • + λ n p n | λ 1 , . . . , λ n ∈ N}
defined by a base b in Z d and a finite set of periods p j in Z d -equivalently, these sets are definable in Presburger arithmetic FO(Z, +, ≤). [START_REF] Howell | Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states[END_REF] then showed that this construction was in 2-NEXP and improved it to obtain a 2-EXP algorithm. This left a gap with the NP-hardness proven by [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF] the same year. The lower bound was improved to PSPACE-hardness by [START_REF] Fearnley | Reachability in two-clock timed automata is PSPACE-complete[END_REF], and finally [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] closed the complexity gap with a PSPACE upper bound. These bounds hold with a binary encoding of the weights of the input VASS. As mentioned in Remark 5.3, the choice of a binary or unary encoding has an influence in fixed dimension, and [START_REF] Englert | Reachability in two-dimensional unary vector addition systems with states is NL-complete[END_REF] further refined the analysis of [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] to show that reachability is NL-complete in dimension 2 when assuming a unary encoding.

The upper bounds in dimension 2 in [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF][START_REF] Englert | Reachability in two-dimensional unary vector addition systems with states is NL-complete[END_REF]] are technical feats relying on fine geometric analyses of the effect of semilinear path schemes [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF] witnessing the semilinearity of reachability, i.e. regular expressions of the form Hopcroft and Pansiot [1979, Lemma 2.8] showed that there exists a 3-dimensional VASS with a non-semilinear reachability set, so this approach does not readily generalise to higher dimensions.

(5.19) v 0 w * 1 v 1 • • • w * k v k for some finite sequences v 0 , w 1 , v 1 , . . . , w k , v k of transitions in T . However,

Extensions.

The decidability of the reachability problem for VASS is an intricate result, and undecidability is never very far. This section is an opportunity to see how far the Decidability Theorem can be pushed, but also to advertise for a few open problems. 5.4.3.1. Zero Tests. A zero test is a special type of transition t = (q, zero i , q ′ ) where i ranges over {1, . . . , d}, allowing a step (q, u)

t -→ (q ′ , u) if u(i) = 0.
Allowing unrestricted zero tests yields a Minsky machine, with an undecidable reachability problem already in dimension two-even coverability is undecidable on such systems.

However, reachability in VASS extended with the ability to test a single component for zero-for instance always the first component-remains decidable. It still remains decidable if several components can be tested with a hierarchical policy: component i 1 can be freely tested for zero, but i 2 can only be tested for zero in configurations where the i 1 th component is zero, and i 3 only in configurations where both the i 1 th and i 2 th components are zero, etc. [START_REF] Bonnet | Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems[END_REF][START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF]. The complexity of reachability in these models is widely open; the best known lower bound is still Lipton's EXPSPACE-hardness, and no upper bound is known. 5.4.3.2. Recursion and Nesting. Motivated by the need to model distributed systems with some recursive behaviour, there is a variety of VASS extensions that include recursion in some manner, and differing on the (sometimes subtle) way in which they allow interactions between recursion and the integer components. For instance, nested counter systems [START_REF] Decker | Ordered navigation on multi-attributed data words[END_REF][START_REF] Decker | On freeze LTL with ordered attributes[END_REF][START_REF] Lomazova | Some decidability results for nested Petri nets[END_REF] act on finite multisets of finite multisets of … of finite multisets of states as configurations, allowing to model hierarchical computations, but have an undecidable reachability problem. On the other hand, the process rewrite systems of [START_REF] Mayr | Process rewrite systems[END_REF] perform prefix rewrites on terms of a process algebra, and generalise in a sense both VASS and pushdown systems, but still enjoy a decidable reachability problem-with unknown complexity.

Pushdown VASS. One natural way to extend VASS to handle recursion is to add new push and pop operations acting on a pushdown stack with a finite stack alphabet. Note that this generalises VASS with a single zero test, since the particular component tested for zero could be implemented as a stack with a distinguished bottom-of-stack symbol. The decidability of reachability is currently open, but here at least we have better lower bounds: [START_REF] Lazić | What makes Petri nets harder to verify: Stack or data? In Concurrency, Security, and Puzzles -Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday[END_REF] showed indeed the problem to be TOWER-hard.

Alternating Branching VASS. A different way of adding a pushdown stack to a VASS is to let it store vectors from N d on its stack. The system can then add a vector a from Z d to the vector u currently on top of the stack. The key question is which semantics to employ when popping u and pushing multiple vectors, say u 1 and u 2 , to the top of the stack. For instance, if we allow to duplicate the vector u so that u = u 1 = u 2 , then we obtain the model of alternating VASS [e.g. C9], which have an undecidable reachability problem.

A very interesting case occurs when we split u nondeterministically into u 1 and u 2 such that u = u 1 + u 2 . This model of branching VASS was introduced by [START_REF] Rambow | Multiset-valued linear index grammars: imposing dominance constraints on derivations[END_REF] in computational linguistics, and independently rediscovered on several occasions since [see the survey in C21]. The decidability of the reachability problem for branching VASS is a major open problem, that we further discuss in Section 6.4. As with pushdown VASS, although we do not know whether reachability is decidable, we have again a TOWER lower bound [J4].

5.4.3.3. Data. The model of data nets of Lazić, Newcomb, Ouaknine, Roscoe, and Worrell [2008] extends Petri nets with the ability to manipulate data from some infinite domain D. Different variants exist, all with an undecidable reachability problem, except for one case: unordered data Petri nets, where the system can only manipulate data as pure names through equality and disequality constraints. In more concrete terms, the configurations of such a system no longer carry a single vector from N d , but a finite multiset of them, padded with infinitely many 0's. Transitions nondeterministically select some (bounded) number of such vectors u 1 , . . . , u k , and apply some translations a 1 , . . . , a k from Z d to each one. The decidability of the reachability problem for this model is open, with an ACKERMANN lower bound proven by [START_REF] Lazić | What makes Petri nets harder to verify: Stack or data? In Concurrency, Security, and Puzzles -Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday[END_REF].

CHAPTER 6

Perspectives

The techniques presented in this thesis provide a comprehensive set of tools for studying the computational complexity of algorithms relying on wqos for their termination: lower bounds through weak implementations of Hardy-style computations (Section 4.2), upper bounds using length function theorems for bad controlled sequences (Chapter 3), and suitable complexity classes for the nonelementary complexities usually encountered in this setting (Section 4.1). We have seen how these techniques can be applied to the safety verification of lossy counter machines, where they allow to prove the F ω -completeness of the coverability problem (Theorems 4.8 and 4.9); this is the simplest case among the coverability problems solved using this standard toolbox (see Table 4.1). As an additional application of these techniques, we have been able to derive the first known complexity upper bounds for VASS Reachability in Chapter 5, a long-standing open question for this central problem with numerous ramifications in logic, automata, process calculi, etc. [see I2, Section 5].

I have already pointed to a number of open issues at the end of each chapter, two of which I recall next in Sections 6.1 and 6.2. However, some of the most interesting perspectives connected to the work in this thesis deal with ideals; those have already proven useful in several algorithmic applications of wqos, which I shall describe in Sections 6.3 and 6.4.

Complexity of VASS Reachability

The most important open question is arguably the exact complexity of VASS Reachability. Our F ω 2 complexity bound certainly beats not having any upper bound at all, but it leaves a gigantic gap with the EXPSPACE lower bound of [START_REF] Lipton | The reachability problem requires exponential space[END_REF]. As pointed in Section 5.4.1, a possibly easier question is to close the complexity gap for the KLMST decomposition algorithm, between F ω and F ω 2 ; this would also allow to prove tight bounds for the Downward VASS Language Inclusion Problem.

Perspective. Show an ACKERMANN upper bound on the size of the KLMST decomposition.

Parameterised Bounds

The bounds in Theorems 4.8 and 4.9 for LCM Coverability do not quite match when the number of counters is fixed. A similar issue arises with the upper bounds for lossy channel machines parameterised by the size of the alphabet, analysed in [C14]. The outcome is that there are no examples of 'natural' decision problems for most of the intermediate complexity classes (F α ) α . Refined 69 upper bound analyses seem required to close these gaps and prove for instance the F |C| -completeness of LCM Coverability with a fixed number of counters.

Tightening such enormous complexity bounds might seem of purely theoretical interest. These are worst-case complexity bounds, with arguably very little bearing on the running time of the actual algorithms when run on practical instances coming from abstractions of real programs and protocols [e.g. [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF][START_REF] Kaiser | Lost in abstraction: Monotonicity in multi-threaded programs[END_REF]. But the question is likely to involve a deeper understanding of how counters, and more generally resources, interact in a system: can we finely capture these interactions through a better parameterisation than just the number of counters? Classical work in implicit complexity theory should be an inspiration here [e.g. [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF][START_REF] Kristiansen | On the computational complexity of imperative programming languages[END_REF], and might even lead to tractable bounds for the systems arising in practice [see Ben-Amram and [START_REF] Ben-Amram | On the edge of decidability in complexity analysis of loop programs[END_REF][START_REF] Brázdil | Efficient algorithms for checking fast termination in VASS[END_REF]Zuleger, 2017, for recent related work].

Perspective. Invent parameterisations of counter machines leading to tight parametric bounds and tractable upper bounds on practical instances.

Algorithmic Applications of Ideals

Let us consider again Backward Coverability from §2.3.3.2. The algorithm relies on two main properties of wqos:

• the Ascending Chain Condition, which ensures the constructed sequence of upwards-closed sets is finite, and • the Finite Basis Property, which allows us to finitely represent upwardsclosed sets and manipulate them algorithmically. Dually, a wqo is also equivalently characterised by the Descending Chain Condition: any descending sequence D 0 ⊇ D 1 ⊇ D 2 ⊇ • • • of downwards-closed subsets eventually stabilises. Hence, provided we could represent these downwardsclosed subsets finitely, we could rely on this dual condition for termination. The right objects for this are ideals.

6.3.1.

Ideals. An ideal of a qo ⟨A, ≤⟩ is a downwards-closed and directed subset I ⊆ A, where this last condition ensures that I is non-empty and that, given any x ∈ I and y ∈ I, there exists z ∈ I with x ≤ z and y ≤ z. We write Idl(A) for the set of ideals of A. For instance, {0, . . . , 4} and the whole of N are ideals of N; in fact, regarding the former, ↓x for x ∈ A is always an ideal of A, and called a principal one. While ideals are well-known objects in order theory, their application to verification problems is quite recent: they have been popularised in a series of articles initiated by Finkel and Goubault-Larrecq [Blondin et al., 2017a;Finkel andGoubault-Larrecq, 2009, 2012a] on a forward alternative to the backward coverability algorithm.

A related notion is the following. A downwards-closed subset D of ⟨A, ≤⟩ is irreducible if and only if it is non-empty, and for any two downwards-closed subsets D 1 , D 2 such that D ⊆ D 1 ∪ D 2 , D is contained in D 1 or in D 2 already; equivalently, D is non-empty and cannot be written as the union of two proper, downwards-closed subsets. Fact 6.1 (Bonnet, 1975, Lemma 1). Let D be a downwards-closed subset of a qo. The following are equivalent:

(1) D is an ideal;

(2) D is directed;

(3) D is irreducible.

Ideals are especially useful when ⟨A, ≤⟩ is a wqo: for one thing, when A is countable, Idl(A) is then also countable [Bonnet, 1975, Theorem 1], and furthermore any downwards-closed subset has a decomposition as a finite union of ideals. Recall that a qo has the finite antichain property (is FAC) if all its antichains are finite. Fact 6.2 (Bonnet, 1975, Lemma 2). A qo is FAC if and only if every downwardsclosed subset is a finite union of ideals.

Thanks to Fact 6.2, any downwards-closed set has a representation using finitely many ideals. Furthermore, by Fact 6.1, there is a unique minimal such decomposition, which we call the canonical ideal decomposition of D. Should we manage to find effective representations of wqo ideals, this will provide us with algorithmic means to manipulate downward-closed sets. This last endeavour is the subject of [START_REF] Finkel | Forward analysis for WSTS, part I: Completions[END_REF][START_REF] Goubault-Larrecq | The ideal approach to computing closed subsets in well-quasiorderings[END_REF]. Not only do most of the wqos mentioned in Section 2.1.2 (and several more) come with finite ideal representations, but furthermore these representations can be manipulated algorithmically: the inclusion relation I ⊆ J, and the canonical decompositions of A, of ↓x, of I ∩J, and of A\↑x can all be computed for elements x and ideals I, J of A.

A Dual Backward Coverability Algorithm.

As an example of application of ideals, one can formulate a dual of the Backward Coverability Algorithm relying on ideals and the Descending Chain Condition. This allows to prove upper bounds in some cases where the approach through controlled bad sequences has proven inconclusive; for instance, the set of configurations of a VASS is Q × N d , and this is isomorphic to that of a lossy counter machine, thus the bounds one can extract from Theorem 3.15 for the backward coverability algorithm are the same for both formalisms. However, coverability is ACKERMANNcomplete in LCM but only EXPSPACE-complete in VASS.

Consider an instance of the Coverability Problem on a system ⟨S, →, ≤⟩ and two configurations s, t ∈ S. We compute instead the limit of the sequence This dual algorithm requires effective ideal representations and predecessors. It computes exactly the complements D n = S \ U n of the elements in the sequence defined by Equation (2.9), and therefore terminates after the same number of steps. Thus it might seem that we have not gained anything by considering this variant.

It turns out however that considering the dual algorithm sometimes allows to exhibit 'monotonicity' invariants on the sets D n , from which tighter upper bounds can be derived. In joint work with Lazić [W1], we have shown how to derive the EXPSPACE upper bound for VASS Coverability, together with the upper bounds of Table 6.1, in a generic manner. The known bounds for these problems were adaptations of Rackoff's ad-hoc analysis for VASS Coverability [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF]C9;J4]. We further show in [C5] a new upper bound for a variant of Table 6.1. The complexity of Coverability in more families of WSTS.

WSTS Complexity Reference

Bottom-up Branching VASS 2-EXP-c. [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF]; W1] Top-down Alternating VASS 2-EXP-c.

[C9; W1] Top-down Branching VASS TOWER-c.

[J4; W1] ν-Petri nets F ω•2 -c. [C5] data nets called ν-Petri nets. All the lower bounds in Table 6.1 rely on counter interfaces, which were presented succinctly in Section 4.3.1.

Beyond

Well-Quasi-Orders. Ideals also appear in two extensions of wqos and well-structured transition systems.

The first one is to consider Noetherian spaces. A topological space is Noetherian if there are no infinite descending chains C 0 ⊋ C 1 ⊋ • • • of closed sets. This generalises well-partial-orders with the Alexandroff topology, which defines closed sets as the downwards-closed ones; however not every Noetherian space is the Alexandroff topology of a wpo. The notion of well-structured transition systems has been extended by [START_REF] Goubault-Larrecq | On Noetherian spaces[END_REF], 2010] to work on Noetherian spaces with a continuity condition instead of compatibility as defined in (2.6). For instance, polynomial automata as used by [START_REF] Benedikt | Polynomial automata: Zeroness and applications[END_REF] fall within this extended setup, while the complexity of their equivalence problem was analysed using the techniques mentioned just before in Section 6.3.2.

The second one is to work with FAC quasi-orders. As seen in Fact 6.2, all we need in order for finite ideal decompositions to exist is the absence of infinite antichains. Blondin et al. [2017c] have accordingly proposed a generalisation of well-structured transition systems based on FAC quasi-orders and the usual compatibility condition. While the backward coverability procedure does not always terminate on such systems (as the ascending chain condition does not hold), Coverability is nevertheless still decidable (under effectiveness conditions), thanks to two semi-decision procedures, one of which amounting to finding a downwardsclosed forward invariant: a downwards-closed set containing the source configuration s and closed under the transition relation →; this relies on ideal decompositions to enumerate candidate downwards-closed sets.

Perspective. Design techniques for analysing the computational complexity of algorithms relying on Noetherian spaces and FAC orders.

Incidentally, there are relatively few examples of problems and classes of systems that can be tackled through Noetherian spaces and FAC orders, but not through classical WSTS algorithms, and this seems worth developing.

Reachability in VASS Extensions

We have seen a number of VASS extensions where the decidability of the reachability problem is still open in Table 5.2, where Branching VASS are of special importance. Ideals provide a potential attack to these problems, through extensions of the Decomposition Theorem proven with Leroux in [C8].

6.4.1. Branching VASS Reachability. Branching vector addition systems with states (BVASS) form a natural extension of VAS invented independently in several fields (see [C21] for a survey, in particular of the linguistic applications). The reachability problem for BVASS is a notorious open problem in theoretical computer science [START_REF] Bojańczyk | Some open problems in automata and logic[END_REF]. Several communities have indeed arrived to the same roadblock: it is equivalent to provability in multiplicative exponential linear logic [START_REF] De Groote | Vector addition tree automata[END_REF]-the sole fragment of propositional linear logic with unknown decidability status, open since 1990-it was also defined independently in computational linguistics [START_REF] Rambow | Multiset-valued linear index grammars: imposing dominance constraints on derivations[END_REF], cryptographic protocol verification [START_REF] Verma | Karp-Miller trees for a branching extension of VASS[END_REF], verification of APIs for distributed computing [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF], and a slight extension of it is also equivalent to satisfiability of data logics for XML processing [START_REF] Jacquemard | FO 2 (<, +1, ∼) on data trees, data tree automata and branching vector addition systems[END_REF] and observational equivalence of functional program in ML [Cotton-Barratt et al., 2017]; finally, it has the dubious honour of having an incorrect published decidability proof [START_REF] Bimbó | The decidability of the intensional fragment of classical linear logic[END_REF]. While decidability is open, we know however that the problem has non-elementary complexity [J4]. Regarding fixed dimensions, only dimension 1 is known to be decidable [START_REF] Figueira | Polynomialspace completeness of reachability for succinct branching VASS in dimension one[END_REF][START_REF] Göller | A polynomial-time algorithm for reachability in branching VASS in dimension one[END_REF].

Ideal Decomposition of the Set of Executions.

A very promising angle of attack to the problem is provided by the Decomposition Theorem in [C8]. This theorem shows that the celebrated algorithms for reachability in VASS developed in by [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF], and [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF] can be understood as computing a finite ideal decomposition of the downward-closure of the set of executions of a VASS.

Formally, we see an execution (q 0 , u 0 )

t 1 -→ V (q 1 , u 1 ) t 2 -→ V • • •
tn -→ V (q n u n ) from c 0 def = (q 0 , u 0 ) to c n def = (q n , u n ) in a VASS V as a triple (c 0 , σ, c n ) where σ is the sequence of triples ((q i , u i ), t i+1 , (q i+1 , u i+1 )) 0≤i<n . Therefore an execution is an element of PreRuns def = Confs × (Confs × T × Confs) * × Confs. This set is naturally endowed with a well-quasi-odering ⊴ using Dickson's and Higman's lemmata [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF], and we can consider the downward-closure ↓Runs V (c 0 , c n ) of the set of executions from c 0 to c n . By facts 6.1 and 6.2, this downwards-closed set has a unique finite decomposition into ideals. Theorem 6.3 (Decomposition Theorem; C8). The KLMST decomposition algorithm computes a representation for the ideal decomposition of ↓Runs V (c 0 , c n ).

The main ingredients of the proofs of Mayr, Kosaraju, and Lambert can be recast in this light: the manipulated 'marked witness graph sequences' turn out to be representations for ideals of a specific shape, the decomposition algorithm is an abstraction refinement loop that gets closer and closer to the desired downwardclosure, and the termination criterion is an instance of adherence membership. This last condition, of a topological flavour, asks whether there exists executions of the system arbitrarily close to the limit denoted by the ideal, and is shown to be equivalent to the perfectness (aka θ) condition described in Section 5.2 for the ideals represented by marked witness graph sequences.

In a general setting, adherence membership can be formulated for finitely represented subsets X ⊆ A of a wqo ⟨A, ≤⟩,-e.g. Runs V (c 0 , c n ) ⊆ PreRuns in the Decomposition Theorem, which is represented by the VASS V and the configurations c 0 and c n -and finitely represented ideals I.

Problem (Adherence Membership).

instance: A subset X ⊆ A over a wqo ⟨A, ≤⟩ and an ideal I of A. question: Is I adherent to X, i.e. does there exist a directed subset ∆ ⊆ X such that I = ↓∆?

A connection between adherence membership and computing downwardclosures was exhibited in [C4]: under effectiveness assumptions, the problem of computing downward-closures of subsets X of A and the one of deciding adherence membership are Proposition 16]. However, these effectiveness assumptions do not hold in the case of VASS executions, and one can show that adherence membership is undecidable for VASS executions and arbitrary ideals of PreRuns [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF]Theorem V.2]. Nevertheless, this provides an essential insight into what the KLMST decomposition is really performing; a crucial point in the Decomposition Theorem is that we only need to handle the rather specific ideals that arise during the decomposition, which are ideals represented by marked witness graph sequences.

Extending this approach to handle the branching executions of BVASS is a very challenging endeavour, but at least we have now a general framework in which we can attack the problem.

Perspective. Extend the framework of the Decomposition Theorem to solve BVASS Reachability.

As related problems, the decidability of reachability is also open in unordered data Petri nets and pushdown VASS, and could be approached from the same angle (c.f. Table 5.2). In fact, the decidability proof of [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF] for VASS with a single zero test or hierarchical zero tests also seems approachable with these techniques. In turn, this approach motivates further investigations of the basic properties, finite representations, and algorithmics of ideals and of the adherence membership problem. This is called the maximal order type of ⟨A, ≤⟩, since de Jongh and Parikh show that there always exists a linearisation ⟨A, ⪯⟩ that reaches this order type, i.e. 'sup' can be replaced by 'max' in (A.1) [START_REF] Blass | Program termination and well partial orderings[END_REF] also call this the stature of ⟨A, ≤⟩). The notion extends to wqos by considering the associated quotient wpos.

The maximal order types of the wqos used in this document can be computed using o(Q [START_REF] De Jongh | Well-partial orderings and hierarchies[END_REF]. Regarding Higman's Lemma and Kruskal's Theorem, the maximal order types were computed by [START_REF] Schmidt | Well-partial orderings and their maximal order types[END_REF], while the case of Robertson and Seymour's Graph Minor Theorem is still unsettled-but see [ [START_REF] Van Der Meeren | Connecting the Two Worlds: Well-partial-orders and Ordinal Notation Systems[END_REF] for recent advances.

, =) = |Q| for Q finite, o(A ⊔ B, ≤ ⊔ ) = o(A, ≤ A ) ⊕ o(B, ≤ B ), o(A × B, ≤ × ) = o(A, ≤ A ) ⊗ o(B, ≤ B ) [de
Maximal order types provide a measure of the 'strength' of wqos. They might however conceal some important distinctions; for instance o(N d , ≤ × ) = ω d = o(N d , ≤ lex ).

A.2. Subrecursive Functions

A.2.1. Monotonicity Properties. Assume h is monotone and inflationary. Then both h α and h α are monotone and inflationary [see [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF][START_REF] Schwichtenberg | Proofs and Computation[END_REF]L1]. However, those hierarchies are not monotone in the ordinal indices: for instance, H ω (x) = 2x+1 < 2x+2 = H x+2 (x) although ω > x + 2.

Some refinement of the ordinal ordering is needed in order to obtain monotonicity of the hierarchies. Define for this the pointwise ordering ≺ x at some x in N as the smallest transitive relation such that

α ≺ x α + 1 , λ(x) ≺ x λ . (A.2)
The relation 'β ≺ x α' is noted 'β ∈ α[x]' in [Schwichtenberg and Wainer, 2012, pp. 158-163]. The ≺ x relations form a strict hierarchy of refinements of the ordinal ordering <:

(A.3) ≺ 0 ⊊ ≺ 1 ⊊ • • • ⊊ ≺ x ⊊ • • • ⊊ < .

Algorithmic Complexity of Well-Quasi-Orders

Abstract. This document is dedicated to the algorithmic complexity of wellquasi-orders, with a particular focus on their applications in verification, where they allow to tackle systems featuring an infinite state-space, representing for instance integer counters, the number of active threads in concurrent settings, real-time clocks, call stacks, cryptographic nonces, or the contents of communication channels.

The document presents a comprehensive framework for studying such complexities, encompassing the definition of complexity classes suitable for problems with non-elementary complexity and proof techniques for both upper and lower bounds, along with several examples where the framework has been applied successfully. In particular, as a striking illustration of these applications, it includes the proof of the first known complexity upper bound for reachability in vector addition systems and Petri nets. Key words. Well-quasi-order, verification, infinite-state system, fast-growing complexity, vector addition system, Petri net.

Complexité algorithmique des beaux pré-ordres

Résumé. Ce document est consacré à l'étude de la complexité algorithmique des beaux pré-ordres, et se concentre particulièrement sur leurs applications en vérification, où ils permettent de raisonner sur des systèmes dotés d'une infinité d'états, car modélisant des variables à valeurs entières, un nombre de processus actifs non borné dans un contexte concurrent, des horloges à valeurs réelles dans un contexte temporisé, des piles d'appels de programmes récursifs, des nonces cryptographiques, ou encore des canaux de communication.

Le document présente un cadre théorique pour l'étude de telles complexités, qui inclut la définition de classes de complexité adaptées pour des problèmes de complexité non élémentaire, et des techniques pour établir des bornes supérieures ou inférieures de complexité, ainsi que des exemples pour lesquels ce cadre a pu être appliqué avec succès. En particulier, un exemple frappant de telles applications est celui du problème d'accessibilité dans les systèmes d'addition de vecteurs et les réseaux de Petri, pour lequel ce cadre fournit la première borne supérieure connue.

Mots clefs. Beaux pré-ordres, vérification, système infini, complexité à croissance rapide, système d'addition de vecteurs, réseau de Petri.

  The associated control-flow graph.

Figure 2 . 1 .

 21 Figure 2.1. A simple terminating program.

  A counter machine implementing Figure2.2a.

Figure 2 . 2 .

 22 Figure 2.2. The counter machine for Example 2.4.

  consider as their Example 3 a program computing the two-arguments Ackermann function: a (m, k ) = i f m = 0 then k + 1 e l s e i f k = 0 then a (m-1 , 1 ) e l s e a (m-1 , a (m, k -1 ) )

  Example 3.16 (Coverability in LCMs). Consider an instance of the coverability problem for a LCM with |Q| = p control states, |C| = d counters, and a target configuration q, v with max c∈C v(c) = n. As seen in Example 3.11, o(Q × N C ) = ω d • p.

Figure 4 . 1 .

 41 Figure 4.1. Some complexity classes beyond ELEMENTARY.

Theorem 4. 1 (

 1 Strictness). For all k and 2

Figure 4 . 2 .

 42 Figure 4.2. A Minsky machine M a implementing direct Hardylike computations as in equations (4.19) and (4.20).

Figure 4

 4 Figure 4.3. A Minsky machine M a -1 implementing inverse Hardy-like computations as in equations (4.21) and (4.22).

  and 4.3 with lossy semantics, we need to ensure that, if two valuations v and v ′ from N C d are such that v ≤ v ′ (for the product ordering), then (4.23)

Figure 4

 4 Figure 4.4. The LCM M d constructed in the proof of Theorem 4.9.

5. 1 . 2 . 1 .

 121 Petri Nets. A Petri net is a tuple N = ⟨P, T, W ⟩ where P is a finite set of places, T is a finite set of transitions, and W : (P × T ) ∪ (T × P ) → N is a (weighted) flow function. It defines a transition system with configurations in N P -i.e. multisets of places, also called markings-and steps m t -→ m ′ whenever m(p) ≥ W (p, t) and m ′ (p) = m(p) -W (p, t) + W (t, p) for all p in P . A Petri net can be encoded as an equivalent |P |-dimensional VASS with |T | + 1 states, and conversely a d-dimensional VASS can be encoded as an equivalent Petri net with d + 2 places (see Figure 5.3 for the result of this construction on the VASS of Figure 5.2, where places are depicted as circles, transitions as rectangles, and flows as arrows)-'equivalence' here should be understood as far as the decision problems like reachability are concerned.

  Sequences. We fix the VASS V = ⟨Q, d, T ⟩ under consideration. Let us first complete N with a top element ω and write N ω def = N ⊎ {ω} for the result; also let ω + z = z + ω = ω for all z in Z.

  shown in [C19, Section VII-C], these values can be analysed by considering the length of bad sequences over the nwqo (S × N d ) • d with maximal order type ω d • |S|d. The sequences are controlled with initial norm c def = ∥c in ∥ or c def = ∥c out ∥ depending on whether we are checking forward or backward pumpability, and by the function f (x) def = x + ∥T ∥ representing how fast the values can grow in the VASS. Choosing h(x) def = x + ∥T ∥d = H ∥T ∥d (x) fits the conditions of Theorem 3.15, and Equation (3.13) then provides a boundB ≤ h ω d •|S|d (cd) = (H ∥T ∥d ) ω d •|S|d (cd) ≤ H ω d •∥T ∥|S|d 2 (cd) (5.13) by Equation (3.12). Letting p(∥ξ∥) def = max(∥T ∥|S|d 2 , cd), B ≤ H ω d+1 (p(∥ξ∥)) . (5.14) By Lemma 4.4 and assuming d ≥ 2, ∥ξ ′ ∥ ≤ ∥ξ∥ • B d ≤ H ω d+1 (e(∥ξ∥)) for some elementary function e as advertised in (5.12).

S

  \ ↑t = D 0 ⊇ D 1 ⊇ • • • where D n+1 def = D n ∩ Pre ∀ (D n ) (6.1) using the universal predecessor set Pre ∀ (D) def = {s ∈ S | ∀s ′ ∈ S, (s → s ′ =⇒ s ′ ∈ D)} .(6.2)

  commutative and distributive:(ω 2 + ω) ⊕ ω 3 = ω 3 + ω 2 + ω, 2 ⊗ ω = ω • 2, and (ω + 2) ⊗ ω = ω 2 + ω • 2.A.1.1.2. Computing Order Types. The order types o(A, ≤ A ) of the well orders ⟨A, ≤ A ⟩ we already mentioned in this document are well-known:o([d], ≤) = d, o(N, ≤) = ω, o(A × B, ≤ lex ) = o(B, ≤ B ) • o(A, ≤ A ), and o(M(A), ≤ m ) = ω o(A,≤ A ) .By extension, we also write o(x, ≤) for the ordinal term in o(A, ≤) associated to an element x in A. Formally, this is the order type of the restriction of A to elements no larger thanx: o(x, ≤) def = o({y ∈ A | x ̸ ≤ y}, ≤). For instance in ⟨N d , ≤ lex ⟩, o((n 1 , . . . , n d ), ≤ lex ) = ω d-1 • n 1 + • • • + ω • n d-1 + n d .A.1.2. Maximal Order Types.[START_REF] De Jongh | Well-partial orderings and hierarchies[END_REF] extend the notion of order types to wpos ⟨A, ≤⟩:(A.1)o(A, ≤) def = sup{o(A, ⪯) | ⪯ is a linearisation of ≤} .

  ; I3].

	Contents
	2.1. Basic Definitions	10
	2.1.1. Well-Quasi-Orders	10
	2.1.1.1. Ascending Chain Condition	10
	2.1.1.2. Finite Basis Property	10
	2.1.1.3. Well-(Partial)-Orders	10
	2.1.2. Examples	11
	2.2. Application: Program Termination	11
	2.2.1. Ranking Functions	12
	2.2.1.1. Monolithic Ranking Functions	12
	2.2.1.2. Lexicographic Ranking Functions	13
	2.2.1.3. Ordinal Ranking Functions	13
	2.2.2. Quasi-Ranking Functions	13
	2.2.2.1. Termination by Quasi-Ranking	14
	2.2.2.2. Disjunctive Termination Arguments	14
	2.3. Application: Well-Structured Transition Systems	14
	2.3.1. Formal Definition	15
	2.3.2. Example: Lossy Counter Machines	15
	2.3.3. Verifying WSTS	16
	2.3.3.1. Coverability	16
	2.3.3.2. Backward Coverability	17
	2.3.3.3. Termination and Effectiveness of the Algorithm	17

  and (2) ≤ satisfies the finite antichain condition, i.e. there are no infinite sets of mutually ≤-incomparable elements in A. 2.1.1.1. Ascending Chain Condition. Another equivalent characterisation is that a qo ⟨A, ≤⟩ is a wqo if and only if any increasing sequence U

  1 over a wo is equivalent to requiring f (s) > f (s ′ ), and then implies by transitivity f (s) > f (s ′ ) whenever s → + s ′ .Proof. Let f be a quasi-ranking function of S into a wqo ⟨A, ≤⟩. Any sequence of configurations s 0 → s 1 → • • • of S is associated by f to a bad sequence f (s 0 ), f (s 1 ), . . . over A and is therefore finite. □

	2.2.2.1. Termination by Quasi-Ranking. The existence of a quasi-ranking func-
	tion always yields termination:
	Proposition 2.2. Given a transition system S = ⟨S, →⟩, if there exists a quasi-
	ranking function for S, then S terminates.
	Note that the converse statement also holds, as seen in §2.2.1.1.
	2.2.2.2. Disjunctive Termination Arguments. In order to prove a program tran-
	sition relation → to be well-founded,

  and the invited papers [I4; I3].

	Contents
	3.1. Controlling Bad Sequences	20
	3.1.1. Normed wqos	21
	3.1.2. Controlled Sequences	21
	3.1.2.1. Example: Controlled Quasi-Rankings	22
	3.1.2.2. Example: Controlled Minimal Predecessors	22
	3.1.3. Length Functions	22
	3.2. Subrecursive Hierarchies	23
	3.2.1. Fundamental Sequences and Predecessors	23
	3.2.2. Hardy and Cichoń Hierarchies	23
	3.3. Length Functions for Ordinals Below ε 0	24
	3.3.1. Residuals and a Descent Equation	25
	3.3.2. Upper Bounds	25
	3.4. Length Functions for Dickson's Lemma	26
	3.4.1. Polynomial Normed wqos	27
	3.4.2. Reflecting Normed wqos	27
	3.4.2.1. Inductive Reflection of Residuals	28
	3.4.2.2. Derivation Relation	28
	3.4.3. Maximal Order Types	29
	3.4.4. Upper Bounds	30
	3.5. Related Work & Perspectives	31
	3.5.1. Length Functions for Ordinals	31
	3.5.2. Length Functions for Well-Quasi-Orders	32
	3.5.3. Further Applications	32
	3.5.4. Perspectives	33

. Complexity Classes Beyond ELEMENTARY

  .

	4.1
	Contents
	4.1. Complexity Classes Beyond ELEMENTARY	36
	4.1.1. The Extended Grzegorczyk Hierarchy	36
	4.1.1.1. Computational Characterisation	36
	4.1.1.2. Main Properties	37
	4.1.1.3. Decision Problems	38
	4.1.2. The Fast-Growing Complexity Hierarchy	38
	4.1.2.1. Milestones	39
	4.1.2.2. Strictness	39

  As could be expected given the definitions, each class F α is closed both under many-one and Turing F <α reductions[START_REF] Schmitz | Complexity hierarchies beyond Elementary[END_REF] Theorems 4.7 and 4.8].

if there exists a Turing transducer T working in deterministic time f (n) such that, for all x, x is in A if and only if T (x) is in B. For a class of functions C, we write A ≤ C m B if there exists f in C such that A ≤ f m B. We write similarly that A ≤ f T B if there exists a Turing machine for A working in deterministic time f (n) with oracle calls to B, and A ≤ C T B if there exists f in C such that A ≤ f T B. Theorem 4.3. Let A and B be two languages with B

Table 4 .

 4 1. The complexity of Coverability in a few families of WSTS.

	WSTS	Complexity	Reference for lower bound
	Lossy Counter Machines F ω -complete

Table 5 .

 5 1. The complexity of a few VASS problems.

	Problem	Lower bound	Upper bound
	Reachability Reversible Reachability	EXPSPACE [Lipton, 1976] EXPSPACE	F ω 2 [Th. 5.1]

Somewhat oddly, the complexities above RECURSIVE are better explored and can rely on the arithmetical and analytical hierarchies.

Note that this is equivalent to defining h α+1 (x) def = h α (h(x)) and h λ (x) def = h λ(x) (x).

LENGTH FUNCTION THEOREMS

In terms of the extended Grzegorczyk hierarchy[START_REF] Löb | Hierarchies of number theoretic functions[END_REF]; see also Section 4.1.1], Clote places his bound at level F d+6 and McAloon's at level F d+1 for successor-controlled bad sequences in fixed dimension d; Theorem

3.15 provides an upper boundH ω d •d (dn) in F d in this case.

See the Decomposition Theorem in[C8] and Section 6.4.2 for a formal viewpoint.

Acknowledgements * I am indebted to a very large number of people who supported me on institutional, scientific, and personal levels while carrying this work.

Technical Appendix

A.1. Ordinals

From a set-theoretic perspective, an ordinal is an equivalence class of wellorders up to order isomorphism. We also employ ordinals, or rather ordinal terms denoting ordinals, in order to define subrecursive functions in Section 3.2.

A.1.1. Ordinals Terms. Ordinals in ε 0 can be canonically represented as ordinal terms α abstract syntax in Cantor normal form

We write as usual 1 for the term ω 0 and ω for the term ω 1 . Grouping equal exponents yields the strict form

the least solution of ω x = x, is the supremum of the ordinals presentable in this manner.

A. 1.1.1. Operations on Ordinal Terms. Thanks to the bijection between ordinal terms in CNF and ordinals below ε 0 , the usual ordinal operations can also be expressed 'syntactically' on ordinal terms. Later we will use terms as representatives for isomorphism classes of well orders with order types below ε 0 . We therefore include these syntactic characterisations here for the sake of completeness.

The ordinal ordering has a syntactic characterisation for ordinal terms in CNF:

∑ m j=1 ω β j if and only if there exists 1 ≤ j ≤ m such that α i = β i for all 1 ≤ i < j and either j ≤ p and α j < β j or j > p.

The direct sum α + β of two ordinals can also be defined on their CNFs α = ∑ p i=1 ω α i and β = ∑ m j=1 ω β j : thanks to the associativity of +, it suffices to consider ω αp + ω β 1 , which is already in CNF if α p ≥ β 1 , and is otherwise equated with ω β 1 . For instance ω 2 + ω + ω 3 = ω 2 + ω 3 = ω 3 ; note that the direct sum is not commutative. Similarly, the direct product α • β of α = ∑ p i=1 ω α i and β = ∑ m j=1 ω β j can be defined thanks to left distributivity as

• ω = ω 2 ; note that direct products are neither commutative nor right distributive.

The natural sum α ⊕ β of two ordinals with CNFs α = ∑ p i=1 ω α i and β = ∑ m j=1 ω β j can be defined as

Unlike the direct operations, the natural operations are As desired, our hierarchies are monotone for the pointwise ordering [START_REF] Cichoń | Ordinal recursive bounds for Higman's Theorem[END_REF][START_REF] Schwichtenberg | Proofs and Computation[END_REF]L1]: 2.1.1. Ordinal Norms. Recall the ordinal norm defined in Equation (3.4): the norm of an ordinal as the maximal coefficient that appears in its associated CNF, i.e. if α = ω α andc 1 , Lemma A.1 (Eventual Majoration). Let β < α be two ordinals and h be a monotone inflationary function. Then, for all x ≥ N β, h β (x) ≤ h α (x) and h β (x) ≤ h α (x).

List of Publications

Invited Papers