A Vector Addition System (VAS) is a finite set of actions $A \subset \mathbb{Z}^d$. $\mathbb{N}^d$ is the set of markings. A run is a non-empty word of markings $m_0 m_1\dots m_n$ s.t. $\forall i \in \{0, \dots, n-1\}, m_{i+1}-m_i \in A$. If such a word exists we say that $m_n$ is reachable from $m_0$.

The problem of reachability for VASs is known to be decidable (but its complexity is an open problem).

Now let us assume that a finite set of forbidden markings (the obstacles) is given. I would like to know if the problem of reachability is still decidable.

Intuitively, the finite set of obstacles should interfere with paths only locally, so the problem should remain decidable. But it does not seem trivial to prove it.

EDIT. I will keep @Jérôme's answer as the accepted one, but I would like to add a follow-up question: what if the set of markings is $\mathbb{Z}^d$?


The idea is based on a discussion I got with Grégoire Sutre this afternoon.

The problem is decidable as follows.

A Petri net $T$ is a finite set of pairs in $\mathbb{N}^d\times\mathbb{N}^d$ called transitions. Given a transition $t=(\vec{u},\vec{v})$, we denote by $\xrightarrow{t}$ the binary relation defined on the set of configurations $\mathbb{N}^d$ by $\vec{x}\xrightarrow{t}\vec{y}$ if there exists a vector $\vec{z}\in\mathbb{N}^d$ such that $\vec{x}=\vec{u}+\vec{z}$ and $\vec{y}=\vec{v}+\vec{z}$. We denote by $\xrightarrow{T}$ the one step reachability relation $\bigcup_{t\in T}\xrightarrow{t}$. The reflexive and transitive closure of this relation is denoted by $\xrightarrow{T^*}$.

Let $\leq$ be the classical componentwise partial order over $\mathbb{N}^d$ and defined by $\vec{u}\leq \vec{x}$ if there exists $\vec{z}\in\mathbb{N}^d$ such that $\vec{x}=\vec{u}+\vec{z}$. The upward closure of a set $\vec{X}$ of $\mathbb{N}^d$ is the set ${\uparrow}\vec{X}$ of vectors $\{\vec{v}\in\mathbb{N}^d \mid \exists \vec{x}\in\vec{X}.\,\vec{x}\leq\vec{v}\}$. The downward closure of a set $\vec{X}$ is the set ${\downarrow}\vec{X}$ of vectors $\{\vec{v}\in\mathbb{N}^d \mid \exists \vec{x}\in\vec{x}.\,\vec{v}\leq\vec{x}\}$.

Notice that if $\vec{U}={\uparrow}\vec{B}$ for some finite set $\vec{B}$ of $\mathbb{N}^d$ and if $T$ is a Petri net, we can compute a new Petri net $T_{\vec{B}}$ such that for every configurations $\vec{x},\vec{y}$, we have $\vec{x}\xrightarrow{T}\vec{y}$ and $\vec{x},\vec{y}\in\vec{U}$ if, and only if, $\vec{x}\xrightarrow{T_{\vec{B}}}\vec{y}$. In fact, if $t=(\vec{u},\vec{v})$ is a transition, then for each $\vec{b}\in\vec{B}$, let $t_{\vec{b}}=(\vec{u}+\vec{z},\vec{v}+\vec{z})$ where $\vec{z}$ is the vector in $\mathbb{N}^d$ defined componentwise by $\vec{z}(i)=\max\{\vec{b}(i)-\vec{u}(i),\vec{b}(i)-\vec{v}(i),0\}$ for every $1\leq i\leq d$. Notice that $T_{\vec{U}}=\{t_{\vec{b}} \mid t\in T\,\vec{b}\in\vec{B}\}$ satisfies the requirement.

Now, assume that $T$ is a Petri net, $\vec{O}$ the set of obstacle. We introduce the finite set $\vec{D}={\downarrow}\vec{O}$. Observe that we can compute effectively a finite set $\vec{B}$ of $\mathbb{N}^d$ such that ${\uparrow}\vec{B}=\mathbb{N}^d\backslash\vec{D}$. Let $R$ be the binary relation defined over $\mathbb{N}^d\backslash \vec{O}$ by $\vec{x} R \vec{y}$ if $\vec{x}=\vec{y}$, or there exists $\vec{x}',\vec{y}'\in \mathbb{N}^d\backslash \vec{O}$ such that $\vec{x}\xrightarrow{T}\vec{x}'\xrightarrow{T_{\vec{B}}^*}\vec{y}'\xrightarrow{T}\vec{y}$.

