On Bisimilarity and Substitution in Presence of Replication

Abstract. We prove a new congruence result for the π-calculus: bisimilarity is a congruence in the sub-calculus that does not include restriction nor sum, and features top-level replications. Our proof relies on algebraic properties of replication, and on a new syntactic characterisation of bisimilarity. We obtain this characterisation using a rewriting system rather than a purely equational axiomatisation. We then deduce substitution closure, and hence, congruence. Whether bisimilarity is a congruence when replications are unrestricted remains open.

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Daniel Hirschkoff, Damien Pous
• Keywords: Algebraic Properties, Equational Axiomatisation, Features Top-level Replications, ICALP 2010, Programming Languages