Complexité algorithmique des beaux pré-ordres

This document is dedicated to the algorithmic complexity of well-quasi-orders, with a particular focus on their applications in verification, where they allow to tackle systems featuring an infinite state-space, representing forinstance 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.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