A Correct Abstract Machine for the Stochastic Pi-calculus

In this paper, an abstract machine is presented for a variant of the stochastic pi-calculus, in order to correctly model the stochastic simulation of biological processes. The machine is first proved sound and complete with respect to the calculus, and then used as the basis for implementing a stochastic simulator. The correctness of the stochastic machine helps ensure that the simulator is correctly implemented, giving greater confidence in the simulation results. A graphical representation for the pi-calculus is also introduced.