English

Coverability is Undecidable in One-dimensional Pushdown Vector Addition Systems with Resets

Formal Languages and Automata Theory 2022-05-12 v1

Abstract

We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem. In the absence of resets, this problem is known to be decidable for one-dimensional pushdown vector addition systems, but decidability is open for general pushdown vector addition systems. Moreover, coverability is known to be decidable for reset vector addition systems without a pushdown stack. We show in this note that the problem is undecidable for one-dimensional pushdown vector addition systems with resets.

Cite

@article{arxiv.1906.07069,
  title  = {Coverability is Undecidable in One-dimensional Pushdown Vector Addition Systems with Resets},
  author = {Sylvain Schmitz and Georg Zetzsche},
  journal= {arXiv preprint arXiv:1906.07069},
  year   = {2022}
}

Comments

8 pages

R2 v1 2026-06-23T09:55:43.147Z