Bisimulation by Unification

Citation

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. http://link.springer.com/chapter/10.1007/3-540-45719-4_18#; https://doi.org/10.1007/3-540-45719-4_18

Abstract
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.