next up previous
Next: Incremental Construction of Abstractions Up: New tools and techniques Previous: New tools and techniques

Efficient state-space exploration of Petri nets

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], the equivalence notion is essentially ``to have the same reachable markings''. Four solutions to the reachability problem are studied and compared experimentally. In [ES01a], a technique is presented for automatically simplifying the system before constructing the unfolding. This paper profits from reduction techniques for Petri nets well established in the literature, and shows that in the present setting they can be sharpened, leading to larger reductions.