A polynomial-time algorithm for reachability in branching VASS in dimension one
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 config...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
2016
|