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

TL;DR

This paper proves that the coverability problem becomes undecidable when a pushdown stack and reset instructions are combined in one-dimensional vector addition systems, highlighting the increased complexity of this model.

Contribution

It establishes the undecidability of coverability in one-dimensional pushdown vector addition systems with resets, a previously open problem.

Findings

Coverability is decidable without resets.

Coverability is undecidable with resets alone.

Undecidability is proven for the combined model.

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.

Tables

Table 1. Table 1 . Decidability status of the coverability and reachability problems in extensions of two-dimensional VASS; our contribution is indicated in bold.

$\mathbb{N}$	${\mathbb{N}}_{𝗋}$	${\mathbb{N}}_{𝗍}$	${\mathbb{N}}_{𝗓}$	$\mathrm{𝖯𝖣}$
D [7]	D [1]	D [4]	D [15]	D [12]	$\mathbb{N}$
	D [1]	D [4]	D [6]	U	${\mathbb{N}}_{𝗋}$
		D [4]	U [6]	U [6]	${\mathbb{N}}_{𝗍}$
			U [14]	U [14]	${\mathbb{N}}_{𝗓}$
				U	$\mathrm{𝖯𝖣}$

Table 2. (a) Coverability problem.

$\mathbb{N}$	${\mathbb{N}}_{𝗋}$	${\mathbb{N}}_{𝗍}$	${\mathbb{N}}_{𝗓}$	$\mathrm{𝖯𝖣}$
D [7]	D [1]	D [4]	D [15]	D [12]	$\mathbb{N}$
	D [1]	D [4]	D [6]	U	${\mathbb{N}}_{𝗋}$
		D [4]	U [6]	U [6]	${\mathbb{N}}_{𝗍}$
			U [14]	U [14]	${\mathbb{N}}_{𝗓}$
				U	$\mathrm{𝖯𝖣}$

Table 3. (b) Reachability problem.

$\mathbb{N}$	${\mathbb{N}}_{𝗋}$	${\mathbb{N}}_{𝗍}$	${\mathbb{N}}_{𝗓}$	$\mathrm{𝖯𝖣}$
D [9]	D [15]	D [15]	D [15]	??	$\mathbb{N}$
	D [6]	D [6]	D [6]	U	${\mathbb{N}}_{𝗋}$
		D [6]	U [6]	U [6]	${\mathbb{N}}_{𝗍}$
			U [14]	U [14]	${\mathbb{N}}_{𝗓}$
				U	$\mathrm{𝖯𝖣}$

Equations

$$R_{m_f}$$

$$R_{d_f}$$

$$R_{t_f}$$

$$\overrightarrow{R}$$

$$\overleftarrow{R}$$

