The Substitution Properties Of Petri Nets Based On Workflow

As a modeling and analyzing tool for distributed system, Petri nets are widely used in the fields of communication, traffic, manufacturing, and automatic control, to make research of problem like design of the controller, analyze of the deadlock prevention, and liveness preservation, and fairness preservation. While the complexity of system increases, the complexity of the Petri net model increases accordingly, and the state space explosion problem is produced: even a small increase, may bring the explosion of state space, and result in the difficulty in analyzing. To overcome this problem, academy often uses the idea of refinement, which is an up to down modeling method, layered simulation, and step-wise process, and can predigest the process of modeling, and get the properties of complex model at the same time. So refinement was widely studied. This paper is based on the idea of refinement, makes research about the problem of the properties preserving in Petri net substitution, and the research content is as follows:This paper makes research about the soundness and generalized soundness first, defines the place substitution of Petri net and net system, gives the distribution formula of tokens. Then it substitutes safety place of Petri nets with sound workflow nets, and proves that the net substituted can preserve behavioral properties as liveness, boundedness, and reversibleness. Then it points to generalized places in Petri nets, and proves that substitute places by generalized sound workflow nets can also preserve the behavioral properties above.Then this paper defines the transition workflow nets, and the transition substitution formula of Petri nets and net systems based on T-workflow nets. Then it researches the properties preservation of the substituted nets, and proves that the transition substitution net can also preserve liveness, boundedness, and reversibleness.At last, this paper expands the application of substitution into connection arcs, using the connection arc workflow nets. So it defines TP-type and PT-type workflow nets, which are used to substitute the connection arcs in the Petri nets correspondingly. It proves that the substituted nets gotten from the methods above can also preserve the behavioral properties above. The introduce of method of connection arc substitution can expand the application range of refinement, and it has a very important meaning to the modeling and analyzing of Petri nets.