Abstract
Bisimulation is an equivalence relation widely used for comparing processes expressed in CCS and related process calculi [1,6,8,9]. Simulation is its asymmetric variant. The advantages of bisimilarity are simplicity, efficiency and variety. Proofs based bisimulation for particular programs can often be delegated to a model checker. Refinement is a weaker asymmetric relation used for the same purpose in CSP [2,3,14]. Its advantages are abstraction, expressive power and completeness. Refinement permits proofs of more equations and inequations than bisimilarity. When bisimulation and refinement are reconciled, all their distinctive advantages can be combined and exploited whenever the occasions demands. This paper shows how to link these two approaches by introducing an observation-preserving mapping, which gives rise a Galois connection between simulation and refinement. The same mapping is also applicable to coincide barbed simulation with failures/divergence refinement.
| Original language | English |
|---|---|
| Pages (from-to) | 61-74 |
| Number of pages | 14 |
| Journal | Lecture Notes in Computer Science |
| Volume | 3525 |
| DOIs | |
| State | Published - 2005 |
| Event | Symposium on the Occasion of 25 Years of CSP - Communicating Sequential Processes - London, United Kingdom Duration: 7 Jul 2004 → 8 Jul 2004 |