$$(q_1,\perp u\#a^m,0)$$

$$s^{\prime }$$

$$\begin{matrix}m&R_{1}&\tilde{n}\\ &&\rotatebox[origin={c}]{-90.0}{$\geq$}\\ &&n\\ &&\rotatebox[origin={c}]{-90.0}{$>$}\\ \tilde{m}&R_{1}&n^{\prime}\\ \rotatebox[origin={c}]{-90.0}{$\geq$}&&\\ m^{\prime}&&\end{matrix}$$

$$\begin{matrix}m=p_{0}&\overrightarrow{R_{1}}\cdots\overrightarrow{R_{i}}&\tilde{p}_{i}&&\\ &&\rotatebox[origin={c}]{-90.0}{$>$}&&\\ &&p_{i}&\overrightarrow{R_{i+1}}\cdots\overrightarrow{R_{\ell}}&p_{\ell}\\ &&&&\rotatebox[origin={c}]{-90.0}{$=$}\\ m=q_{0}&\overleftarrow{R_{1}}\cdots\overleftarrow{R_{i}}&q_{i}&\overleftarrow{R_{i+1}}\cdots\overleftarrow{R_{\ell}}&q_{\ell}\end{matrix}$$

Full text

Keywords.  Pushdown vector addition systems; decidability

1. Introduction

Vector addition systems with states (VASS) play a central role for modelling systems that manipulate discrete resources, and as such provide an algorithmic toolbox applicable in many different fields. Adding a pushdown stack to vector addition systems yields so-called pushdown VASS (PVASS), which are even more versatile: one can model for instance recursive programs with integer variables [2] or distributed systems with a recursive server and multiple finite-state clients, and PVASS can be related to decidability issues in logics on data trees [8]. However, this greater expressivity comes with a price: the coverability problem for PVASS is only known to be decidable in dimension one [12]. This problem captures most of the decision problems of interest and in particular safety properties, and is the stumbling block in a classification for a large family of models combining pushdown stacks and counters [16].

Another viewpoint on one-dimensional PVASS [12] is to see those systems as extensions of two-dimensional VASS, where one of the two counters is replaced by a pushdown stack. In this context, a complete classification with respect to decidability of coverability, and of the more difficult reachability problem, was provided by Finkel and Sutre [6],

whether one uses plain counters ($\mathbb{N}$), counters with resets ($\mathbb{N}_{\mathsf{r}}$), counters whose contents can be transferred to the other counter ($\mathbb{N}_{\mathsf{t}}$), or counters with zero tests ($\mathbb{N}_{\mathsf{z}}$); see Table 1. In particular, two-dimensional VASS with one counter extended to allow resets and one extended to allow zero tests have a decidable reachability problem [6]: put differently, the coverability problem for one-dimensional PVASS with resets ($1$-PRVASS) is decidable if the stack alphabet is of the form $\{a,\bot\}$ where $\bot$ is a distinguished bottom-of-stack symbol.

Contributions.

In this note, we show that Finkel and Sutre’s decidability result does not generalise to one-dimensional pushdown VASS with resets over an arbitrary finite stack alphabet.

Theorem 1**.**

The coverability problem for $1$-PRVASS is undecidable.

As far as the coverability problem is concerned, this fully determines the decidability status in extensions of two-dimensional VASS where one may also replace counters by pushdown stacks ($\mathsf{PD}$); see Table 1(a).

Technically, the proof of Theorem 1 presented in Section 3 reduces from the reachability problem in two-counter Minsky machines. The reduction relies on the ability to weakly implement [13] basic operations—like multiplication by a constant—and their inverses—like division by a constant. This in itself would not bring much; for instance, plain two-dimensional VASS can already weakly implement multiplication and division by constants. The crucial point here is that, in a $1$-PRVASS, we can also weakly implement the inverse of a sequence of basic operations performed by the system, by using the pushdown stack to record a sequence of basic operations and later replaying it in reverse, and relying on resets to “clean-up” between consecutive operations. Note that without resets, while PVASS are known to be able to weakly implement Ackermannian functions already in dimension one [11], they cannot weakly compute sublinear functions [10]—like iterated division by two, i.e., logarithms.

2. Pushdown Vector Addition Systems with Resets

A ($1$-dimensional) pushdown vector addition system with resets ($1$-PRVASS) is a tuple $\mathcal{V}=(Q,\Gamma,A)$, where $Q$ is a finite set of states, $\Gamma$ is a finite set of stack symbols, and $A\subseteq Q\times I^{*}\times Q$ is a finite set of actions. Here, transitions are labelled by finite sequences of instructions from I\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.45}{{def}}}}}{{=}}}}\Gamma\cup\bar{\Gamma}\cup\{\mathsf{\mathord{+}},\mathsf{\mathord{-}},\mathsf{r}\} where \bar{\Gamma}\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.45}{{def}}}}}{{=}}}}\{\bar{z}\mid z\in\Gamma\} is a disjoint copy of $\Gamma$.

A $1$-PRVASS defines a (generally infinite) transition system acting over configurations $(q,w,n)\in Q\times\Gamma^{*}\times\mathbb{N}$. For an instruction $x\in I$, $w,w^{\prime}\in\Gamma^{\ast}$, and $n,n^{\prime}\in\mathbb{N}$, we write $(w,n)\xrightarrow{y}(w^{\prime},n^{\prime})$ in the following cases:

**push: **

if $x=z$ for $z\in\Gamma$, then $w^{\prime}=wz$ and $n^{\prime}=n$,

**pop: **

if $x=\bar{z}$ for $z\in\Gamma$, then $w=w^{\prime}z$ and $n^{\prime}=n$,

**increment: **

if $x=\mathsf{\mathord{+}}$, then $w^{\prime}=w$ and $n^{\prime}=n+1$.

**decrement: **

if $x=\mathsf{\mathord{-}}$, then $w^{\prime}=w$ and $n^{\prime}=n-1$, and

**reset: **

if $x=\mathsf{r}$, then $w^{\prime}=w$ and $n^{\prime}=0$.