Now, just observe that if there exists a run from the initial configuration $\vec{x}$ to the final one $\vec{y}$ that avoid the obstacle $\vec{O}$, then there exists one that avoid the obstacle in $\vec{O}$ and that passes by configurations in $\vec{D}\backslash \vec{O}$ at most the cardinal of that set. Hence, the problem reduces to select non-deterministically distinct configurations $\vec{c}_1,\ldots,\vec{c}_n$ in $\vec{D}\backslash \vec{O}$, fix $\vec{c}_0$ as the initial configuration $\vec{x}$, $c_{n+1}$ as the final one $\vec{y}$, and check that $\vec{c}_j R \vec{c}_{j+1}$ for every $j$. This last problem reduces to classical reachability questions for Petri nets.

  • $\begingroup$ Great, thanks a lot!! This question was periodically coming back to my mind! $\endgroup$ – Nicolas Perrin Jan 27 '15 at 17:33
  • 2
    $\begingroup$ Now, it might be obvious, but I'd like to ask a follow-up question, to be sure. What if we allow $\mathbb{Z}^d$ to be the set of markings? In that case, the exact same construction does not work. Is there a simple argument that extends the result? $\endgroup$ – Nicolas Perrin Jan 27 '15 at 17:36

I've been thinking about your question for vector addition systems with states (VASS) which are equivalent to VAS and came up with this solution. Now, I've read Jérôme's nice answer and I have to say that my answer is very similar, so please accept his answer even if you consider mine correct.

Idea: It is possible to convert a VASS $V$ into a VASS $V'$ that forbids vectors smaller or equal to the obstacles. This is not exactly what we want, since vectors smaller but not equal to the obstacles are allowed to be reached. However, there are finitely many such vectors. This allows a decomposition of minimals runs into finitely many runs that are either a transition of $V$ or an equivalent run of $V'$. Therefore, yes, the problem is decidable.

Details: Let $V=(Q,T)$ be a $d$-VASS, i.e. $V$ is a finite labelled graph such that $T \subseteq Q \times \mathbb{Z}^d \times Q$. Let $O \subseteq \mathbb{N}^d$ be the set of obstacles. Let $\pi ­\in T^*$ and $X \subseteq \mathbb{N}^d$, we write $p(\boldsymbol{u}) \xrightarrow{\pi}_X q(\boldsymbol{v})$ whenever $\pi$ is a run from $p(\boldsymbol{u})$ to $q(\boldsymbol{v})$ with every intermediate configuration in $Q \times X$. We denote ${\downarrow}X = \{\boldsymbol{y} : \boldsymbol{y} \leq \boldsymbol{x} \text{ for some } \boldsymbol{x} \in X\}$.

Let $\pi$ be a minimal run such that $p(\boldsymbol{u}) \xrightarrow{\pi}_{\mathbb{N}^d \setminus O} q(\boldsymbol{v})$, i.e. a minimal run that avoids the obstacles. Then, by the pigeonhole principle, $\pi$ can be factorized as a run that enters ${\downarrow}O \setminus O$ only finitely many times. More formally, there exist $t_1, t_1' \ldots, t_{n+1}, t_{n+1}' \in T \cup \{\varepsilon\}$, $\pi_1, \ldots, \pi_{n+1} \in T^*$ and $\{p_i(\boldsymbol{u}_i), q_i(\boldsymbol{v}_i), r_i(\boldsymbol{w}_i)\}_{i \in [0,n+1]} \subseteq Q \times \mathbb{N}^d$ such that

  • $\pi = t_1 \pi_1 t_1' \cdots t_{n+1} \pi_{n+1} t_{n+1}'$,
  • $\forall i \in [0,n]\ \; p_i(\boldsymbol{u}_i) \xrightarrow{t_{i+1}}_{\mathbb{N}^d} q_{i+1}(\boldsymbol{v}_{i+1}) \xrightarrow{\pi_{i+1}}_{\mathbb{N}^d \setminus {\downarrow}O} r_{i+1}(\boldsymbol{w}_{i+1}) \xrightarrow{t_{i+1}'}_{\mathbb{N}^d} p_{i+1}(\boldsymbol{u}_{i+1})$
  • $p_0(\boldsymbol{u}_0) = p(\boldsymbol{u}),\ p_{n+1}(\boldsymbol{u}_{n+1}) = q(\boldsymbol{v})$,
  • $\forall i \in [1,n]\ \; \boldsymbol{u}_i \in {\downarrow}O \setminus O$.
  • $n \leq |Q| \cdot |{\downarrow}O|$.

Therefore, it suffices to guess $n$, $t_1, t_1', \ldots, t_{n+1}, t_{n+1}'$ and the intermediate configurations. Testing whether $p(\boldsymbol{x}) \xrightarrow{*}_{\mathbb{N}^d \setminus {\downarrow}O} q(\boldsymbol{y})$ can be carried out by converting $V$ into a new $d$-VASS $V'$ where each transition $t \in T$ is replaced by a gadget of $4|O|+1$ transitions. For example, if $O = \{(1,5), (2,3)\}$ then the transitions are replaced as follows: VASS gadget

  • 1
    $\begingroup$ Thanks!! Two correct answers in less than 2 days, I have to say that this community works well :) $\endgroup$ – Nicolas Perrin Jan 27 '15 at 17:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.