License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-28638
URL:

; ; ;

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

pdf-format:


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.

BibTeX - Entry

@InProceedings{bonnet_et_al:LIPIcs:2010:2863,
  author =	{R{\'e}mi Bonnet and Alain Finkel and J{\'e}r{\^o}me Leroux and Marc Zeitoun},
  title =	{{Place-Boundedness for Vector Addition Systems with one zero-test}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{192--203},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2863},
  URN =		{urn:nbn:de:0030-drops-28638},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.192},
  annote =	{Keywords: Place-boundedness, vector addition system with one zero-test, Karp-Miller algorithm}
}

Keywords: Place-boundedness, vector addition system with one zero-test, Karp-Miller algorithm
Seminar: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue date: 2010
Date of publication: 2010


DROPS-Home | Fulltext Search | Imprint Published by LZI