[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.

> 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.