The asynchronous π-calculus is a variant of the π-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation. Their bisimulation relies on a modified transition system where, at any moment, a process can perform any input action. In this paper we propose a new notion of bisimulation for the asynchronous π-calculus, defined on top of the standard labelled transition system. We give several characterizations of this equivalence including one in terms of Honda and Tokoro’s bisimulation, and one in terms of barbed equivalence. We show that this bisimulation is preserved by name substitutions, hence by input prefix. Finally, we give a complete axiomatization of the (strong) bisimulation for finite terms.
CITATION STYLE
Amadio, R. M., Castellani, I., & Sangiorgi, D. (1996). On bisimulations for the asynchronous π-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1119, pp. 147–162). Springer Verlag. https://doi.org/10.1007/3-540-61604-7_53
Mendeley helps you to discover research relevant for your work.