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

I propose to present recent and ongoing work on Branching Vector Addition System (BVASS), that extend Vector Addition Systems with special branching transitions like in tree automata. When performing a branching step, the counter values are distributed non-deterministically between two successor processes. 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. Our recent result is that the reachability, coverability and boundedness problems are polynomial-time complete for BVASS in dimension one. Regarding the reachability problem, this is the first decidability result in a subclass of BVASS known so far. This is joint work with Stefan G\”oller, Christoph Haase and Ranko Lazi\’c, to be published at ICALP’16 under the same name and also available here: http: //arxiv. org/abs/1602. 05547

Authors

• with Stefan Göller
• Christoph Haase
• Ranko Lazic

Keywords

No keywords are indexed for this paper.