2015/03/31 by Jérôme Leroux, Sylvain Schmitz · 2 citations
Computer Science · #cs.LO
paper · pdf · doi:10.1109/lics.2015.16
published as Proceedings of LICS 2015, pp. 56--67, IEEE Press · To appear in the Proceedings of LICS 2015
arxiv created 2015/05/13 · arxiv updated 2015/08/11
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, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability.