Skip to content

Research

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\).
Draft

Rackoff-Type Lemmata

Coverability and boundedness are two important problems on VASS that also provided insights to reachability problem. Karp and Miller1 designed the first algorithm for these two problems based on the Karp-Miller Coverability Tree. For a quick exposition, consider we are to decide whether \(p(\mathbf{s})\) can cover \(q(\mathbf{t})\). The algorithm construct a tree like follows.

  1. Build a tree initially with a single root \(p(\mathbf{s})\).
  2. Each time grow a leaf by adding all its direct successors as its children.

  3. After each growth check whether a self-covering path shows up on the tree, which is a path from some \(r(\mathbf{u})\) to \(r(\mathbf{u}')\) such that \(\mathbf{u}' > \mathbf{u}\).4

    Once such a path shows up (so \(r(\mathbf{u}')\) is a leaf), we replace \(\mathbf{u}'\) by the vector \(\mathbf{u}''\) where:

    \[ \mathbf{u}''(i) = \begin{cases} \mathbf{u}'(i) & \text{if } \mathbf{u}'(i) = \mathbf{u}(i)\\ \omega & \text{if } \mathbf{u}'(i) > \mathbf{u}(i)\\ \end{cases} \]

  4. We don't grow a leaf if its vector is \(\vec{\omega}\).

By Konig's Lemma this algorithm terminates, as there cannot be an infinite branch with no increasing pairs. To test coverability from this tree, just check if \(q(\mathbf{t})\) is covered by some vertex. Its correctness should be obvious. However, the complexity could be Ackermannian!

Rackoff2 designed a much more efficient algorithm for coverability and boundedness. What's more important is the underlying combinatorics constriction.

Farkas-Minkowski-Weyl Lemma for Open Cones

Recall the Farkas-Minkowski-Weyl Lemma states that

Theorem

A cone is polyhedra if and only if it is finitely generated.

where

  • a polyhedra cone is a cone given by

    \[ V = \{\mathbf{x} \in \mathbb{Q}^d : M \cdot \mathbf{x} \ge 0\} \]

    in which \(M \in \mathbb{Q}^{m \times d}\) is a rational matrix.

  • a finitely generated cone is given by

    \[ V = \{\mathbf{x} \in \mathbb{Q}^d : \mathbf{x} = R \cdot \mathbf{t} \text{ for some } \mathbf{t} \ge 0 \} \]

    in which the columns of \(R\) are the generators, and the coefficients have to be non-negative.

Using this fact, we can argue that any cone (for example, the cone generated by simple cycle effects in a VASS) can be represented as an intersection of finitely many half spaces. Note that a half space is a set given by a normal vector \(\mathbf{a}\):

\[ H = \{ \mathbf{x} \in \mathbb{Q}^d : \mathbf{a} \cdot \mathbf{x} \ge 0 \} \]

In the paper [CJLO25]1, the authors studied open cones, i.e. finitely generated cones where every coefficient must be positive:

\[ V^\circ = \{\mathbf{x} \in \mathbb{Q}^d : \mathbf{x} = R \cdot \mathbf{t} \text{ for some } \mathbf{t} > 0 \} \]

It was claimed that \(V^\circ\) is always an intersection of finitely many open half spaces, but the proof (only for \(d = 3\)) was vague. Here we consider it in more rigor.