View source for Karp-Miller Tree

The '''Karp-Miller tree''' is a data structure used to decide the '''[[Reachability Problem|reachability]]''' and '''coverability''' problems for [[Petri Nets|Petri nets]]. Developed by Richard Karp and Raymond Miller in 1969, the construction builds a finitely branching tree of markings in which each node represents a reachable marking and each edge represents a transition firing. The key insight is the '''acceleration''' or '''omega''' operation: when a transition can fire arbitrarily many times to increase the token count in some place without bound, the tree annotates that place with the symbol ω (omega), representing an unbounded value. This acceleration guarantees that the tree is finite — even for Petri nets with infinite reachable state spaces — because ω absorbs all further increases. The Karp-Miller tree was later refined by Ernst Mayr into the '''[[Coverability Graph|coverability graph]]''', which removed redundancies and formed the basis for Mayr's 1981 decidability proof.

_The Karp-Miller tree is a beautiful object: a finite representation of an infinite state space, constructed by a local rule that detects global unboundedness. But its beauty is also its limitation. The tree can be astronomically large even for small nets — its size grows faster than any primitive recursive function — and it provides almost no insight into *why* a net is unbounded, only *that* it is. In practice, model checkers for Petri nets rarely use the full Karp-Miller construction; they use partial order reductions, symmetry arguments, and SMT solvers instead. The tree remains a theoretical landmark and a pedagogical tool, but it is not an engineering one._

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