provide a matching lower bound.

##### Our contribution.

We show that *Existential Coverability* (and thus universal safety) is decidable and [$\mathsf{PSPACE}$]{}-complete. This positively resolves an open question from [@ADM2004] regarding the decidability of universal safety in the controller-less networks. Moreover, a symbolic representation of the set of coverable configurations can be computed (using exponential space).

The [$\mathsf{PSPACE}$]{} lower bound is shown by a reduction from the iterated monotone Boolean circuit problem. (It does not follow directly from the [$\mathsf{PSPACE}$]{}-completeness of the reachability problem in timed automata of [@AD:1994], due to the lack of a central controller.)

The main ideas for the [$\mathsf{PSPACE}$]{} upper bound are as follows. First we provide a logspace reduction of the Existential Coverability problem for TPN to the corresponding problem for a syntactic subclass, non-consuming TPN. Then we perform an abstraction of the real-valued clocks, similar to the one used in [@AMM07]. Clock values are split into integer parts and fractional parts. The integer parts of the clocks can be abstracted into a finite domain, since the transition guards cannot distinguish between values above the maximal constant that appears in the system. The fractional parts of the clock values that occur in a marking are ordered 