Accession Number : ADA192725

Title :   Bisimulation Can't Be Traced.

Descriptive Note : Preliminary rept.,

Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s) : Bloom, Bard ; Istrail, Sorin ; Meyer, Albert R

PDF Url : ADA192725

Report Date : Nov 1987

Pagination or Media Count : 24

Abstract : 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. We examine what additional operations are needed to explain bisimulation similarly-specifically in the case of finitely branching processes without silent moves. We 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, we work out some of the basic proof theoretic facts which justify the SOS discipline. Keywords: Languages, Semantics, Concurrency, Parallelism, Bisimulation, Observational equivalence, Trace equivalence.

Descriptors :   *SIMULATION LANGUAGES, CALCULUS, SEMANTICS, RECURSIVE FUNCTIONS, SEQUENCES

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE