Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One
复制标题
DOI：
10.4230/lipics.icalp.2017.119
复制
发表时间：
2017-04
期刊：
影响因子：
--
通讯作者：
Diego Figueira;R. Lazic;Jérôme Leroux;Filip Mazowiecki;G. Sutre
中科院分区：
文献类型：
--
作者：
Diego Figueira;R. Lazic;Jérôme Leroux;Filip Mazowiecki;G. Sutre
分支向量加法系统的可达性问题，或者等价于乘法指数线性逻辑的可证明性问题，是否可判定一直是一个悬而未决的问题。一维的情况下，是一个广泛研究的单计数器网络的推广，它是最近建立的多项式时间完全提供计数器更新在一元。我们的主要贡献是确定的复杂性时，编码是二进制：多项式空间完成。
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.