SYMBOLIC BISIMULATIONS

We re-examine bismulation equivalence for value-passing process languages in which actions have associated with them values from a possibly infinite value set. Using symbolic actions we generalise the standard notion of labelled transition graph to that of symbolic transition graph. The advantage of the latter is that the operational semantics of many value-passing processes may be expressed in terms of finite symbolic transition graphs although the underlying (standard) labelled transitions graph is infinite. A collection of symbolic bisimulations parameterised on boolean expressions, congruent-to(b), are then defined over symbolic transition graphs. These are related to standard bisimulations by proving that t congruent-to(b) u if and only if in every interpretation which satisfies b, t is bisimulation equivalent to u in the standard sense. We then give an algorithm for checking the relation t congruent-to(b) u which can be applied to arbitrary finite symbolic trees. The results apply to both early and late bisimulation equivalence, which are the two natural generalisations of the standard bisimulation equivalence to value-passing languages.