Conversion and verification of recursive structure in PI-calculus with compositional petri-NET

This paper presents the recursive expression types of PI-calculus on the basis of the general method and transition rules of transforming PI-calculus to Petri-net which are proposed by Raymond Devillers et al. Then, after exploring the problems of value selection and data saving that will surely appear in the conversion process, this paper expands the proposed rp-net based on the general method of Raymond Devillers et al, and provides the method of transforming the recursive structure in PI-calculus into a Petri-net. In the end, the conversion result net of the typical recursive structure is verified by using the CPNtools which is an authoritative simulation tools currently.