一句话：证明连续下推向量加法系统（PVASS）的可达性是 NEXPTIME 完全的，且对二进制/一元编码与有界栈等条件具有鲁棒性。
下推向量加法系统（PVASS）由有限控制状态、下推栈和一组只能增减、不能测试零的计数器组成；其可达性是否可判定是长期未解问题。本文研究连续 PVASS：计数器取有理数，每次加法前先将向量按任意有理因子（0 到 1 之间）缩放。作者证明连续 PVASS 的可达性问题是 NEXPTIME 完全的，并给出异常鲁棒的结果：即使所有数用二进制表示，也可在 NEXPTIME 内判定；而 NEXPTIME 困难性已对覆盖性成立，且在固定维数、有界栈、所有数用一元表示时仍成立。
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.
@article{paperbot2599,
title = {Reachability in Continuous Pushdown VASS},
author = {A. R. Balasubramanian and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3633279}
}