Near Reachability in 3-VASS¶

Let \(\mathbb{D}_{I, C}\) be the region defined by

\[ \mathbb{D}_{I, C} := \{ \mathbf{x} \in \mathbb{N}^3 : \exists i \in I, \mathbf{x}(i) \le C \} \]

The region \(\mathbb{D}_{\{1, 2, 3\}, C} =: \mathbb{D}_{C}\) is the region where at least one coordinate is less than or equal to \(C\).

We study the problem of reachability in 3-VASS where every configuration is constrained in the region \(\mathbb{D}_{I, C}\). Formally,

Definition

The Near Reachability Problem for 3-VASS asks: Given a 3-VASS \(G\) with configurations \(p(\mathbf{x}), q(\mathbf{y})\), and \(I \subseteq \{1, 2, 3\}\), \(C \in \mathbb{N}\) encoded in unary, does it hold that

\[ p(\mathbf{x}) \xrightarrow{*}_{\mathbb{D}_{I, C}} q(\mathbf{y}) \]

When \(|I| = 1\), the only counter in \(I\) can be encoded into the states, so the problem essentially becomes reachability in 2-VASS.

In this post we further show that the problem is

PSPACE-complete when \(|I| \le 2\),
undecidable (!) when \(|I| = 3\).

Near to 2 coordinate planes¶

Let's name the 3 counters by \(a, b, c\) and suppose \(I = \{a, b\}\). We reduce the near reachability problem to reachability in 2-VASS with one zero-testable counter, which is known to be in PSPACE. Notice that any configuration on the run has one counters of \(a, b\) bounded by \(C\). We can use the zero-testable counter to simulate either \(a\) or \(b\), and use the zero tests to shift between these roles.

Formally, let the 3-VASS \(G\) be \((Q, T)\). We construct a 2-TVASS \((Q_z, T_z)\) as follows:

\[ Q_z := \left\{ q_{a=\ell} | q \in Q, \ell \in [0, C] \right\} \cup \left\{ q_{b=\ell} | q \in Q, \ell \in [0, C] \right\}. \]

States \(q_{a = \ell}\) simulates the configurations where \(a\) is bounded, and the counters will record \(b\) and \(c\). States \(q_{b = \ell}\) has similar intuition. So we shall have the following transitions in \(T_z\):

\[ \begin{align*} p_{a=\ell} \xrightarrow{(b, c)} q_{a = \ell'} \text{ where } p \xrightarrow{(\ell' - \ell, b, c)} q \in T \\ p_{b=\ell} \xrightarrow{(a, c)} q_{b = \ell'} \text{ where } p \xrightarrow{(a, \ell' - \ell, c)} q \in T \end{align*} \]

To shift from, for example, \(q_{a = \ell}\) to \(q_{b = k}\), we can guess the value \(k <= C\) and use zero tests to verify our guess. This is realized by the following transitions:

\[ \begin{align*} q_{a = \ell} \xrightarrow{(-k, 0)} \bullet \xrightarrow[=0]{(+\ell, 0)} q_{b = k} \text{ for each } k \in [0, C]\\ q_{b = \ell} \xrightarrow{(-k, 0)} \bullet \xrightarrow[=0]{(+\ell, 0)} q_{a = k} \text{ for each } k \in [0, C] \end{align*} \]

It is then routine to verify that this new 2-TVASS simulates the \(\mathbb{D}_{I, C}\)-reachability relation correctly.

Near to 3 coordinate planes¶

We show that near reachability with \(I = \{a, b, c\}\) can simulates 2 counter machine, which is known to be Turing powerful. We use \(a, b\) to mimic the 2 counters in 2-CM, keeping \(c = 0\). Zero tests are simulated by the following program:

zero-test(a):
    b += C + 1; c += C + 1; a += C; 
    a -= C; c -= C + 1; b -= C + 1;

This shows the undecidability of near reachability where configurations can move in 3-regions near some axes plane.