${\boldsymbol{v'}}=F^m({\boldsymbol{v}})$. This means that it suffices to add one transition $t$ with ${\mathit{Pre}}(t)=({\mathit{True}_{0}},0)$ whose enabledness witnesses the existence of a reachable encoding $M_{{\boldsymbol{v}}'}$ containing a token $({\mathit{True}_{0}},0)$. By the properties above, there exists $m\in{\mathbb{N}}$ with $F^m({\boldsymbol{v}})={\boldsymbol{v}}'$ and ${\boldsymbol{v}}'[0]=1$ iff $M_{{\boldsymbol{v}}}{\xrightarrow{*}}M_{{\boldsymbol{v}}'}{\xrightarrow{t}}$.

This lower bound holds even for discrete time TPN, e.g. [@EFR2000], because the proof uses only timed steps with duration $d=1$.

Upper Bound {#sec:upperbound}
===========

We start by observing that we can restrict ourselves, without loss of generality, to non-consuming TPN (\[def:nonconsuming\]) for showing the upper bound. Intuitively, since we start with an arbitrarily high number of tokens anyway, it does not matter how many of them are consumed by transitions during the computation, since some always remain.

[lemma]{}[lemnonconsuming]{} \[lem:mtpn:wlog\] \[lem:nonconsuming\] The [$\exists$COVER ]{} problem for TPN logspace-reduces to the [$\exists$COVER ]{}problem for non-consuming TPN. That is, for every TPN ${\mathcal{N}}$ and for every place $p$ and transition $t$ of ${\mathcal{N}}$, one can construct, using logarithmic space, a non-consumimg TPN ${\mathcal{N}}'$ together with a place $p'$ and transition $t'$ of ${\mathcal{N}}'$, so that there exists $M\in{\mathit{Cover}_{{\mathcal{N}}}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot\{(p,{0})\}{\aftergroup\egroup\originalright})}$ enabling $t$ in ${\mathcal{N}}$ if and only if there exists $M'\in{\mathit{Cover}_{{\mathcal{N}}'}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot\{(p',0)\}{\aftergroup\egroup\originalright})}$ that enables $t'$ in ${\mathcal{N}}'$.

First notice that the first condition in \[def:nonconsuming\], 