This paper presents some new results on bared equivalences for the π-calculus. The equivalences studied are barbed congruence and a variant of it called open barbed bisimilarity. The difference between the two is that in open barbed the quantification over contexts is inside the definition of the bisimulation and is therefore recursive. It is shown that if infinite sums are admitted to the π-calculus then it is possible to give a simple proof that barbed congruence and early congruence coincide on all process, not just on image-finite processes. It is also shown that on the π-calculus, and on the extension of it with infinite sums, open barbed bisimilarity does not correspond to any known labelled bisimilarity. It coincides with a variant of open bisimilarity in which names that have been extruded are treated in a special way, similarly to how names are treated in early bisimilarity.
展开▼
