Petri net is an efficient model for concurrent systems. State space of a general Petri net is infinite. Even if it is finite, its size grows expornentially as the size of the net does. This problem, called state space explosion, makes Petri net analysis hard. Unfolding is suggested to give a compact description of the state space of a bounded Petri net. This is extended to unbounded net using ω borrowed from the coverability tree generating algorithm. However, using ω causes lack of information. On the other hand, if unbounded Petri net has a semilinear state space, it can be expressed without lack of information with extended coverability tree. This report suggests an extension of unfolding of Petri net with semilinear state space without lack of information.
展开▼
