Bisimulation congruence of chi calculus

Abstractχ-Calculus was proposed as a process calculus that has a uniform treatment of names. Preliminary properties of χ-calculus have been examined in the literature. In this paper a more systematic study of bisimilarities for χ-processes is carried out. The notion of L-bisimilarity is introduced to give a possible classification of bisimilarities on χ-processes. It is shown that the set of L-bisimilarities form a four element lattice and that well-known bisimilarities for χ-processes fit into the lattice hierarchy. The four distinct L-bisimilarities give rise to four congruence relations. Complete axiomatization system is given for each of the four congruences