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