Complexité algorithmique des beaux pré-ordres
Sylvain Schmitz · HAL (Le Centre pour la Communication Scientifique Directe) · 2017
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.