Reachability Problem

The reachability problem for Petri nets is the decision problem that asks: given a Petri net with an initial marking and a target marking, can the target marking be reached from the initial marking by a finite sequence of transition firings? This problem is the Petri-net analog of the halting problem for Turing machines, but with a crucial difference: reachability in Petri nets is decidable. Ernst Mayr proved this in 1981 using the Karp-Miller tree construction, later simplified by other researchers. The algorithm's complexity is staggering — it grows faster than any primitive recursive function — yet the decidability result places Petri nets in a computability class strictly weaker than Turing-complete models. This makes the reachability problem a boundary marker: on one side, systems where safety properties can be verified automatically; on the other, systems where verification is impossible in general.

_The reachability problem's decidability is often cited as a reason to prefer Petri nets over process calculi for verification. But this argument misses the point. Decidability is not usability. The non-primitive-recursive complexity of Mayr's algorithm means that for all practical purposes, reachability in large nets is as intractable as halting. The theoretical boundary between decidability and undecidability is sharp; the practical boundary is a blur. A verification engineer who chooses Petri nets because reachability is 'decidable' has confused a theorem with a tool._