Abstract: A formal encoding method was given to represent bounded Petri nets by CCS which is one kind model of process calculi for researching the relationship between Petri nets and process calculi. A Place/Transition net could be encoded to a finite process by this method. The process and the original net satisfy the operational and observational correspondence. In this view, they have the same behaviors. It shows that the encoding method is fully abstract with respect to the labeled bisimulation, which is an equivalence relation between nets.

Key words: Petri nets, process calculi, encoding