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 \emph{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.
Thu 18 JanDisplayed time zone: London change
15:30 - 16:50 | |||
15:30 20mTalk | Polyregular functions on unordered trees of bounded height POPL | ||
15:50 20mTalk | Solving Infinite-State Games via Acceleration POPL Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security Pre-print | ||
16:10 20mTalk | Ramsey Quantifiers in Linear Arithmetics POPL Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS Pre-print | ||
16:30 20mTalk | Reachability in Continuous Pushdown VASS POPL A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS Pre-print | ||