We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking.

• 68Q60 - Specification and verification (program logics, model checking, etc.)
• 68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)