Calculating place capacity for Petri nets using unfoldings
Toshiyuki Miyamoto, Satoshi Kumagai · 2002
Though Petri nets have powerful mathematical verification ability, we have to construct the state space in many cases. An upper bound of a place is the maximum number of tokens on the place for all reachable markings. We can find the upper bound by using a reachability graph or S-invariants. This paper proposes a method to find the upper bound by using an unfolding, and a comparison is made among these methods.