In: Proc. of 1997 IEEE Systems, Man, and Cybernetics, 12-15 October 1997, Orlando, USA, pages 4274-4278. October 1997.
Abstract: Discrete event systems are modeled compactly by using Petri nets. Though Petri nets have powerful mathematical verification ability, in many cases, we have to construct the whole state space for verification. A reachability graph is one of representations of the state space. Petri nets can describe huge systems compactly, but then again sometimes it is impossible to generate the reachability graph because of an explosion of required computational time and space.
A Petri net is called a reversible net, when it can come back to the initial marking from any reachable marking. This paper considers a verification method of the reversibility. An unfolding is obtained by unfolding a Petri net, and it preserves reachability information of an original net and structural analysis on it is much easier than on the original net. This paper clears relations between unfoldings and the reversibility, and provides a verification method of the reversibility by using unfoldings.
Keywords: reversibility, unfolding.