Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets

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.

Work partially funded by ANR-17-CE40-0028 BraVAS.

A Proof of Proposition 2

It remains to prove Proposition 2. We will use the following lemma.

Lemma 1

Let $R_1,\ldots ,R_\ell \subseteq \mathbb {N}\times \mathbb {N}$ be strictly monotone relations and $(m,n)\in \overrightarrow{R_1}\cdots \overrightarrow{R_\ell }$ and $(m',n')\in \overleftarrow{R_1}\cdots \overleftarrow{R_\ell }$. If $n'\le n$, then $m'\le m$. Moreover, if $n'<n$, then $m'<m$.

Proof

It suffices to prove the lemma in the case $\ell =1$: then, the general version follows by induction. Let $(m,n)\in \overrightarrow{R_1}$ and $(m',n')\in \overleftarrow{R_1}$. Then there are $\tilde{n}\ge n$ with $(m,\tilde{n})\in R_1$ and $\tilde{m}\ge m'$ with $(\tilde{m},n')\in R_1$. If $n'<n$, then we have the following relationships:

Since $R_1$ is strictly monotone, this implies $\tilde{m}<m$ and thus $m'<m$. The case $n'\le n$ follows by the same argument.    $\square$

We are now ready to prove Proposition 2.

Proposition 2

If $R_1,\ldots ,R_\ell \subseteq \mathbb {N}\times \mathbb {N}$ are strictly monotone relations, then $R_1R_2\cdots R_\ell =\overrightarrow{R_1}\overrightarrow{R_2}\cdots \overrightarrow{R_\ell }\cap \overleftarrow{R_1}\overleftarrow{R_2}\cdots \overleftarrow{R_\ell }$.

Proof

Of course, for any relation $R\subseteq \mathbb {N}\times \mathbb {N}$, one has $R\subseteq \overrightarrow{R}$ and $R\subseteq \overleftarrow{R}$. In particular, $R_1R_2\cdots R_\ell$ is included in both $\overrightarrow{R_1}\overrightarrow{R_2}\cdots \overrightarrow{R_\ell }$ and $\overleftarrow{R_1}\overleftarrow{R_2}\cdots \overleftarrow{R_\ell }$.

For the converse inclusion, suppose $(m,n)\in \overrightarrow{R_1}\overrightarrow{R_2}\cdots \overrightarrow{R_\ell }\cap \overleftarrow{R_1}\overleftarrow{R_2}\cdots \overleftarrow{R_\ell }$. Then there are $p_0,\ldots ,p_{\ell }\in \mathbb {N}$ with $p_0=m$, $p_\ell =n$, and $(p_{i-1},p_{i})\in \overrightarrow{R_i}$ for $0< i\le \ell$. There are also $q_0,\ldots ,q_{\ell }\in \mathbb {N}$ with $q_0=m$, $q_\ell =n$, and $(q_{i-1},q_{i})\in \overleftarrow{R_i}$ for $0<i\le \ell$.

Towards a contradiction, suppose that $(p_{i-1},p_i)\notin R_i$ for some $0<i\le \ell$. Then there is a $\tilde{p}_i>p_i$ with $(p_{i-1},\tilde{p}_i)\in R_i$. With this, we have

Since $p_\ell =q_\ell$, Lemma 1 applied to $R_{i+1},\dots ,R_\ell$ implies $q_i\le p_i$ and thus $q_i<\tilde{p}_i$. Applying Lemma 1 to $R_1,\dots ,R_i$ then yields $q_0<p_0$, a contradiction. Therefore, we have $(p_{i-1},p_i)\in R_i$ for every $0<i\le \ell$ and thus $(m,n)\in R_1\cdots R_\ell$.   $\square$