Unfoldings and Reachability Checking

An unfolding of a Petri net describes the net’s behaviour in a way that differs from its reachability graph. While a reachability graph has firing sequences as paths and describes reachable markings as nodes, and may be cyclic, an unfolding is always acyclic and describes firing sequences as linearisations of, and reachable markings as cuts through, a partial order. Causal dependencies can be detected in an unfolding more explicitly than in a reachability graph. Unfoldings allow polynomialtime reachability checks and are conducive to the application of various partial order specific verification techniques.