Petri net termination Termination is the following problem.
Input: a Petri Net with initial marking
Output: "yes" iff there exists an infinite firing sequence. The naive algorithm in the case of bounded nets for example consists in running the net until either all configurations have been reached or a repeating one is found. Is there any clever way to solve the problem? What is the lower bound complexity?
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.