Combinatorics and resource circuit-based enumeration of reachable states for S3PR

Reachability graphs can accurately reflect the state information of bounded Petri nets. However, the complexity of reachability graphs generation is exponential, which makes time waste and sometimes the computation may stop midway after a long time due to exhausted memory. Hence, this work presents combinatorics and resource circuit-based method to estimate the number of reachable states for a class of Petri nets-(SPR)-P-3. First, by combinatorics, an upper bound of reachable states of an (SPR)-P-3 can be calculated. The upper bound is the sum of reachable states and unreachable states. Hence, the next step is to obtain the number of unreachable states. By analysis, it is found that there exists a close relationship between resource circuits and the unreachable states. Therefore, the number of unreachable states of an (SPR)-P-3 can be found by extracting all the resource circuits. Finally, the resulting number of subtracting the number of unreachable states from the upper bound is the expected result. In addition, example calculation and analysis are given to show the effectiveness of the proposed method.