Bisimulation Lattice of the Asymmetric Chi Calculus with Mismatch

The chi calculus is a mobile computing model. A systematic investigation into the bisimulation lattice is carried out to understand the interplay between the asymmetry and the mismatch in the framework of the chi calculus. Both features are motivated by applications. And both are significant in theory. The syntax and labeled transition system of the calculus are presented. L-bisimilarities are defined. It is shown that all the sixty three L-bisimilarities collapse to twelve distinct relations. The twelve L-bisimilarites form a bisimulation lattice with respect to set inclusion. The top and the bottom of the lattice coincide with the barbed bisimilarity and the open bisimilarity respectively.