In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. 81-A, No. 4, pages 532-539. 1998.
Abstract: Unfolding originally introduced by McMillan is gaining ground as a partial-order method for the verification of concurrent systems without the explosion of the state space. However, it can be exposed to redundancy which may increase its size exponentially. So far, there have been trials to reduce such redundancy from conflicts by improving McMillan's cut-off criteria. This paper shows that concurrency is also another cause of redundancy in unfolding; an algorithm to reduce such redundancy in live, bounded and reversible Petri nets is presented which is independent of any cut-off algorithm.
Keywords: Petri nets, net unfolding, partial order semantics, state space explosion.