{\mathit{Var}}, G, {\mathit{Pre}},{\mathit{Post}})$ is *non-consuming* if for all $t\in T$, $p\in P$ and $x\in{\mathit{Var}}$ it holds that both 1) ${\mathit{Pre}}(t)(p,x) \le 1$, and 2) ${\mathit{Pre}}(t) \le {\mathit{Post}}(t)$.

In a non-consuming TPN, token multiplicities are irrelevant for discrete transitions. Intuitively, having one token $(p,{c})$ is equivalent to having an inexhaustible supply of such tokens.

The first condition is merely syntactic convenience. It asks that each transition takes at most one token from each place. The second condition in \[def:nonconsuming\] implies that for each discrete step $M{\longrightarrow_{t}}M'$ we have $M' \ge M$. Therefore, once a token $(p,{c})$ is present on a place $p$, it will stay there unchanged (unless time passes), and it will enable transitions with $(p,{c})$ in their precondition.

Wherever possible, we will from now on therefore allow ourselves to use the set notation for markings, that is simply treat markings $M\in{{(P{\times}{{\mathbb R}_{\geq 0}})}^\oplus}$ as sets $M\subseteq (P{\times}{{\mathbb R}_{\geq 0}})$.

Lower Bound {#sec:lowerbound}
===========

[$\mathsf{PSPACE}$]{}-hardness of [$\exists$COVER ]{}does not follow directly from the [$\mathsf{PSPACE}$]{}-completeness of the reachability problem in timed automata of [@AD:1994]. The non-consuming property of our TPN makes it impossible to fully implement the control-state of a timed automaton. Instead our proof uses multiple timed tokens and a 