Yeah, like Jonathan I don't see how proving one particular problem that's known to take at least exponential space is in \$$\text{NP}\$$ would imply \$$\textrm{EXPSPACE} \subseteq \textrm{NP}\$$.

I've never heard anything about Petri net reachability being \$$\textrm{EXPSPACE} \$$-complete. If it's true I wanna know!