where for all $p\in P$ and $c\in{{\mathbb R}_{\geq 0}}$, $$\begin{aligned}
        \pi({\mathit{Pre}}(t))(p,c){{\overset{\text{\tinydef}}{=}}}\sum_{\pi(v)=c} {\mathit{Pre}}(t)(p,v)
        \qquad
        \text{and}
        \qquad
        \pi({\mathit{Post}}(t))(p,c){{\overset{\text{\tinydef}}{=}}}\sum_{\pi(v)={c}} {\mathit{Post}}(t)(p,{v}).
    \end{aligned}$$ A transition $t\in T$ is called *enabled* in marking $M$, if there exists an evaluation $\pi$ that satisfies $G(t)$ and such that $\pi({\mathit{Pre}}(t))\le M$. In this case, there is a discrete step $M{\longrightarrow_{t}}M'$ from marking $M$ to $M'$, defined as $
        M' = M \ominus \pi({\mathit{Pre}}(t)) \oplus \pi({\mathit{Post}}(t)).
        $

\[def:mtpn:tsteps\] Let $M$ be a marking and $d\in {{\mathbb R}_{\geq 0}}$. There is a time step $M{\longrightarrow_{d}}M'$ to the marking $M'$ with $M'(p,{c}){{\overset{\text{\tinydef}}{=}}}M(p,{c}-{d})$ for ${c}\ge{d}$, and $M'(p,{c}){{\overset{\text{\tinydef}}{=}}}0$, otherwise. We also refer to $M'$ as $(M+d)$.

We write ${\xrightarrow{}_{\textit{Time}}}$ for the union of all timed steps, ${{\xrightarrow{}_{\textit{Disc}}}}$ for the union of all discrete steps and simply ${\xrightarrow{}}$ for ${{\xrightarrow{}_{\textit{Disc}}}}\cup{{\xrightarrow{}_{\textit{Time}}}}{}$. The transitive and reflexive closure of ${\xrightarrow{}}$ is ${\xrightarrow{*}}$. ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}(M{\aftergroup\egroup\originalright})}$ denotes the set of markings $M'$ for which there is an $M''\ge M'$ with $M{\xrightarrow{*}}M''$.

We are interested in the *existential coverability problem* ([$\exists$COVER ]{} for short), as follows.

[ ]{}

We show that this problem is [$\mathsf{PSPACE}$]{}-complete. Both lower and upper bound will be shown (w.l.o.g., see \[lem:mtpn:wlog\]) for the syntactic subclass of *non-consuming* TPN, defined as follows.

\[def:nonconsuming\] A *timed Petri net* $(P,T, 