2026-07-25T13:18:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20806 2024-08-29T05:40:58Z ddc:004 open_access

On Continuous Pushdown VASS in One Dimension Pérez, Guillermo A. Rao, Shrisha Vector addition systems Pushdown automata Reachability A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables. Unfortunately, reachability analysis, even for one-dimensional PVASS is not known to be decidable. So, we relax the model of one-dimensional PVASS to make the counter updates continuous and show that in this case reachability, coverability, and boundedness are decidable in polynomial time. In addition, for the extension of the model with lower-bound guards on the states, we show that coverability and reachability are NP-complete, and boundedness is coNP-complete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guillermo A. Pérez and Shrisha Rao 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.34 urn:nbn:de:0030-drops-208065 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.34 eng https://creativecommons.org/licenses/by/4.0/legalcode