Petri net termination
Testing whether a Petri net $\mathcal{N} = (P, T, F)$ does not terminate from a marking $M_0$ can be decided by testing whether there exist a firing sequence $\sigma$ and markings $M, M'$ such that $M_0 \rightarrow^* M \rightarrow^\sigma M'$, $|\sigma| &gt; 0$ and $M' \geq M$. By [Rac78], if such a firing sequence exists, then there is one of length doubly exponential. Thus, it can be guessed non deterministically, which shows that the problem is in EXPSPACE. By [Lip76], the problem is EXPSPACE-hard and hence EXPSPACE-complete. See, e.g., Section 3.2.4 of these lecture notes for a presentation of Lipton's reduction.

[Rac78] Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223–231, 1978.

[Lip76] Richard J. Lipton. The reachability problem requires exponential space. Technical report 63, Department of Computer Science, Yale University, 1976.