Document Open Access Logo

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

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

PDF

File

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

Document Identifiers

Subject Classification

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
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Rémi Bonnet
Alain Finkel
Jérôme Leroux
Marc Zeitoun
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact