The Edinburgh site is working on the development of the unfolding technique for state space exploration. In this technique a concurrent system, represented as a Petri net, is unfolded into a usually larger acyclic net, equivalent to the first one with respect to a suitable equivalence notion. Different notions are used, depending on the type of property considered. In [ES01b] (D1), the equivalence notion is essentially ``to have the same reachable markings''. Four solutions to the reachability problem are studied and compared experimentally. The paper [ES01a] (D1) presents a technique to automatically simplify the system before constructing the unfolding. The authors profit from reduction techniques for Petri nets well established in the literature, and show that in their setting these techniques can be sharpened, leading to larger reductions.