Barbed congruence of the asymmetric chi calculus

摘要

The chi calculus is a model of mobile processes. It has evolved from the pi-calculus with motivations from simplification and communication-as-cut-eliminalion. This paper studies the chi calculus in the framework incorporating asymmetric communication. The major feature of the calculus is the identification of two actions; x/x and tau. The investigation on the barbed bisimilarity shows how the property affects the observational theory. Based on the definition of the barbed bisimilarity, the simulation properties of the barbed bisimilarity are studied. It shows that the algebraic properties of the barbed bisimilarity have changed greatly compared with the chi calculus. Although the definition of the barbed bisimilarity is very simple, the property of closeness under contexts makes it difficult to understand the barbed bisimilarity directly. Therefore an open style definition of the barbed bisimilarity is given, which is a context free description of barbed bisimilarity. Its definition is complex, but it is a well-behaved relation for it coincides with the barbed bisimilarity. It also helps to build an axiomati-zation system for the barbed congruence. Besides the axioms for the strong barbed bisimilarity, the paper proposes a new tau law and four new update laws for the barbed congruence. Both the operational and algebraic properties of the enriched calculus improve the understanding of the bisimulation behaviors of the model.