License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2010.192
URN: urn:nbn:de:0030-drops-28638
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2863/
Go to the corresponding LIPIcs Volume Portal

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

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

pdf-format:
17.pdf (0.5 MB)

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 =		{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
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI