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.ICALP.2016.105
URN: urn:nbn:de:0030-drops-62409
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6240/
Go to the corresponding LIPIcs Volume Portal

Göller, Stefan ; Haase, Christoph ; Lazic, Ranko ; Totzke, Patrick

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

pdf-format:
LIPIcs-ICALP-2016-105.pdf (0.6 MB)

Abstract

Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.

BibTeX - Entry

@InProceedings{gller_et_al:LIPIcs:2016:6240,
  author =	{Stefan G{\"o}ller and Christoph Haase and Ranko Lazic and Patrick Totzke},
  title =	{{A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{105:1--105:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Ioannis Chatzigiannakis and Michael Mitzenmacher and Yuval Rabani and Davide Sangiorgi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6240},
  URN =		{urn:nbn:de:0030-drops-62409},
  doi =		{10.4230/LIPIcs.ICALP.2016.105},
  annote =	{Keywords: branching vector addition systems, reachability, coverability, boundedness}
}

Keywords: branching vector addition systems, reachability, coverability, boundedness
Collection: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
Issue Date: 2016
Date of publication: 23.08.2016

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