In: LNCS 2154: CONCUR 2001 - Concurrency Theory, pages 366-pp. 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings / K. G. Larsen, M. Nielsen (Eds.) --- Springer Verlag, 2001.
Abstract: Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings, which contain enough information to reason about the reachable markings of the original Petri nets. In this paper, we propose several improvements to the existing algorithms for generating finite complete prefixes of net unfoldings. Experimental results demonstrate that one can achieve significant speedups when transition presets of a net being unfolded have overlapping parts.
Keywords: Model checking, Petri nets, unfolding, concurrency..