The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.48
URN: urn:nbn:de:0030-drops-128605
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12860/
Go to the corresponding LIPIcs Volume Portal

Czerwiński, Wojciech ; Lasota, Sławomir ; Lazić, Ranko ; Leroux, Jérôme ; Mazowiecki, Filip

Reachability in Fixed Dimension Vector Addition Systems with States

pdf-format:
LIPIcs-CONCUR-2020-48.pdf (0.6 MB)

Abstract

The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability.
We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.

BibTeX - Entry

@InProceedings{czerwiski_et_al:LIPIcs:2020:12860,
  author =	{Wojciech Czerwiński and S{\l}awomir Lasota and Ranko Lazić and J{\'e}r{\^o}me Leroux and Filip Mazowiecki},
  title =	{{Reachability in Fixed Dimension Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{48:1--48:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12860},
  URN =		{urn:nbn:de:0030-drops-128605},
  doi =		{10.4230/LIPIcs.CONCUR.2020.48},
  annote =	{Keywords: reachability problem, vector addition systems, Petri nets}
}

Keywords: reachability problem, vector addition systems, Petri nets
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

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