zbMATH — the first resource for mathematics

Place-boundedness for vector addition systems with one zero-test. (English) Zbl 1245.68131
Lodaya, Kamal (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2010), December 15–18, 2010, Chennai, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-23-1). LIPIcs – Leibniz International Proceedings in Informatics 8, 192-203, electronic only (2010).
Summary: 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.
For the entire collection see [Zbl 1213.68048].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI Link