Strong bisimulation for explicit fusions

Lucian Wischik, Philippa Gardner. Submitted for publication.

Abstract.

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.

Download

  • None yet.  
  • See also

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