Rackoff-Type Lemmata¶

Coverability and boundedness are two important problems on VASS that also provided insights to reachability problem. Karp and Miller¹ 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.

Build a tree initially with a single root $p(\mathbf{s})$.
Each time grow a leaf by adding all its direct successors as its children.
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}$.⁴

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} \]
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!

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

Rackoff's Original Lemma, Rephrased¶

Lemma

Let $G = (Q, T)$ be a d-VASS and $q(\mathbf{t})$ be a configuration. For any $p(\mathbf{s})$, if $q(\mathbf{t})$ is coverable from $p(\mathbf{s})$ then there is a run witnessing this fact with length bounded by $((|Q| + 1)M)^{d!^2}$ where $M := \max\{\Vert T \Vert, \Vert \mathbf{t} \Vert\}$.

Proof. We generalize the statement by allowing $\mathbf{s}$ ranging over $\mathbb{N}_\omega^d$. Suppose there is a run

\[ \pi: p(\mathbf{s}) \xrightarrow{*} q(\mathbf{t}') \ge q(\mathbf{t}) \]

Let $n$ be the number of non-$\omega$ components in $\mathbf{s}$. We will prove the lemma by induction on $n$. Let $C(p(\mathbf{s}))$ be the length of the shortest run covering $q(\mathbf{t})$ starting from $p(\mathbf{s})$. Let

\[ L_n := \sup_{\mathbf{s} \in \mathbb{N}_\omega^d}\{ C(p(\mathbf{s})) : \mathbf{s}\text{ has $n$ non-$\omega$ components}, C(p(\mathbf{s})) \ne \omega \} + 1 \]

Clearly we have $L_0 \le |Q|$, as a simple path from $p$ to $q$ works.

Claim

Let $M := \max\{\Vert T \Vert, \Vert \mathbf{t} \Vert\}$, we have

\[ L_{n+1} \le |Q| (M \cdot L_n)^{n+1} + L_n \]

Sub Proof. Let $\mathbf{s}_0 \in \mathbb{N}_\omega^d$ be of $n+1$ non-$\omega$ components from where $q(\mathbf{t})$ is coverable. We need to show that $C(p(\mathbf{s_0}))$ has the same bound. If on the shortest covering run, all the non-$\omega$ counters are bounded by $M \cdot L_n$ then we are done. Otherwise, suppose the first counter firstly exceeds the bound, we can decompose the run as

\[ \pi_0: p(\mathbf{s}_0) \xrightarrow{\pi_1} r(\mathbf{v}) \xrightarrow{\pi_2} q(\mathbf{t}') \ge q(\mathbf{t}) \]

So $|\pi_1| \le |Q| (M \cdot L_n)^{n+1}$ and $\mathbf{v}(1) > M \cdot L_n$. Let $\mathbf{v}_\omega$ be obtained from $\mathbf{v}$ by setting the first component to $\omega$. Then there is a path $\pi_2'$ from $r(\mathbf{v}_\omega)$ covering $q(\mathbf{t})$ of length bounded by $L_n - 1$, which is the induction hypothesis. Note that any prefix of $\pi_2'$ has effect $\Delta(\pi_2'[1..k])(1) \ge -M \cdot (L_n - 1)$, so

\[ \mathbf{v}(1) + \Delta(\pi_2'[1..k])(1) \ge M \ge \Vert \mathbf{t} \Vert \]

Therefore, $\pi_1 \circ \pi_2'$ is a run covering $q(\mathbf{t})$ from $p(\mathbf{s}_0)$, with length bounded by $|Q| (M \cdot L_n)^{n+1} + L_n$.

Sub Q.E.D.

Eventually we care about $L_d$. It's easy to show by induction that $L_d \le ((|Q| + 1)M)^{d!^2}$.

Q.E.D.

Rackoff Extraction by Leroux and Schmitz¶

From Rackoff's proof, we see that the core argument is: if one counter is raise up to a high value once, higher than what's needed by the remaining counters, we can discard this counter for the remaining short path. This inspiration leads to the following lemma by Leroux and Schmitz³.

Lemma

Let $G = (Q, T)$ be a $d$-VASS.

Assume there is a path $\rho$ from $p(\mathbf{s})$ to $q(\mathbf{t}_0)$ such that for every counter $j \in [d]$, $\rho$ contains a configuration $q_j(\mathbf{c}_j)$ such that $\mathbf{c}_j(j) \ge C^{1 + d^d}$ for a parameter $C \ge \text{size}_{\text{bin}}(G)$.
Then there is a path $\pi$ from $p(\mathbf{s})$ to $q(\mathbf{t})$ such that $\mathbf{t}(j) \ge C - \text{size}_{\text{bin}}(G)$ for all $i \in [d]$, and $|\pi| \le C^{(d+1)^{d+1}}$.

This is a consequence of the following finer lemma

Lemma

Let $G = (Q, T)$ be a $d$-VASS, $p(\mathbf{s})$ an $\omega$-configuration in $G$, $n$ be the number of non-$\omega$ components in $\mathbf{s}$.

Assume there is a path $\rho$ from $p(\mathbf{s})$ to $q(\mathbf{t}_0)$ such that for every counter $j \in [d]$, $\rho$ contains a configuration $q_j(\mathbf{c}_j)$ such that $\mathbf{c}_j(j) \ge C^{1 + n^n}$ for a parameter $C \ge \text{size}_{\text{bin}}(G)$.
Then there is a path $\pi$ from $p(\mathbf{s})$ to $q(\mathbf{t})$ such that $\mathbf{t}(j) \ge C - \text{size}_{\text{bin}}(G)$ for all $i \in [d]$, and $|\pi| \le C^{(n+1)^{n+1}}$.

Proof. We proceed by induction on $n$. Again the case $n = 0$ is trivial.

Richard M. Karp and Raymond E. Miller. 1969. Parallel program schemata. Journal of Computer and System Sciences 3, 2 (May 1969), 147–195. https://doi.org/10.1016/S0022-0000(69)80011-5 ↩
Charles Rackoff. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 2 (1978), 223–231. https://doi.org/10.1016/0304-3975(78)90036-1 ↩
Jérôme Leroux and Sylvain Schmitz. 2019. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In 2019 34^th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), June 2019. 1–13. https://doi.org/10.1109/LICS.2019.8785796 ↩
by $\mathbf{u}' > \mathbf{u}$ we mean $\mathbf{u}' \ge \mathbf{u}$ but $\mathbf{u}' \ne \mathbf{u}$. ↩