On Expression Of General Petri Net Systems With ?-calculus

Petri net and ? calculus are two formal models which are used to model concurrent systems. Petri net is a system model in graphic form with rigorous mathematical analysis theory. However, due to the connections between its transfers and positions are fixed, it is difficult to describe the loose dynamic coupling systems. ? calculus is a process algebra that can not only describe and analyze concurrent systems but also simulate dynamic behavior of concurrent systems through the interactions between processes. In ? calculus, name is the easiest entity, which can be transmitted along the channel and can be used as the name of the channel, therefore ? calculus can describe the loose dynamic coupling system. However, due to the lack of synchronous communication primitives, its communications can not be a one-time synchronous execution, but perform serially.This paper proposes a method for the expression of the general Petri net system with ? calculus to prove that ? calculus can express the general Petri net system. After a brief introduction to the concepts of Petri net and ? calculus, this paper analyzes the existing synchronization and identification problems that ? calculus expresses the general Petri nets, gives the solution based on the identification mechanism and the notification mechanism, and proposes ? calculus model in expressing the general Petri net system, thus proved that ? calculus can express the general Petri nets.Then this paper gives an example of a general Petri net system, establishes the corresponding ? calculus process using the proposed expressing method, and achieves an automatic conversion process of Petri nets to ? calculus expressions. Finally, this paper verifies the correctness of the ? calculus expressions through an automatic verification tool MWB for ? calculus. Result indicates that the execution routes of ? calculus concurrent processes is coincident with the dynamic behaviors of the Petri net system in the example.