Strong bisimulation for explicit fusions

Lucian Wischik, Philippa Gardner. Submitted for publication.


In the pi calculus, the various definitions of (strong) congruence yield different relations. In one widely-studied variant of the pi calculus, the asynchronous, it turns out that they coincide. We show that they also coincide in a different variant, the explicit fusion calculus.

The important consequence of adding explicit fusions to a calculus is that an explicit fusion in parallel with a term can effect a substitution. This means that parallel contexts become as discriminating as arbitrary contexts, and that open bisimulation is more natural for the explicit fusion calculus than it was for the pi calculus.


  • None yet.  
  • See also

  • Explicit fusions: theory & implementation - Wischik's PhD dissertation, covers much of the material in this paper.