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.37
URN: urn:nbn:de:0030-drops-128498
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12849/
Go to the corresponding LIPIcs Volume Portal

Leroux, Jérôme ; Sutre, Grégoire

Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free

pdf-format:
LIPIcs-CONCUR-2020-37.pdf (0.5 MB)

Abstract

Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.

BibTeX - Entry

@InProceedings{leroux_et_al:LIPIcs:2020:12849,
  author =	{J{\'e}r{\^o}me Leroux and Gr{\'e}goire Sutre},
  title =	{{Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{37:1--37:17},
  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/12849},
  URN =		{urn:nbn:de:0030-drops-128498},
  doi =		{10.4230/LIPIcs.CONCUR.2020.37},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Infinite-state system}
}

Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Infinite-state system
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