zbMATH — the first resource for mathematics

Polynomial-space completeness of reachability for succinct branching VASS in dimension one. (English) Zbl 1442.68136
Chatzigiannakis, Ioannis (ed.) et al., 44th international colloquium on automata, languages, and programming, ICALP 2017, Warsaw, Poland July 10–14, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 80, Article 119, 14 p. (2017).
Summary: 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.
For the entire collection see [Zbl 1373.68018].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
03F52 Proof-theoretic aspects of linear logic and other substructural logics
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI