VASS reachability in three steps

TL;DR

This paper provides an intuitive, three-step explanation of the decidability proof for VASS reachability, highlighting a condition that reduces problem complexity iteratively.

Contribution

It offers a simplified, conceptual overview of the key ideas in the classic VASS reachability proof, emphasizing the reduction technique through a specific condition.

Findings

Decidable condition Theta implies reachability.

Size reduction of VASS via negation of Theta.

Method applies to various VASS generalizations.

Abstract

This note is a product of digestion of the famous proof of decidability of the reachability problem for vector addition systems with states (VASS), as first established by Mayr in 1981 and then simplified by Kosaraju in 1982. The note is neither intended to be rigorously formal nor complete; it is rather intended to be an intuitive but precise enough description of main concepts exploited in the proof. Very roughly, the overall idea is to provide a decidable condition Theta on a VASS such that Theta implies reachability and its negation implies that the size of VASS can be reduced. With these two properties, the size of input can be incrementally reduced until the problem becomes trivial. We proceed in three steps: we first formulate the condition Theta for plain VASS, then adapt it to more general VASS with unconstrained coordinates, and finally to generalized VASS of Kosaraju.

Equations

$$(q,v)\stackrel{e}{⇝}(q^{\prime },v+z)$$

$$q^{\prime },v^{\prime }+m\Delta \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\text{fold}(\tau )-\text{fold}(\rho )\ge {\vec{1}}_E.$$

$$\text{fold}(\tau )-\text{fold}(\rho )-\text{fold}(\pi )-\text{fold}({\pi }^{\prime })\ge \vec{1}.$$

$$\text{fold}(\nu )=\text{fold}(\tau )-\text{fold}(\rho )-\text{fold}(\pi )-\text{fold}({\pi }^{\prime }).$$

$$(v\oplus w)(i)=\{\begin{array}{ll}v(i)& \text{ if }i\in C\\ w(i)& \text{ if }i\in B.\end{array}$$

$$\pi :$$

$${\pi }^{\prime }:$$

$${\pi }_0:$$

$${\pi }_1:$$

$$\pi :$$

$${\pi }^{\prime }:$$

$$\text{fold}(\nu )=\text{fold}({\pi }_1)-\text{fold}({\pi }_0)-\text{fold}(\pi )-\text{fold}({\pi }^{\prime }).$$

$$\textstyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}q^{\prime}},({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}v^{\prime}}+m\Delta)\oplus({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\bar{v}^{\prime}}+m(\bar{\delta}{+}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$

$${\mathcal{V}}_i=(d,E_i,Q_i,q_i,q_i^{\prime },R_i,r_i,C_i,U_i,C_i^{\prime },U_i^{\prime },v_i,v_i^{\prime })$$

$$\displaystyle\begin{aligned} &\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 31.09361pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-31.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{q_{1},r_{1}\oplus v_{1}\oplus u_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 55.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 55.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{q^{\prime}_{1},r_{1}\oplus v^{\prime}_{1}\oplus u^{\prime}_{1}\stackrel{{\scriptstyle e_{1}}}{{\leadsto}}}$}}}}}}}\ignorespaces}}}}\ignorespaces\\ &\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 31.09361pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-31.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{q_{2},r_{2}\oplus v_{2}\oplus u_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 55.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 55.09361pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{q^{\prime}_{2},r_{2}\oplus v^{\prime}_{2}\oplus u^{\prime}_{2}\stackrel{{\scriptstyle e_{2}}}{{\leadsto}}}$}}}}}}}\ignorespaces}}}}\ignorespaces\ \ldots\\ \ldots\stackrel{{\scriptstyle e_{l-1}}}{{\leadsto}}&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 31.55583pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-31.55583pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ q_{l},r_{l}\oplus v_{l}\oplus u_{l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 55.55583pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 55.55583pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ q^{\prime}_{l},r_{l}\oplus v^{\prime}_{l}\oplus u^{\prime}_{l}}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{aligned}$$

$$(u_1,f_1,u_1^{\prime },\dots ,u_l,f_l,u_l^{\prime })\in {\mathbb{N}}^k$$

Full text

VASS reachability in three steps

S. Lasota

This note is a product of digestion of the famous proof of decidability of the reachability problem for vector addition systems with states (VASS), as first established by Mayr [2, 3] and then simplified by Kosaraju [1]. The note is neither intended to be rigorously formal nor complete; it is rather intended to be an intuitive but precise enough description of main concepts exploited in the proof. Very roughly, the overall idea is to provide a decidable condition $\Theta$ on a VASS such that $\Theta$ implies reachability and $\neg\Theta$ implies that the size of VASS can be reduced. With these two properties, the size of input can be incrementally reduced until the problem becomes trivial. We proceed in three steps: we first formulate the condition $\Theta$ for plain VASS, then adapt it to more general VASS with unconstrained coordinates, and finally to generalized VASS of [1].

1 The reachability problem

A vector addition system with states (VASS) consists of a finite set of control states $Q$ and a finite set $E\subseteq Q\times\mathbb{Z}^{d}\times Q$ of arcs. The number $d\geq 1$ is the dimension of a VASS. A pseudo-configuration is a pair $(q,v)\in Q\times\mathbb{Z}^{d}$; it is a configuration if $v\in\mathbb{N}^{d}$. An arc $e=(q,z,q^{\prime})$ induces a step

[TABLE]

between pseudo-configurations. We write \textstyle{q,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}} if there is a sequence of steps from $(q,v)$ to $(q^{\prime},v^{\prime})$; every such sequence we call pseudo-run. We reserve this term for a sequence of steps, as well as for an (inducing) sequence of arcs. If all vectors appearing in a pseudo-run belong to $\mathbb{N}^{d}$ we call it run, and write \textstyle{q,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}} ; this implies in particular that $(q,v)$ and $(q^{\prime},v^{\prime})$ themselves are configurations. The aim of this note is to describe an algorithm for

VASS reachability problem:

[TABLE]

Sufficient condition

As a warm-up, we prove a sufficient condition for reachability. For a VASS and two configurations $(q,v)$, $(q^{\prime},v^{\prime})$, define the following two conditions:

1. $\Theta_{1}$:

For every $m\geq 1$, \textstyle{q,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}} by a pseudo-run that uses every arc at least $m$ times. 2. $\Theta_{2}$:

There are vectors $\Delta,\Delta^{\prime}\geq\vec{1}$ such that

[TABLE]

Proposition 1**.**

$\Theta_{1}\land\Theta_{2}$* implies \textstyle{q,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}} .*

Proof.

We will use the following claim, to be proved later:

Claim 1**.**

\textstyle{q^{\prime},\Delta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},\Delta^{\prime}} .

Here is a shape of a required run from $(q,v)$ to $(q^{\prime},v^{\prime})$:

[TABLE]

Observe that when $m$ increases, the three intermediate points also increase on all coordinates. Therefore, for a sufficiently large $m$, the two pseudo-runs become runs. ∎

Proof of Claim 1.

Consider the underlying graph of the VASS, whose vertices are control states and edges are arcs (note that there may be parallel edges). Every pseudo-run induces a path in the graph. For a pseudo-run from $(p,w)$ to $(p^{\prime},w^{\prime})$, we shortly speak of a pseudo-run from $p$ to $p^{\prime}$ when vectors $w,w^{\prime}$ are irrelevant. Let $E$ denote the set of arcs. By the folding of a pseudorun $\pi$ we mean the vector $\text{fold}(\pi)\in\mathbb{N}^{E}$ that says how many times every arc is used by $\pi$. The following lemma, roughly speaking, allows us to subtract one pseudo-run from another (it is proved using Eulerian equalities):

Lemma 1**.**

*Let $\tau,\rho$ be two pseudo-runs from $p$ to $p^{\prime}$ such that111 We write $\vec{m}_{C}$ for a constant vector in $\mathbb{Z}^{C}$ having $m$ on all coordinates. We prefer to omit the subscript $C$ and write simply $\vec{m}$ whenever this does not lead to confusion. *

[TABLE]

For every non-isolated control state $p^{\prime\prime}$ there is a pseudo-run $\sigma$ from $p^{\prime\prime}$ to $p^{\prime\prime}$ with $\text{fold}(\sigma)=\text{fold}(\tau)-\text{fold}(\rho)$.

By $\text{shift}(\pi)\in\mathbb{Z}^{d}$ we mean the effect of a pseudo-run $\pi$, namely the difference between its final vector and its initial one. Note that the shift of a pseudo-run is completely determined by its folding. To prove Claim 1, we need to show that there is a pseudo-run from $q^{\prime}$ to $q^{\prime}$ with shift $\Delta^{\prime}-\Delta$.

Basing on condition $\Theta_{1}$, we know that we can pick two pseudo-runs $\tau$, $\rho$ from $(q,v)$ to $(q^{\prime},v^{\prime})$ with arbitrarily large difference $\text{fold}(\tau)-\text{fold}(\rho)$. Fix (due to $\Theta_{2}$) a run $\pi$ from $(q,v)$ to $(q,v+\Delta)$, and a run $\pi^{\prime}$ from $(q^{\prime},v^{\prime}+\Delta^{\prime})$ to $(q^{\prime},v^{\prime})$. Then fix two pseudoruns $\tau$, $\rho$ from $(q,v)$ to $(q^{\prime},v^{\prime})$ such that

[TABLE]

Finally, apply Lemma 1 three times in a sequence, to deduce that there is a pseudo-run $\nu$ from $q^{\prime}$ to $q^{\prime}$ satisfying

[TABLE]

Indeed, $\text{shift}(\nu)=\text{shift}(\tau)-\text{shift}(\rho)-\text{shift}(\pi)-\text{shift}(\pi^{\prime})=\Delta^{\prime}-\Delta$ as required.

2 Partially unconstrained reachability problem

We now slightly generalize the reachability problem, and a sufficient condition. In the next section we will provide a yet further generalization that will be finally suitable for designing a decision procedure for reachability.

We will need a bit of concise notation. From now on we identify $\mathbb{Z}^{d}$ and $\mathbb{Z}^{\{1\ldots d\}}$; for instance, the set of configurations is $Q\times\mathbb{N}^{\{1\ldots d\}}$. For two disjoint subsets $C,B\in\{1\ldots d\}$ and two vectors $v\in\mathbb{Z}^{C}$ and $w\in\mathbb{Z}^{B}$, we write $v\oplus w$ for the unique vector in $\mathbb{Z}^{C\cup B}$ obtained by glueing together $v$ and $w$. Formally:

[TABLE]

From now on, by convention $\bar{C}$ will always denote the complement $\{1\ldots d\}-C$.

The generalization of the reachability problem amounts to considering only some subset $C\subseteq D$ of coordinates as constrained, while the remaining coordinates (i.e., those in $\bar{C}$) are considered unconstrained. The input and output configuration is specified only on constrained coordinates, and left unspecified on the remaining ones. Nevertheless, a run we ask for should remain nonnegative on all coordinates. Here is a precise formulation:

Partially unconstrained VASS reachability problem:

[TABLE]

We remark that we do not assume $C=C^{\prime}$. The setting of the previous section is the special case $C=C^{\prime}=\{1\ldots d\}$.

Sufficient condition

Here is a generalization of $\Theta_{1}$ and $\Theta_{2}$ to the more general setting. We write \textstyle{q,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{C}$$\textstyle{q^{\prime},v^{\prime}} , for $C\subseteq\{1\ldots d\}$, to say that there is a pseudo-run from $(q,v)$ to $(q^{\prime},v^{\prime})$ whose all vectors are non-negative on coordinates from $C$ (such pseudo-runs we call $C$-runs). We write shortly $\mathbb{N}_{\geq m}$ for $\mathbb{N}-\{0\ldots m-1\}$.

1. $\Theta_{1}$:

For every $m\geq 1$, there are some vectors $\bar{v}\in(\mathbb{N}_{\geq m})^{\bar{C}}$, $\bar{v}^{\prime}\in(\mathbb{N}_{\geq m})^{\bar{C}^{\prime}}$ such that

\textstyle{q,v\oplus\bar{v}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}\oplus\bar{v}^{\prime}} by a pseudo-run that traverses every arc at least $m$ times. 2. $\Theta_{2}$:

There are vectors $\Delta\in(\mathbb{N}_{\geq 1})^{C}$, $\Delta^{\prime}\in(\mathbb{N}_{\geq 1})^{C^{\prime}}$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}\in\mathbb{Z}^{\bar{C}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}}\in\mathbb{Z}^{\bar{C}^{\prime}} such that

[TABLE]

Proposition 2**.**

$\Theta_{1}\land\Theta_{2}$* implies \textstyle{q,v\oplus\bar{v}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}\oplus\bar{v}^{\prime}} for some vectors $\bar{v}\in\mathbb{N}^{\bar{C}}$, $\bar{v}^{\prime}\in\mathbb{N}^{\bar{C}^{\prime}}$.*

Proof.

The general idea of the proof is similar to the previous section, namely pumping up by a multiplicity of $\Delta$ (and de-pumping down by the same multiplicity of $\Delta^{\prime}$) in order to make some pseudorun \textstyle{q,v\oplus\bar{v}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}\oplus\bar{v}^{\prime}} into a run. The new difficulty is that pumping involves \Delta\oplus{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}, with {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}} possibly negative on some coordinates (and likewise for de-pumping). This issue is solved by starting from $v\oplus\bar{v}$, for a sufficiently large $\bar{v}\geq\vec{m}$.

We will need a couple of facts. The first one easily follows from $\Theta_{1}$:

Claim 2**.**

There are vectors $\bar{v}\in\mathbb{N}^{\bar{C}}$, $\bar{v}^{\prime}\in\mathbb{N}^{\bar{C}^{\prime}}$ and a pseudo-run

[TABLE]

such that for every $m>0$ there is a pseudo-run

[TABLE]

*with $\text{fold}(\pi_{1})-\text{fold}(\pi_{0})\geq\vec{m}_{E}$ and $\bar{\delta}\geq\vec{m}_{\bar{C}}$ and $\bar{\delta}^{\prime}\geq\vec{m}_{\bar{C}^{\prime}}$. *

In other words, $\pi_{0}$ and $\pi_{1}$ can be chosen to make the three vectors $\text{fold}(\pi_{1})-\text{fold}(\pi_{0})$,  $\bar{\delta}$ and $\bar{\delta}^{\prime}$ arbitrarily large on all coordinates. Therefore we conclude:

Claim 3**.**

The pseudo-runs $\pi_{0}$ and $\pi_{1}$ can be chosen so that:

• (a) 

\bar{\delta}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}\geq\vec{1}_{\bar{C}},   \bar{\delta}^{\prime}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}}\geq\vec{1}_{\bar{C}^{\prime}}

• (b) 

pseudo-runs in $\Theta_{2}$, lifted by $\vec{0}\oplus(\bar{v}+\bar{\delta})$ and $\vec{0}\oplus(\bar{v}^{\prime}+\bar{\delta}^{\prime})$, respectively, become runs:

[TABLE]

• (c) 

$\text{fold}(\pi_{1})-\text{fold}(\pi_{0})-\text{fold}(\pi)-\text{fold}(\pi^{\prime})\geq\vec{1}_{E}$.

Using Claim 3(a)–(b) together with the monotonicity of VASSes, we deduce that for an arbitrary $m>0$, the runs $\pi$ and $\pi^{\prime}$ can be repeated $m$ times when lifted further by $\vec{0}\oplus m\bar{\delta}$ and $\vec{0}\oplus m\bar{\delta}^{\prime}$, respectively:

Claim 4**.**

For every $m\geq 1$ it holds

[TABLE]

The last claim generalizes Claim 1 from the previous section.

Claim 5**.**

\textstyle{q^{\prime},\Delta\oplus(\bar{\delta}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},\Delta^{\prime}\oplus(\bar{\delta}^{\prime}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}})} .

Proof.

We have $\text{shift}(\pi_{1})-\text{shift}(\pi_{0})=(\vec{0}\oplus\bar{\delta}^{\prime})-(\vec{0}\oplus\bar{\delta})$ and \text{shift}(\pi)=\Delta\oplus{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}} and \text{shift}(\pi^{\prime})=(-\Delta^{\prime})\oplus(-{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}}). By Claim 3(c) we can apply Lemma 1 three times, to deduce that there is a pseudo-run $\nu$ from $q^{\prime}$ to $q^{\prime}$ satisfying

[TABLE]

We check: \text{shift}(\nu)=(\text{shift}(\pi_{1})-\text{shift}(\pi_{0}))-\text{shift}(\pi)-\text{shift}(\pi^{\prime})=\Delta^{\prime}\oplus(\bar{\delta}^{\prime}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}})-\Delta\oplus(\bar{\delta}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}), as required. ∎

We are now prepared to draw a shape of a required run (for readability, the primed items are depicted in blue):

[TABLE]

When $m$ increases, each of the three intermediate points increases on all coordinates. As a conclusion, for sufficiently large $m$, all the pseudo-runs become runs. ∎

Remark**.**

For the next section it is important to note that we have actually shown

\textstyle{q,v\oplus(\bar{v}+m\bar{\delta})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{q^{\prime},v^{\prime}\oplus(\bar{v}^{\prime}+m\bar{\delta}^{\prime})}

for all sufficiently large $m$.

3 Generalized reachability problem

We do now the last generalization in order to complete the decidability proof. By a component we mean a VASS $(d,Q,E)$ together with the following data:

• •

initial and final state $q,q^{\prime}\in Q$;

• •

subset of rigid coordinates $R\subseteq\{1\ldots d\}$; we assume that all arcs in $E$ have [math] on all coordinates in $R$ and hence, intuitively speaking, $d-|R|$ may be considered as the actual dimension of the component;

• •

rigid vector $r\in\mathbb{N}^{R}$;

• •

two partitions $\{1\ldots d\}-R=C\cup U=C^{\prime}\cup U^{\prime}$ of non-rigid coordinates into initial constrained coordinates $C$ and initial unconstrained coordinates $U$, and into final constrained coordinates $C^{\prime}$ and final unconstrained coordinates $U^{\prime}$;

• •

initial and final vector $v\in\mathbb{N}^{C}$, $v^{\prime}\in\mathbb{N}^{C^{\prime}}$.

Note that component does not essentially differ from the input of the partially unconstrained reachability problem from the previous section. The generalized VASS (GVASS) ${\cal G}$ consists of $l\geq 1$ components

[TABLE]

of the same dimension $d$, with pairwise disjoint state sets $Q_{i}$, and $l{-}1$ arcs of the form $e_{i}=(q^{\prime}_{i},z_{i},q_{i+1})$, where $z_{i}\in\mathbb{Z}^{d}$, for $i\in\{1\ldots i-1\}$. We will be interested in pseudo-runs $\pi$ from $q_{1}$ to $q^{\prime}_{l}$ of the following form:

[TABLE]

for some $u_{1}\in\mathbb{N}^{U_{1}},u^{\prime}_{1}\in\mathbb{N}^{U^{\prime}_{1}},\ldots,u_{l}\in\mathbb{N}^{U_{l}},u^{\prime}_{l}\in\mathbb{N}^{U^{\prime}_{l}}$. Each such pseudo-run $\pi$ passes through every arc $e_{i}$ exactly once, and thus splits into $l$ pseudo-runs $\pi=\pi_{1}e_{1}\pi_{2}e_{2}\ldots e_{l-1}\pi_{l},$ each $\pi_{i}$ being a pseudo-run in ${\cal V}_{i}$. When each of $\pi_{i}$ is a run, we call $\pi$ a run; if such a run exists we say that ${\cal G}$ admits reachability.

Generalized VASS reachability problem:

[TABLE]

The setting of the previous section is the special case of one component without rigid coordinates: $l=1$, $R_{1}=\emptyset$.

Sufficient condition

The condition $\Theta_{2}$ below is essentially the conjunction of conditions $\Theta_{2}$ of the previous section for each of the VASSes ${\cal V}_{i}$ separately; the only difference is taking rigid coordinates into account. On the other hand, the condition $\Theta_{1}$ below speaks jointly about all the VASSes ${\cal V}_{i}$.

1. $\Theta_{1}$:

For every $m\geq 1$, there is a pseudo-run from $q_{1}$ to $q^{\prime}_{l}$ of the form (1) that traverses every arc in every $E_{i}$ at least $m$ times, for some $u_{1}\in(\mathbb{N}_{\geq m})^{U_{1}},u^{\prime}_{1}\in(\mathbb{N}_{\geq m})^{U^{\prime}_{1}},\ldots,u_{l}\in(\mathbb{N}_{\geq m})^{U_{l}},u^{\prime}_{l}\in(\mathbb{N}_{\geq m})^{U^{\prime}_{l}}$. 2. $\Theta_{2}$:

For every $i\in\{1\ldots l\}$ there are vectors $\Delta\in(\mathbb{N}_{\geq 1})^{C_{i}}$, $\Delta^{\prime}\in(\mathbb{N}_{\geq 1})^{C^{\prime}_{i}}$, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta}}\in\mathbb{Z}^{U_{i}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\bar{\small\Delta^{\prime}}}\in\mathbb{Z}^{U^{\prime}_{i}} such that

[TABLE]

Observe that $\Theta_{1}$ implies $C^{\prime}_{i}=C_{i+1}$ for $i\in\{1\ldots l{-}1\}$. The sufficient condition for reachability is proved similarly as in the previous section:

Proposition 3**.**

If ${\cal G}$ satisfies $\Theta_{1}\land\Theta_{2}$ then ${\cal G}$ admits reachability.

Indeed, in Claim 2 one should consider all components simultaneously and recall the remark at the end of Section 2; for the other claims and the construction of a run, one can consider the components separately.

Furthermore, the sufficient condition can be effectively tested:

Proposition 4**.**

Both $\Theta_{1}$ and $\Theta_{2}$ are decidable.

Proof.

Pseudo-runs (1) can be encoded as the set of nonegative solutions of a system of linear Diophantine equations. Then condition $\Theta_{1}$ can be decided by inspecting the (hybrid-linear) set of solutions (cf. Claim 8 below). Checking condition $\Theta_{2}$ reduces to the coverability problem. ∎

Refinement

Let $\text{size}({\cal V}_{i})=(d-|R_{i}|,|E_{i}|,|U_{i}|+|U^{\prime}_{i}|)\in\mathbb{N}^{3}$. Thus the size of ${\cal V}_{i}$ is a triple consisting of: the number of non-rigid coordinates, the number of arcs, the number of unconstrained coordinates. For a GVASS ${\cal G}$, we define $\text{size}({\cal G})$ as the multiset of sizes of all components ${\cal V}_{i}$.

Order triples in $\mathbb{N}^{3}$ lexicographically. For two finite multisets of triples $m$ and $m^{\prime}$, we say that $m^{\prime}$ refines $m$ if $m^{\prime}$ is obtained by removing one triple from $m$, and replacing it by a finite number of lexicographically strictly smaller triples.

Claim 6**.**

The refinement relation is well-founded.

