Method to improve unfolding in Petri nets

摘要

Petri net models, of systems, communication protocols, and software programs, which include place objects, transition objects, arcs, and initial markings, may be used for testing and verification. To reduce computations, a new unfolding process is performed on the net models. Two or more candidate buffer place interfaces are selected from the input net model. The input net is subdivided with a preliminary cut to form two subnets, wherein the preliminary cut passes through suitable candidate buffer place interfaces, objects of each of the subnets other than the suitable candidate buffer place interfaces are reachable from at least one initial marking, and the subnets do not include a mix of initial and non-initial marking places. Each of the two subnets are unfolded and then joined to form an unfolded net that is behaviorally equivalent to original input net model. The unfolded net is then stored in a storage unit.