DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.34

On Continuous Pushdown VASS in One Dimension

Authors: Guillermo A. Pérez and Shrisha Rao

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

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.

Cite as

Guillermo A. Pérez and Shrisha Rao. On Continuous Pushdown VASS in One Dimension. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CONCUR.2024.34,
  author =	{P\'{e}rez, Guillermo A. and Rao, Shrisha},
  title =	{{On Continuous Pushdown VASS in One Dimension}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{34:1--34:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.34},
  URN =		{urn:nbn:de:0030-drops-208065},
  doi =		{10.4230/LIPIcs.CONCUR.2024.34},
  annote =	{Keywords: Vector addition systems, Pushdown automata, Reachability}
}

Search Results

Documents authored by Rao, Shrisha

On Continuous Pushdown VASS in One Dimension

Abstract

Cite as

Thanks for your feedback!

Could not send message