‘bad event’ of transition $t$ can never happen regardless of the number $m$ of processes, i.e., the network is safe for any size. Thus by checking existential coverability, one solves the dual problem of *Universal Safety*. (Note that the $m$ timed tokens/processes are only initially identical. They can develop differently due to non-determinacy in the transitions.)

The corresponding problem for timed networks studied in [@ADM2004] does not allow the dynamic creation of new timed processes (unlike the TPN model which can increase the number of timed tokens), but considers multiple clocks per process (unlike our TPN with one clock per token).

The TPN model above corresponds to a distributed network without a central controller, since initially there are no tokens on other places that could be used to simulate one. Adding a central controller would make *Existential Coverability* polynomially inter-reducible with normal *Coverability* and thus complete for $F_{\omega^{\omega^\omega}}$ [@HSS2012] (and even undecidable for $>1$ clocks per token [@ADM2004]).

Aminof et. al. [@ARZS2015] study the model checking problem of $\omega$-regular properties for the controller-less model and in particular claim an [$\mathsf{EXPSPACE}$]{} upper bound for checking universal safety. However, their result only holds for discrete time (integer-valued clocks) and they do not 