Moreover, for a sequence of instructions $u=x_{1}\cdots x_{k}$ with $x_{1},\ldots,x_{k}\in I$, we have $(w_{0},n_{0})\xrightarrow{u}(w_{k},n_{k})$ if for some $(w_{1},n_{1}),\ldots,(w_{k-1},n_{k-1})\in\Gamma^{*}\times\mathbb{N}$, we have $(w_{i},n_{i})\xrightarrow{x_{i}}(w_{i+1},n_{i+1})$ for all $0\leq i<k$. Finally, for two configurations $(q,w,n),(q^{\prime},w^{\prime},n^{\prime})\in Q\times\Gamma^{*}\times\mathbb{N}$, we write $(q,w,n)\rightarrow_{\mathcal{V}}(q^{\prime},w^{\prime},n^{\prime})$ if there is an action $(q,u,q^{\prime})\in A$ such that $(w,n)\xrightarrow{u}(w^{\prime},n^{\prime})$.

The coverability problem for 1-PRVASS is the following decision problem.

**given: **

a 1-PRVASS $\mathcal{V}=(Q,\Gamma,A)$, states $s,t\in Q$.

**question: **

are there $w\in\Gamma^{*}$ and $n\in\mathbb{N}$ with $(s,\varepsilon,0)\rightarrow^{*}_{\mathcal{V}}(t,w,n)$?

3. Reduction from Minsky Machines

We present in this section a reduction from reachability in two-counter Minsky machines to coverability in 1-PRVASS.

3.1. Preliminaries

Recall that a two-counter (Minsky) machine is a tuple $\mathcal{M}=(Q,A)$, where $Q$ is a finite set of states and $A\subseteq Q\times\{0,1\}\times\{\mathsf{\mathord{+}},\mathsf{\mathord{-}},\mathsf{z}\}\times Q$ a set of actions. A configuration is a now triple $(q,n_{0},n_{1})$ with $q\in Q$ and $n_{0},n_{1}\in\mathbb{N}$. We write $(q,n_{0},n_{1})\rightarrow_{\mathcal{M}}(q^{\prime},n^{\prime}_{0},n^{\prime}_{1})$ if there is an action $(q,c,x,q^{\prime})\in A$ such that $n^{\prime}_{1-c}=n_{1-c}$ and

**increment: **

if $x=\mathsf{\mathord{+}}$, then $n^{\prime}_{c}=n_{c}+1$,

**decrement: **

if $x=\mathsf{\mathord{-}}$, then $n^{\prime}_{c}=n_{c}-1$, and

**zero test: **

if $x=\mathsf{z}$, then $n^{\prime}_{c}=n_{c}=0$.

The reachability problem for two-counter machines is the following undecidable decision problem [14].

**given: **

a two-counter machine $\mathcal{M}=(Q,A)$, and states $s,t\in Q$.

**question: **

does $(s,0,0)\rightarrow^{*}_{\mathcal{M}}(t,0,0)$ hold?

Gödel Encoding.

The first ingredient of the reduction is to use the well-known encoding of counter values $(n_{0},n_{1})\in\mathbb{N}\times\mathbb{N}$ as a single number $2^{n_{0}}3^{n_{1}}$; for instance, the pair $(0,0)\in\mathbb{N}\times\mathbb{N}$ is encoded by $2^{0}3^{0}=1$. In this encoding, incrementing the first counter means multiplying by $2$, decrementing the second counter means dividing by $3$, and testing the second counter for zero means verifying that the encoding is not divisible by $3$, etc. Note that, in each case, we encode the instruction as a partial function $g\colon\mathbb{N}\nrightarrow\mathbb{N}$; let us we define its graph as the binary relation R\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.45}{{def}}}}}{{=}}}}\{(m,n)\in\mathbb{N}\times\mathbb{N}\mid\text{g$is defined on$m$and$g(m)=n}\}. Thus the encoded instructions are the partial functions with the following graphs:

[TABLE]

for a factor $f\in\{2,3\}$. This means that we can equivalently see

• •

a two-counter machine with distinguished source and target states $s$ and $t$ as a regular language $M\subseteq\Delta^{*}$ over the alphabet \Delta\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.45}{{def}}}}}{{=}}}}\{m_{f},d_{f},t_{f}\mid f\in\{2,3\}\}, and

• •

reachability as the existence of a word $u=x_{1}\cdots x_{\ell}$ in the language $M$, with $x_{1},\dots,x_{\ell}\in\Delta$, such that the pair $(1,1)$ belongs to the composition $R_{x_{1}}R_{x_{2}}\cdots R_{x_{\ell}}$.

