View source for Reachability Problem

The '''reachability problem''' for [[Petri Nets|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 machine|Turing machines]], but with a crucial difference: reachability in Petri nets is '''decidable'''. Ernst Mayr proved this in 1981 using the '''[[Karp-Miller Tree|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._

[[Category:Computer Science]]
[[Category:Systems]]
[[Category:Mathematics]]