Place-Boundedness for Vector Addition Systems with one zero-test

Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zero-test. Surprisingly, place-boundedness remained open. We provide here a variation of the Karp-Miller algorithm to compute a basis of the downward closure of the reachability set which allows to decide place-boundedness. This forward algorithm is able to pass the zero-tests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zero-test), is undecidable. Keywords and phrases Vector addition systems; Inhibitor arcs; Karp-Miller algorithms; Reachability sets; Cover sets; Well-quasi orders.

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun
• Keywords: FSTTCS 2010, Karp-miller Algorithms, Reachability, Software Engineering, Vector Addition Systems