Petri nets semantics of π-calculus

As π-calculus based on the interleaving semantics cannot depict the true concurrency and has few supporting tools, it is translated into Petri nets. π-calculus is divided into basic elements, sequence, concurrency, choice and recursive modules. These modules are translated into Petri nets to construct a complicated system. Petri nets semantics for π-calculus visualize system structure as well as system behaviors. The structural analysis techniques allow direct qualitative analysis of the system properties on the structure of the nets. Finally, Petri nets semantics for π-calculus are illustrated by applying them to mobile telephone systems.