Unfolding of Petri nets with semilinear reachability set

Petri net is an effective model for concurrent systems. The state space of a general Petri net is infinite. Even if it is finite, its size grows exponentially 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 an unbounded net using symbol ω used in the coverability tree generating algorithm. However, using ω causes lack of information. On the other hand, if the unbounded Petri net has a semilinear state space, it can be expressed without lack of information with an extended coverability tree. This paper suggests an extension of unfolding of Petri net with semilinear state space without lack of information.