Weak Relations.

Here, the problem is that it does not seem possible to implement these operations (multiplication, division, divisibility test) directly in a $1$-PRVASS. Therefore, a key idea of our reduction is to perform the instructions of $u$ weakly—meaning that the resulting value may be smaller than the correct result—but twice: once forward and once backward. More precisely, for any relation $R\subseteq\mathbb{N}\times\mathbb{N}$, we define the weak forward and backward relations $\overrightarrow{R}$ and $\overleftarrow{R}$ by

[TABLE]

Let us call a relation $R\subseteq\mathbb{N}\times\mathbb{N}$ strictly monotone if for $(m,n)\in R$ and $(m^{\prime},n^{\prime})\in R$, we have $m<m^{\prime}$ if and only if $n<n^{\prime}$. We shall rely on the following Section, which is proven in Appendix A. {restatable}propositiontwoapprox If $R_{1},\ldots,R_{\ell}\subseteq\mathbb{N}\times\mathbb{N}$ are strictly monotone relations, then $R_{1}R_{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}}$.

We shall thus construct in Section 3.2 a $1$-PRVASS $\mathcal{V}$ in which a particular state is reachable if and only if there exists a word $u\in M$ with $u=x_{1}\cdots x_{\ell}$ and $x_{1},\ldots,x_{\ell}\in\Delta$, such that $(1,1)\in\overrightarrow{R_{x_{1}}}\cdots\overrightarrow{R_{x_{\ell}}}$ and $(1,1)\in\overleftarrow{R_{x_{1}}}\cdots\overleftarrow{R_{x_{\ell}}}$. Since the relations $R_{m_{f}}$, $R_{d_{f}}$, and $R_{t_{f}}$ for $f\in\{2,3\}$ are strictly monotone, Section 3.1 guarantees that this is equivalent to $(1,1)\in R_{x_{1}}\cdots R_{x_{\ell}}$. Intuitively, if we make a mistake in the forward phase $\overrightarrow{R_{x_{1}}}\cdots\overrightarrow{R_{x_{\ell}}}$, then at some point, we produce a number $n$ that is smaller than the correct result $\tilde{n}>n$. Then, the backward phase cannot compensate for that, because it can only make the results even smaller, and cannot reproduce the initial value.

3.2. Construction