We shortly say that ${\cal G}^{\prime}$ refines ${\cal G}$ when $\text{size}({\cal G}^{\prime})$ refines $\text{size}({\cal G})$. We can assume wlog. that every component of ${\cal G}$ is strongly connected:

Claim 7**.**

If the underlying graph222We ignore here one inessential detail: this is a multigraph, i.e., parallel edges are allowed. of some component of ${\cal G}$ is not strongly-connected then one can compute ${\cal G}_{1}\ldots{\cal G}_{n}$ refining ${\cal G}$ such that ${\cal G}$ admits reachability if, and only if some of ${\cal G}_{1}\ldots{\cal G}_{n}$ does.

Indeed, it suffices to do the decomposition into strongly connected graphs.

For trivial ${\cal G}$, whose size contains only zero triples $(0,0,0)$, the reachability problems trivializes. Otherwise, either ${\cal G}$ satisfies $\Theta_{1}\land\Theta_{2}$ and thus admits reachability, or ${\cal G}$ can be refined:

Proposition 5**.**

If a non-trivial ${\cal G}$ violates $\Theta_{1}$ then one can compute ${\cal G}_{1}\ldots{\cal G}_{n}$ refining ${\cal G}$ such that ${\cal G}$ admits reachability if, and only if some of ${\cal G}_{1}\ldots{\cal G}_{n}$ does.

Proof.

Wlog. assume that the underlying graphs of all components ${\cal V}_{i}$ are strongly connected. Let $k=\sum_{i=1}^{l}|U_{i}|+E_{i}+|U^{\prime}_{i}|.$ Consider the set $L\subseteq\mathbb{N}^{k}$ of all vectors

[TABLE]

such that there is a pseudo-run $\pi=\pi_{1}e_{1}\pi_{2}e_{2}\ldots e_{l-1}\pi_{l}$ of the form (1) with $\text{fold}(\pi_{1})=f_{1}\geq\vec{1},\ldots,\text{fold}(\pi_{l})=f_{l}\geq\vec{1}$. The set $L$ is the set of nonnegative solutions of a system of linear Diophantine equations, and thus we have:

Claim 8**.**

One can compute finite sets $B,P\subseteq\mathbb{N}^{k}$ such that $L=B+P^{*}$.

Suppose ${\cal G}$ does not satisfy $\Theta_{1}$. Hence for some coordinate in $\{1\dots k\}$, all vectors in $P$ have zero on that coordinate. This zero coordinate corresponds either to some arc, or to some unconstrained (input or output) coordinate.

Suppose the first case holds, and let $e\in E_{i}$ be the arc corresponding to the zero coordinate. By Claim 8 one can compute a number $c$ such that every pseudo-run (1) passes through $e$ at most $c$ times. We refine ${\cal G}$ by $c+1$ GVASSes ${\cal G}_{0}\ldots{\cal G}_{c}$, each ${\cal G}_{m}$ obtained by replacing ${\cal V}_{i}$ by a sequence of $m+1$ copies of ${\cal V}_{i}-\{e\}$, i.e. of ${\cal V}_{i}$ without the arc $e$. The rigid coordinates and rigid vector of all copies are as in ${\cal V}_{i}$. The initial constrained coordinates of the first copy are $C_{i}$, the final constrained coordinates of the last copy are $C^{\prime}_{i}$, and the remaining initial or final constrained coordinates of all copies are empty sets. The initial vector of the first copy is $v_{1}$ and the final vector of the last copy is $v^{\prime}_{l}$; all other initial and final vectors are empty ones.

Now suppose the second case holds, i.e., the zero coordinate corresponds to some, say, initial unconstrained coordinate $j\in U_{i}$ (final unconstrained coordinate is treated symmetrically). By Claim 8 one can compute a number $c$ such that the value on coordinate $j$ in $u_{i}$ (cf. (8)) is at most $c$, for every pseudo-run $\pi$. We refine ${\cal G}$ by constraining the coordinate $j$ to some value in $\{0\ldots c\}$. We define $c+1$ refining GVASSes ${\cal G}_{0}\ldots{\cal G}_{c}$, where ${\cal G}_{m}$ differs from ${\cal G}$ only by making the coordinate $j$ in ${\cal V}_{i}$ an initial constrained coordinate, with value $m$. ∎

