Bisimulation Can't Be Traced.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1987
Accession Number
ADA192725

Entities

People

  • Albert R. Meyer
  • Bard Bloom
  • Sorin Istrail

Organizations

  • Massachusetts Institute of Technology

Tags

DTIC Thesaurus Topics

  • Calculus
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Contrast
  • Grammars
  • Guarantees
  • Information Processing
  • Language
  • Military Research
  • Multithreading
  • Programming Languages
  • Security
  • Semantics
  • Sequences
  • Standards

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.