We now describe the construction of our $1$-PRVASS $\mathcal{V}$. Its stack alphabet \Gamma\mathrel{\raisebox{-0.43057pt}{\stackrel{{\scriptstyle\raisebox{-0.75346pt}{\scalebox{0.45}{{def}}}}}{{=}}}}\Delta\cup\{\bot,\#,a\}. In $\mathcal{V}$, each configuration will be of the form $(q,\bot w\#a^{n},k)$, where $w\in\Delta^{*}$, and $n,k\in\mathbb{N}$. In the forward phase, we simulate the run of the two-counter machine so that $n$ is the Gödel encoding of the two counters. In order to perform the backward phase, the word $w$ records the instruction sequence of the forward phase. The resettable counter is used as an auxiliary counter in each weak computation step.

Gadgets.

For each weak computation step, we use one of the gadgets from Fig. 1; note that, for instance, “$+^{f}$” denotes the sequence of instructions $+\cdots+$ of length $f$. Observe that we have:

[TABLE]

and analogous facts hold for $\mathcal{D}_{f}$ and $\bar{\mathcal{D}}_{f}$ (with $d_{f}$ instead of $m_{f}$) and also for $\mathcal{T}_{f}$ and $\bar{\mathcal{T}}_{f}$ (with $t_{f}$ instead of $m_{f}$). Let us explain this in the case $\mathcal{M}_{f}$. In the loop at $q_{1}$, $\mathcal{M}_{f}$ removes $a$ from the stack and adds $f$ to the auxiliary counter. When $\#$ is on top of the stack the automaton moves to $q_{2}$ and changes the stack from $\bot u\#$ to $\bot um_{f}\#$. Therefore, once $\mathcal{M}_{f}$ is in $q_{2}$, it has set the counter to $f\cdot m$. In the loop at $q_{2}$, it decrements the counter and pushes $a$ onto the stack before it resets the counter and moves to $q_{3}$. Thus, in state $q_{3}$, we have $0\leq n\leq f\cdot m$.

Main Control.

Let $M\subseteq\Delta^{*}$ be accepted by the finite automaton $\mathcal{A}=(\Delta,Q,A,s,t)$. Schematically, our $1$-PRVASS $\mathcal{V}$ is structured as in the following diagram:

[TABLE]

The part in the dashed rectangle is obtained from $\mathcal{A}$ as follows. Whenever there is an action $(q,m_{f},q^{\prime})$ in $\mathcal{A}$, we glue in a fresh copy of $\mathcal{M}_{f}$ between $q$ and $q^{\prime}$, including $\varepsilon$-actions from $q$ to $q_{1}$ and from $q_{3}$ to $q^{\prime}$. The original action $(q,m_{f},q^{\prime})$ is removed. We proceed analogously for actions $(q,d_{f},q^{\prime})$ and $(q,t_{f},q^{\prime})$, where we glue in fresh copies of $\mathcal{D}_{f}$ and $\mathcal{T}_{f}$, respectively. Clearly, the part in the dashed rectangle realizes the forward phase as described above.

Once it reaches $t$, $\mathcal{V}$ can check if the current number stored on the stack equals $1$ and if so, move to state $b$. In state $b$, the backward phase is implemented. The $1$-PRVASS $\mathcal{V}$ contains a copy of $\bar{\mathcal{M}}_{f}$, $\bar{\mathcal{D}}_{f}$, and $\bar{\mathcal{T}}_{f}$ for each $f\in\{2,3\}$. Each of these copies can be entered from $b$ and goes back to $b$ when exited.

Finally, the stack is emptied by an action from $b$ to $t^{\prime}$, which can be taken if and only if the stack content is $\bot\#a$. We can check that from $(s^{\prime},\varepsilon,0)$, one can reach a configuration $(t^{\prime},w,m)$ with $w\in\Gamma^{*}$ and $m\in\mathbb{N}$, if and only if there exists $u\in M$, $u=x_{1}\cdots x_{\ell}$, and $x_{1},\ldots,x_{\ell}\in\Delta$, with $(1,1)\in\overrightarrow{R_{x_{1}}}\cdots\overrightarrow{R_{x_{\ell}}}\cap\overleftarrow{R_{x_{1}}}\cdots\overleftarrow{R_{x_{\ell}}}$. According to Section 3.1, the latter is equivalent to $(1,1)\in R_{x_{1}}\cdots R_{x_{\ell}}$.

4. Concluding Remarks

In this note, we have proven the undecidability of coverability in one-dimensional pushdown VASS with resets (c.f. Theorem 1). The only remaining open question in Table 1 regarding extensions of two-dimensional VASS is a long-standing one, namely the reachability problem for one-dimensional PVASS. Another fruitful research avenue is to pinpoint the exact complexity in the decidable cases of Table 1. Here, not much is known except regarding coverability and reachability in two-dimensional VASS: these problems are \PSPACE-complete if counter updates are encoded in binary [3] and \NL-complete if updates are encoded in unary [5].

Appendix A Proof of Section 3.1

It remains to prove Section 3.1. We will use the following lemma.

Lemma 2**.**

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^{\prime},n^{\prime})\in\overleftarrow{R_{1}}\cdots\overleftarrow{R_{\ell}}$. If $n^{\prime}\leq n$, then $m^{\prime}\leq m$. Moreover, if $n^{\prime}<n$, then $m^{\prime}<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^{\prime},n^{\prime})\in\overleftarrow{R_{1}}$. Then there are $\tilde{n}\geq n$ with $(m,\tilde{n})\in R_{1}$ and $\tilde{m}\geq m^{\prime}$ with $(\tilde{m},n^{\prime})\in R_{1}$. If $n^{\prime}<n$, then we have the following relationships:

[TABLE]

Since $R_{1}$ is strictly monotone, this implies $\tilde{m}<m$ and thus $m^{\prime}<m$. The case $n^{\prime}\leq n$ follows by the same argument.∎

We are now ready to prove Section 3.1.

\twoapprox

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_{1}R_{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\leq\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\leq\ell$.

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

[TABLE]

Since $p_{\ell}=q_{\ell}$, Lemma 2 applied to $R_{i+1},\dots,R_{\ell}$ implies $q_{i}\leq p_{i}$ and thus $q_{i}<\tilde{p}_{i}$. Applying Lemma 2 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\leq\ell$ and thus $(m,n)\in R_{1}\cdots R_{\ell}$.∎

Acknowledgements

Work partially funded by ANR-17-CE40-0028 Bra​VAS.