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