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

Authors Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2010.192.pdf
  • Filesize: 0.49 MB
  • 12 pages

Document Identifiers

Author Details

Rémi Bonnet
Alain Finkel
Jérôme Leroux
Marc Zeitoun

Cite AsGet BibTex

Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 192-203, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/LIPIcs.FSTTCS.2010.192

Abstract

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
  • Place-boundedness
  • vector addition system with one zero-test
  • Karp-Miller algorithm

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail