Research On Translation From Recursion π-calculus To Petri Net

In recent years, formal modeling methods for concurrent and distributed systems arerequired no matter in theory or in practice with the rapid development of concurrent anddistributed computing technology. At present, a lot of scholars use π calculus and Petri netmodel as theory foundation for system modeling, but in academia there exists a greatcontroversy about which model is more suitable for system modeling. The reason is that πcalculus indicates dynamic evolution between the processes by reduction, and it can be usedto describe the distributed system with vulnerable topological structure, while it sometimescan’t reflect systems’ physical structure information vividly when modeling actually, and thereare only a few system verification support tools, which makes it hard to verify the correctnessof formal system models; Petri nets focus on describing the system structure and analyzingsystem properties, and can effectively depict the modeling system’s real concurrent semanticsas well, but it also has some disadvantages, such as lacking semantic information inexpression. We find that each method has its advantages, if we combine their advantagestogether, it can make up the deficiency of simply use one model. Through the translationbetween π calculus and Petri nets, we can analyze the formalization model morecomprehensive, and get more complete descriptions of structure and behavior analysis results.Through the research on recursion π calculus and Petri net, in this paper a translationmethod from recursion π calculus to Petri net is proposed and the bisimulation equivalence isproved, on the basis of scholars’ research on the translation from π-calculus to Petri net, suchas Raymond Devillers. Firstly, the method of how to record the recursion level, how topreserve information in translation, and how to judge recursion export, is provided. Aiming atthe translation of recursion of π calculus, we give the basic process translation rules andcombination rules in this paper. Based on these two rules, a translation method from recursionπ calculus to Petri net is put forward. At the same time, the translation fire rule and identifyequivalence rule are given. We then use the bisimulation equivalence theory to prove theequivalence between recursion π calculus and the translated Petri nets.According to that the recursive subject may perform many times, and result intremendous Petri nets, a more concise Petri nets representation is put forward in this paper. Inthis part, execution process of recursion π calculus is analyzed, the recursive execution graphis given, and then we propose the concepts of state graph and compact state graph, and thenput forward a more concise Petri nets representation method, which is proved to be equivalentto the Petri nets. Finally the Petri nets verification tool---CPN Tools is used to test and verifythe translation results. The innovation points of this paper include:(1) A hierarchical method of the translation from recursion π calculus to Petri net isput forward, which follows the basic process translation rules and combination rules, andit is proved that the recursion π calculus and its translated Petri net satisfied bisimulationequivalence;(2) The compact state graph of recursion π calculus is given, which keeps the systemsemantics, and codes the exact same path set.(3) A more concise Petri nets representation is proposed and it is proved to beequivalent to the Petri nets.Aiming at the recursive structure in π calculus, a method of translating to Petri nets isbrought forward, which sets up a communication bridge between recursion π calculus andPetri nets. According to the multiple recursion, a more concise Petri nets representation ispresented, and it has positive significance to apply Petri net madel in complicated systems.