Bisimulation can't be traced
- 3 January 1995
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 42 (1) , 232-268
- https://doi.org/10.1145/200836.200876
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 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.Keywords
This publication has 17 references indexed in Scilit:
- Experimenting with process equivalenceTheoretical Computer Science, 1992
- Observation equivalence as a testing equivalenceTheoretical Computer Science, 1987
- Higher-level synchronising devices in Meije-SCCSTheoretical Computer Science, 1985
- Algebraic laws for nondeterminism and concurrencyJournal of the ACM, 1985
- Algèbre de processus et synchronisationTheoretical Computer Science, 1984
- A Theory of Communicating Sequential ProcessesJournal of the ACM, 1984
- Testing equivalences for processesTheoretical Computer Science, 1984
- Calculi for synchrony and asynchronyTheoretical Computer Science, 1983
- Communicating sequential processesCommunications of the ACM, 1978
- LCF considered as a programming languageTheoretical Computer Science, 1977