Bisimulation Can't Be Traced

Abstract

In the concurrent language CCS, two programs are considered the same if they are bisimilar. Several years and many researchers have demonstrated that the theory of bisimulation is mathematically appealing and useful in practice. However, bisimulation makes too many distinctions between programs. We consider the problem of adding operations to CCS to make bisimulation fully abstract. We define the class of GSOS operations, generalizing the style and technical advantages of CCS operations. We characterize GSOS congruence in as a bisimulation-like relation called ready-simulation. Bisimulation is strictly finer than ready simulation, and hence not a congruence for any GSOS language. © 1995, ACM. All rights reserved.