Journal of the Association for Computing Machinery, Vol. 42, No. 1, January 1995, pp. 232–268.

Bisimulation Can’t Be Traced

BARD BLOOM

SORIN ISTRAIL

AND

ALBERT R. MEYER

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 congruency 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.

Categories and Subject Descriptors. D.3.1[semantics]; D.3.3[concurrent programming structures]; F.3.2[algebraic approaches to semantics; operational semantics]; I.6.2

General Terms. Languages, Theory, Verification

Additional Key words and Phrases. Bisimulation, structural operational semantics, process algebra, CCS

Copyright 1995 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.