Reachability in Continuous Pushdown VASS

on YouTube ↗25m

" summary

Proves reachability and even coverability for pushdown VASS with continuous semantics (counters are rationals scaled by any factor in (0,1]) is NEXPTIME-complete. Builds a NEXPTIME decision procedure (upper bound borrows continuous-VAS decomposition techniques) and a matching hardness reduction from bounded PCP via simulation of a runlength‑bounded 2-counter machine; hardness already holds for bounded stack, fixed dimension, and even unary numbers, while the algorithm tolerates binary-encoded numbers. Results are constructive and tight.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 1:49Vector Addition Systems
3. 3:15Pushdown VASS explained
4. 5:05Reachability and coverability
5. 8:38Reachability complexity in PVAS
6. 10:03Continuous PVAS approximation
7. 12:29Continuous reachability complexity
8. 13:54Lower bound proof overview
9. 16:50Conclusion and future
10. 17:37Question and answer session