Proposition 6**.**

If a non-trivial ${\cal G}$ violates $\Theta_{2}$ then one can compute ${\cal G}_{1}\ldots{\cal G}_{n}$ refining ${\cal G}$ such that ${\cal G}$ admits reachability if, and only if some of ${\cal G}_{1}\ldots{\cal G}_{n}$ does.

Proof.

Wlog. assume that the underlying graphs of all components ${\cal V}_{i}$ are strongly connected. Suppose that ${\cal G}$ does not satisfy $\Theta_{2}$, i.e. condition (4) fails for some $i$ (condition (7) is treated symmetrically). Thus all initial constrained coordinates can not be simultaneously increased arbitrarily, which means that for some number $c$, in every pseudo-configuration reachable in ${\cal V}_{i}$ from $v_{i}\oplus\vec{0}$ via the relation $\scriptstyle{C_{i}}$ , some of initial constrained coordinates $j\in C_{i}$ is bounded by $c$. From the coverability tree for ${\cal V}_{i}$ one can extract $c$ with a stronger property:

Claim 9**.**

For every $C_{i}$-run $\pi$ in ${\cal V}_{i}$ from $v_{i}\oplus\vec{0}$ there is an initial constrained coordinate $j\in C_{i}$ which is bounded by $c$ in $\pi$.

Relying on the claim, we refine ${\cal G}$ by a finite family of GVASSes. For every $j\in C_{i}\cap C^{\prime}_{i}$ the family contains one GVASS ${\cal G}_{j}$, and for every $j\in C_{i}\cap U^{\prime}_{i}$ the family contains $c+1$ GVASSes ${\cal G}_{j,0}\ldots{\cal G}_{j,c}$, as outlined below:

$j\in C_{i}\cap U^{\prime}_{i}$:

Thus $j$ is a final unconstrained coordinate. We define GVASSes ${\cal G}_{j,0}\ldots{\cal G}_{j,c}$, where ${\cal G}_{j,m}$ differes from ${\cal G}$ only by making the coordinate $j$ a final constrained coordinate in ${\cal V}_{i}$, and fixing its value to $m$.

$j\in C_{i}\cap C^{\prime}_{i}$:

Thus $j$ is a final constrained coordinate. Let $a$ and $a^{\prime}$ be the values of initial and final vectors $v_{i}$, $v^{\prime}_{i}$ on coordinate $j$. We define ${\cal G}_{j}$ by replacing ${\cal V}_{i}$ with two components ${\cal V}^{\prime}$ and ${\cal V}^{\prime\prime}$. ${\cal V}^{\prime}$ behaves exactly as ${\cal V}_{i}$ with the only exception that the value of the $j$th coordinate is kept between [math] and $c$. This can be achieved using a cross-product of ${\cal V}_{i}$ with a finite state automaton, with states $\{0,\ldots,c\}$, the initial state $a$, the final state $a^{\prime}$, and transitions induced by the $j$th coordinate of arcs in $E_{i}$. This allows to set the $j$th coordinate of all arcs in ${\cal V}^{\prime}$ to [math]; in consequence, the coordinate $j$ can be moved to rigid coordinates of ${\cal V}^{\prime}$. Thus ${\cal V}^{\prime}$ has $(c+1)$ times more states and arcs than ${\cal V}_{i}$ but one less non-rigid coordinate. The rigid vector of ${\cal V}^{\prime}$ is set to $a$ on coordinate $j$. The difference $a^{\prime}-a$ is easily compensated by adding one arc-less component ${\cal V}^{\prime\prime}$ to ${\cal G}_{j}$, connected to ${\cal V}^{\prime}$ by an arc that adds $a^{\prime}-a$ on coordinate $j$ and preserves all other coordinates. ∎