Ideals of vector addition runs
More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical. This talk offers a justification for this decomposition technique, by showing that it emerges naturally in the study of the ideals of well quasi ordered sets.
Joint work with Jerome Leroux; paper to appear in LICS'15, available on arXiv: http://arxiv.org/abs/1503.00745
Sylvain Schmitz has been a lecturer at Ecole Normale Superieure de Cachan since 2008, and is a Leverhulme Trust visiting professor at the University of Warwick at present. He held a postdoc position at INRIA Nancy from 2007-2008, and obtained his PhD from the University of Nice - Sophia Antipolis in 2007.