Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One
Diego Figueira, Ranko Lazić, Jérôme Leroux, Filip Mazowiecki, Grégoire Sutre · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2017
Whether the reachability problem for branching vector addition systems, or equivalently the provability problem for multiplicative exponential linear logic, is decidable has been a long-standing open question. The one-dimensional case is a generalisation of the extensively studied one-counter nets, and it was recently established polynomial-time complete provided counter updates are given in unary. Our main contribution is to determine the complexity when the encoding is binary: polynomial-space complete.