Liveness analysis of sequence control specifications described in capacity designated Petri net using reduction

The capacity designated Petri net (CPN), each of its places can have at most designated number of tokens, is a suitable model for describing real systems behavior. Liveness analysis of CPN is important to guarantee that a system described by using CPN is deadlock free. CPN liveness problem can be completely determined by reachability tree analysis, but reachability tree analysis needs a large amount of calculation time in propotion to net size power. In this paper, three reduction rules are proposed, which can be directly applied to the CPN model and preserves the liveness property of original net. The heuristic algorithms for realizing the reduction rules are also proposed and an example of reduction process using these algorithms is demonstrated. These algorithms have been experimentally applied to several CPN models which represent sequence control specifications, and their net sizes have become 1/2 - 1/10 compared with that of original nets.