Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for PVASS is a long-standing open problem. We consider continuous PVASS, which are PVASS with a continuous semantics. This means, the counter values are rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen rational factor between zero and one. We show that reachability in continuous PVASS is NEXPTIME-complete. Our result is unusually robust: Reachability can be decided in NEXPTIME even if all numbers are specified in binary. On the other hand, NEXPTIME-hardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary.

翻译：具有连续语义的下推向量加法系统（PVASS）由有限个控制状态、一个下推栈和一组可递增递减但不能检测零值的计数器组成。PVASS的可达性问题是否可判定是一个长期未解的开放问题。我们考虑连续PVASS，即具有连续语义的PVASS。这意味着计数器值为有理数，且当向量被添加到当前计数器值时，该向量首先与一个介于0和1之间任意选择的有理因子进行缩放。我们证明连续PVASS的可达性是NEXPTIME完全的。我们的结果具有异常鲁棒性：即使所有数字以二进制形式指定，可达性仍可在NEXPTIME内判定。另一方面，对于覆盖性问题，即使在固定维度、有界栈且所有数字以一元形式指定的情况下，NEXPTIME困难性依然成立。