[John Baez wrote in #28](https://forum.azimuthproject.org/discussion/comment/17869/#Comment_17869):

> Yeah, like Jonathan I don't see how proving one particular problem that's known to take at least exponential space is in \$$\textsf{NP}\$$ would imply \$$\textsf{EXPSPACE} \subseteq \textsf{NP}\$$.
>
> I've never heard anything about Petri net reachability being \$$\textsf{EXPSPACE} \$$-complete. If it's true I wanna know!

My pithy argument was *too* pithy.

Fortunately, I have found some references.

Esparza et al. [*Decidability Issues for Petri Nets* (1994)](https://pdfs.semanticscholar.org/08f6/b004cd6e8cbf63b7a5e89398e3d208db1a0a.pdf) remark remark that Petri net reachability is \$$\textsf{EXPSPACE} \$$-complete for *symmetric* Petri nets. The write "loosely speaking, a Petri net is *symmetric* if for every transition \$$t\$$ there is a reverse transition
\$$t^\prime \$$ whose occurrence 'undoes' the effect of the occurrence of \$$t\$$". They quote the proof in Cardoza, Lipton and Meyer [*Exponential Space Complete Problems for Petri Nets and Commutative Semigroups* (1976)](https://dl.acm.org/citation.cfm?id=803630). Cardoza et al. call symmetric Petri nets *reversible*.

The wider class of reachability problems for arbitrary Petri nets must then *contain* \$$\textsf{EXPSPACE} \$$.

Moreover, \$$\textsf{NP} \subsetneq \textsf{EXPSPACE} \$$ - this is because it is a folk theorem that \$$\textsf{NP} \subseteq \textsf{PSPACE}\$$ and \$$\textsf{PSPACE} \subsetneq \textsf{EXPSPACE}\$$ by the hierarchy theorem.