Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes

Abstract

We introduce an improved version of the symbolic transition graph with assignment (STGA) of Lin. The distinction of our model is that the assignment of a transition is performed after rather than before the action. Consequently, it has two advantages over the original one: on one hand, most regular value-passing processes can be represented more intuitively and compactly as such graphs; on the other hand, the natural definitions of symbolic double transitions can be given. The rules which generate the improved STGAs from regular value-passing processes are presented. The various versions (late/early, ground/symbolic) of strong operational semantics and strong bisimulation are given to such graphs, respectively. Our strong bisimulation algorithms are based on the late strong bisimulation algorithm of Lin, however, ours are more concise and practical. Finally, the improved STGAs are generalized to both symbolic observation graphs with assignments and symbolic congruence graphs with assignments, and therefore weak bisimulation equivalence and observation congruence can be checked, respectively.