Petri nets, called rp-nets, that are high-level nets with read arcs, are utilized in this paper. It develops a mechanism to translate &pgr; calculus (process calculus) terms to rp-nets. This mechanism is expected to facilitate utilization of verification technologies built around Petri nets, for process-based programming. Process-based programs that are based on &pgr; calculus, in particular, can be (possibly) verified. The key idea is to view the system specified in &pgr; calculus as consisting of a main program, together with procedural declarations. The control structure of the program and procedures are represented as disjoint high-level nets.

The first section enumerates the drawbacks of Petri box calculus and modular nets in dealing with recursion. The second section describes the required theory of &pgr; calculus and its semantics. The third section explains the theory of rp-nets. The translation, described in the fourth section, has three phases. The first phase takes as input the syntax trees of a &pgr; calculus program and builds process-based components. The second phase connects the components to form a net, erasing send/receive labeled transition arcs. The final phase inserts initial markings to complete the translation. The fifth section describes the firing rules of resulting rp-nets in detail. The sixth section proves that the resulting structure of nets is finite. Section 7 compares the translation with similar related translations of &pgr; calculus specifications. Section 8 presents the authors’ conclusions.

Both ends of the translation are important in practical computing, making finite output of rp-nets an important result.