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.
Keywords Petri nets - π-calculus - concurrency - structual characteristics - analysis
__________
Translated from Control and Decision, 2007, 22(8): 864–868 [译自:控制与决策]