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

<p>The problem is decidable as follows.</p>

<p>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^*}$.</p>

<p>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}\}$. </p>

<p>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.</p>

<p>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}$.</p>

<p>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.</p>

CC BY-SA 3.0
2015-01-27T17:33:23.040Z
Great, thanks a lot!! This question was periodically coming back to my mind!
Nicolas Perrin
CC BY-SA 3.0
2015-01-27T17:36:29.943Z
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?
Nicolas Perrin
CC BY-SA 3.0
2015-01-26T22:06:15.180Z
2015-01-26T22:06:15.180Z
Jérôme
<p>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 <em>very</em> similar, so please accept his answer even if you consider mine correct.</p>

<hr>

<p>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, <strong>yes</strong>, the problem is decidable.</p>

<hr>

<p>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\}$.</p>

<p>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</p>

<ul>
<li>$\pi = t_1 \pi_1 t_1' \cdots t_{n+1} \pi_{n+1} t_{n+1}'$,</li>
<li>$\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})$</li>
<li>$p_0(\boldsymbol{u}_0) = p(\boldsymbol{u}),\ p_{n+1}(\boldsymbol{u}_{n+1}) = q(\boldsymbol{v})$,</li>
<li>$\forall i \in [1,n]\ \; \boldsymbol{u}_i \in {\downarrow}O \setminus O$.</li>
<li>$n \leq |Q| \cdot |{\downarrow}O|$.</li>
</ul>

<p>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: <img src="https://i.sstatic.net/aqGMR.png" alt="VASS gadget"></p>

CC BY-SA 3.0
2015-01-27T17:50:19.180Z
Thanks!! Two correct answers in less than 2 days, I have to say that this community works well :)
Nicolas Perrin
CC BY-SA 3.0
2015-01-27T00:54:21.800Z
2015-01-27T16:58:09.983Z
2015-01-27T16:58:09.983Z
Michael Blondin
<p>A Vector Addition System (VAS) is a finite set of <em>actions</em> $A \subset \mathbb{Z}^d$. $\mathbb{N}^d$ is the set of <em>markings</em>. 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 <em>reachable</em> from $m_0$.</p>

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

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

<p>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.</p>

<p><strong>EDIT</strong>. 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$?</p>

CC BY-SA 3.0
2015-01-26T11:43:17.417Z
do you have a good reference to get an intuition of the ideas behind the decidability proof ? (for instance slides)
Denis
CC BY-SA 3.0
2015-01-26T12:19:14.423Z
Here are slides: http://www.lsv.ens-cachan.fr/Events/Pavas/slides-Leroux.pdf; and a recent article: https://hal.archives-ouvertes.fr/hal-00674970; basically, reachability is solved by an enumeration algorithm, based on the fact that if $y$ is not reachable from $x$, then there exist two disjoint Presburger sets that somehow prove the non-reachability. Some other slides: http://automata.rwth-aachen.de/movep2010/abstracts/slides-leroux.pdf.
Nicolas Perrin
CC BY-SA 3.0
2015-01-26T12:23:28.077Z
M Praveen has given several talks on the two main approaches to the problem: http://cmi.ac.in/~praveenm/talks/
Sylvain
CC BY-SA 3.0
2015-01-26T12:27:10.397Z
For subcases of the problem with finite obstacles (e.g. with restricted dimension), it seems that a proof of decidability could be based on a "zigzag-elimination" property. See this paper: http://www.labri.fr/perso/leroux/published-papers/LS-concur04.ps, and these slides: http://www.labri.fr/perso/sutre/Talks/Documents/Flat2dimVASS:2004:CONCUR.pdf.
Nicolas Perrin
CC BY-SA 3.0
2015-01-28T07:41:20.817Z
For the state space $\mathbb{Z}^d$, the problem is easier :-) Since if you have non zero actions $a_1,\ldots,a_k$ that sums up to zero, it is possible to transform any run from $x$ to $y$ labeled by $\sigma$ to an other run from $x$ to $y$ labeled by $u^n\sigma v^n$ where $n\in\mathbb{N}$ and $u, v$ are word of actions with a zero total discplacement. In particular, if $x$ and $y$ are sufficiently
Jérôme
CC BY-SA 3.0
2015-01-29T16:52:04.370Z
I understand why the problem is solved when there are non zero actions that sum up to zero, but what happens when such actions do not exist? Part of your answer has been cut off from the comment :)
Nicolas Perrin
<fl.formal-languages><decidability>
Vector Addition Systems with finite "obstacles"
Nicolas Perrin
# Vector Addition Systems with finite "obstacles"

(Asked by: username_0 on 2015-01-24)

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 @username_3'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$?

**Tags:** fl.formal-languages, decidability

> **Comments:**
> **username_1**: do you have a good reference to get an intuition of the ideas behind the decidability proof ? (for instance slides)  
> **username_0**: Here are slides: http://www.lsv.ens-cachan.fr/Events/Pavas/slides-Leroux.pdf; and a recent article: https://hal.archives-ouvertes.fr/hal-00674970; basically, reachability is solved by an enumeration algorithm, based on the fact that if $y$ is not reachable from $x$, then there exist two disjoint Presburger sets that somehow prove the non-reachability. Some other slides: http://automata.rwth-aachen.de/movep2010/abstracts/slides-leroux.pdf.  
> **username_2**: M Praveen has given several talks on the two main approaches to the problem: http://cmi.ac.in/~praveenm/talks/  
> **username_0**: For subcases of the problem with finite obstacles (e.g. with restricted dimension), it seems that a proof of decidability could be based on a "zigzag-elimination" property. See this paper: http://www.labri.fr/perso/leroux/published-papers/LS-concur04.ps, and these slides: http://www.labri.fr/perso/sutre/Talks/Documents/Flat2dimVASS:2004:CONCUR.pdf.  
> **username_3**: For the state space $\mathbb{Z}^d$, the problem is easier :-) Since if you have non zero actions $a_1,\ldots,a_k$ that sums up to zero, it is possible to transform any run from $x$ to $y$ labeled by $\sigma$ to an other run from $x$ to $y$ labeled by $u^n\sigma v^n$ where $n\in\mathbb{N}$ and $u, v$ are word of actions with a zero total discplacement. In particular, if $x$ and $y$ are sufficiently  
> **username_0**: I understand why the problem is solved when there are non zero actions that sum up to zero, but what happens when such actions do not exist? Part of your answer has been cut off from the comment :)  

---

## 2 answers

### Answer by username_3 on 2015-01-26. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: Great, thanks a lot!! This question was periodically coming back to my mind!  
> **username_0**: 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?  

---

### Answer by username_4 on 2015-01-27. Score: 4

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 username_3'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](https://i.sstatic.net/aqGMR.png)

> **Comments:**
> **username_0**: Thanks!! Two correct answers in less than 2 days, I have to say that this community works well :)  

---

