$t$, (in both nets). Suppose $M_i{\xrightarrow{\rho}}$ is a path of length $(k-i)$ that ends in a $t$-transition. By the simulation property, there is such a path from every $m\cdot M_i$, $m>0$. Further, there must exist markings $M'_{i-1}\in\ {\downarrow\!{(}}{\mathbb{N}}\cdot M_{i-1})$ and $M'_{i}\in\ {\downarrow\!{(}}{\mathbb{N}}\cdot M_{i})$ such that $M'_{i-1}{\xrightarrow{}} M'_{i}$. It suffices to pick $M'_{i-1}{{\overset{\text{\tinydef}}{=}}}B\cdot M_{i-1}$, where $B\in{\mathbb{N}}$ is the maximal cardinality of any multiset ${\mathit{Pre}}(t)$ (This number is itself bounded by ${{\lvertP\rvert}}\cdot {{\lvert{\mathit{Var}}\rvert}}$ by our assumption on ${\mathit{Pre}}(t)$). We conclude that in ${\mathcal{N}}$ there is a path ending in a $t$-transition and starting in marking $(B\cdot k) \cdot M_0$, which is in ${\mathbb{N}}\cdot\{(p,{0})\}$.

Region Abstraction {#sec:regionabs}
------------------

We recall a constraint system called regions defined for timed automata [@AD:1994]. The version for TPN used here is similar to the one in [@AMM07].

Consider a fixed, nonconsuming TPN ${\mathcal{N}}=(P,T,{\mathit{Var}},G,{\mathit{Pre}},{\mathit{Post}})$. Let ${c_\mathit{max}}$ be the largest finite value appearing in transition guards $G$. Since different tokens with age $>{c_\mathit{max}}$ cannot be distinguished by transition guards, we consider only token ages below or equal to ${c_\mathit{max}}$ and treat the integer parts of older tokens as equal to ${c_\mathit{max}}+1$. Let ${{\it int}(c)}{{\overset{\text{\tinydef}}{=}}}\min\{{c_\mathit{max}}+1, \lfloor{c}\rfloor\}$ and ${{\it frac}(c)} {{\overset{\text{\tinydef}}{=}}}c-\lfloor{c}\rfloor$ for a real value $c\in{{\mathbb R}_{\geq 0}}$. We will work 