On the reduction of chocs bisimulation to π-calculus bisimulation

Abstract

Chocs and π-calculus are two extensions of CCS where, respectively, processes and channels are transmissible values. In previous work we have proposed a formalization of the notion of bisimulation for Chocs. In this paper we suggest a more effective way to reason about this notion by means of an embedding of Chocs into a richer calculus endowed with a notion of ‘activation’ channel which we christen Chocst. is the name of a new internal action which is produced by a synchronization on an activation channel, such a synchronization has the effect of forcing the execution of an idle process. In first approximation transitions in Chocst may be understood as sequences of synchronizations along activation channels followed by an ‘observable’ transition. There is a simple definition of bisimulation for Chocst which satisfies natural laws and congruence rules, moreover the synchronization trees associated to Chocst processes are finitely branching. We propose Chocst as an intermediate step towards the definition of a tool for the verification of Chocs bisimulation.

CRIN BP239, 54506 Vandœuvre-lès-Nancy Cedex, France. This work was partially supported by ESPRIT BRA 6454 Confer. A preliminary version of this paper has appeared as RR 1786, Inria-Lorraine, (October 1992), and it was presented at the ERCIM workshop on Theory and Practice in Verification (Pisa, December 1992) and at the first Confer workshop (Sophia-Antipolis, January 1993).