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

Almagor, Shaull ; Cohen, Nathann ; Pérez, Guillermo A. ; Shirmohammadi, Mahsa ; Worrell, James

Coverability in 1-VASS with Disequality Tests

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

Abstract

We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.

BibTeX - Entry

@InProceedings{almagor_et_al:LIPIcs:2020:12850,
  author =	{Shaull Almagor and Nathann Cohen and Guillermo A. P{\'e}rez and Mahsa Shirmohammadi and James Worrell},
  title =	{{Coverability in 1-VASS with Disequality Tests}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{38:1--38:20},
  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/12850},
  URN =		{urn:nbn:de:0030-drops-128501},
  doi =		{10.4230/LIPIcs.CONCUR.2020.38},
  annote =	{Keywords: Reachability, Vector addition systems with states, Weighted graphs}
}

Keywords: Reachability, Vector addition systems with states, Weighted graphs
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