Sciweavers

Share
FSTTCS
2010
Springer

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

9 years 7 months ago
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.
Rémi Bonnet, Alain Finkel, Jérô
Added 11 Feb 2011
Updated 11 Feb 2011
Type Journal
Year 2010
Where FSTTCS
Authors Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun
Comments (0)
books