A Transformation from p-π to MSVL

摘要

A structural transformation from p-π processes to MSVL programs is proposed in this paper. To this end, channel and communication primitives are firstly defined in MSVL. Further, based on these definitions, a mapping function γ which transforms p-π processes into MSVL programs is formalized. As a result, p-π can provide a mechanism to model, simulate and verify concurrent systems by means of the techniques of MSVL. Finally, a case study is given to illustrate how the transformation is used in practice.