Conference Proceeding

Bisimulation by Unification


Baldan P, Bracciali A & Bruni R (2002) Bisimulation by Unification. In: Kirchner H & Ringeissen C (eds.) Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, Volume 2422. 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, 09.09.2002-13.09.2002. Amsterdam: Springer, pp. 254-270.;

We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when suitable components (i.e. closed terms) fill in their place-holders. The distinguishing feature of our approach is the definition of a symbolic operational semantics for coordinators that exploits spatial/modal formulae as labels of transitions and avoids the universal closure of coordinators w.r.t. all components. Two kinds of bisimilarities are then defined, called strict and large, which differ in the way formulae are compared. Strict bisimilarity implies large bisimilarity which, in turn, implies the one based on universal closure. Moreover, for process calculi in suitable formats, we show how the symbolic semantics can be defined constructively, using unification. Our approach is illustrated on a toy process calculus with CCS-like communication within ambients.

Title of seriesLecture Notes in Computer Science
Number in seriesVolume 2422
Publication date31/12/2002
Publisher URL
Place of publicationAmsterdam
ISSN of series0302-9743
Conference9th International Conference, AMAST 2002
Conference locationSaint-Gilles-les-Bains, Reunion Island, France