An Operational Semantics of the π-Calculus

L. Li (Canada)


Algebraic process expression, communication and con current mobile system, -calculus, operational semantics.


The -calculus was invented for modeling communication and concurrent mobile systems. It is a general mathemati cal theory based on a few primitive notions for studying the behaviors of mobile systems. It uses algebraic expres sions to represent real systems. Its semantics is specified with reduction and labeled transition rules for manipulat ing the expressions. The intensive dispute in W3C on Petri nets vs. the -calculus as a formal foundation of a choreography description language of Web services im plies the lack of a practical syntax and a clear semantics in the -calculus. Here, we indicate the ambiguity and obscurity of the syntactic specification of the -calculus and present an operational semantics for the -calculus based on a reformulated syntax of the -calculus. We de scribe how to implement the -calculus in terms of the reformulated syntax and semantics.

Important Links:

Go Back