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

Rémi Bonnet, Alain Finkel, Jérôme Leroux & Marc Zeitoun
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.