The decidability of the reachability problem for vector addition systems is a notoriously difficult result. First shown by Mayr in 1981 after a decade of unsuccessful attempts and partial results, its proof has been simplified and refined several times, by Kosaraju, Reutenauer, and Lambert, and re-proven by very different techniques by Leroux in 2012. The principles behind the original proof remained however obscure.

In this seminar, I will present the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness.

Joint work with Jérôme Leroux (LaBRI) presented at LICS’15; see http://arxiv.org/abs/1503.00745