2026-07-29T23:50:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6240 2024-03-06T10:37:51Z ddc:004 open_access

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One Göller, Stefan Haase, Christoph Lazic, Ranko Totzke, Patrick branching vector addition systems reachability coverability boundedness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Göller and Christoph Haase and Ranko Lazic and Patrick Totzke 2016 Is Part Of LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2016.105 urn:nbn:de:0030-drops-62409 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.105 eng https://creativecommons.org/licenses/by/3.0/legalcode