Reachability in Continuous Pushdown VASS

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 non-negative rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen fraction 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. This is joint work with Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Contributed talk given by A. R. Balasubramanian

Authors

• A. R. Balasubramanian Technical University of Munich

Keywords

No keywords are indexed for this paper.