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

2016/02/17 by Göller, Stefan, Haase, Christoph, Lazić, Ranko +1 · 1 citation
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1602.05547

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.

Cited by

• On the Reachability Problem for Two-Dimensional Branching VASS

Related

• On the Reachability Problem for Two-Dimensional Branching VASS
• Reachability for Bounded Branching VASS
• Reachability in Fixed VASS: Expressiveness and Lower Bounds
• Reachability in fixed dimension vector addition systems with states
• Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes