论文标题
具有状态的二维矢量添加系统中的可及性:一个测试是免费的
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free
论文作者
论文摘要
与状态的矢量增加系统是一种无处不在的计算模型,并在计算机科学中广泛应用。矢量添加系统的可及性问题是中心的,因为许多其他问题降低了该问题。该问题是可决定的,最近证明了向量加法系统的维度是复杂性的重要参数。在大于两个大于两个的固定尺寸中,复杂性尚不清楚(具有巨大的复杂性差距)。在第二维度中,Blondin等人证明了可及性问题是Pspace-Complete。在2015年。我们考虑了该模型的扩展名,称为2-TVAS,可以在其中测试第一个计数器的零。该模型自然扩展了一个计数器自动机(OCA)的经典模型。我们表明,在多项式空间中仍然可以解决可及性的2-TVAS。与Blondin等人一样,我们的方法依赖于通过在多个多个周期中串联获得的少量可及性证书的存在。
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.