A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets

TL;DR

This paper introduces the first polynomial translation from finite control pi-calculus processes to safe Petri nets, enabling practical model checking with a natural correspondence and bisimulation guarantees.

Contribution

It presents a novel polynomial translation method from pi-calculus FCPs to safe Petri nets, bridging high-level process models and low-level verification tools.

Findings

Establishes a bisimulation between processes and Petri nets.

Provides a practical approach for model checking pi-calculus models.

First known polynomial translation for this class of processes.

Abstract

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.