Bisimulation can't be traced. Preliminary report
Bard Bloom, Sorin Istrail, Albert R. Meyer · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1987
Bisimulation is the primitive notion of equivalence between concurrent processes in Milner's Calculus of Communicating Systems (CCS); there is a nontrivial game-like protocol for distinguishing nonbisimular processes. In contrast, process distinguishability in Hoare's theory of Communicating Sequential processes (CSP) is determined soley on the basis of traces of visible actions. The authors examine what additional operations are needed to explain bisimulation similarly-specifically in the case of finitely branching processes without silent moves. They formulate a general notion of Structured Operational Semantics for processes with Guarded recursion (GSOS), and demonstrate that bisimulation does not agree with trace congruence with respect to any set of GSOS-definable contexts. In justifying the generality and significance of GSOS's, some of the basic proof theoretic facts are worked out that justify the SOS discipline.