Skip to content

CONCEPT Cited by 1 source

Bisimulation

Definition

Bisimulation is the two-way equality of behaviour-sets between two state machines (typically a specification and an implementation): every behaviour of one is realizable by the other, and vice versa.

If Bspec is the set of behaviours the spec permits and Bimpl is the set the implementation exhibits, then:

  • Bimpl ⊆ Bspec — refinement — the impl never does anything the spec forbids.
  • Bimpl ⊇ Bspec — every spec behaviour is realizable by the impl.
  • Bimpl = Bspec — bisimulation.

Refinement is the minimum for a correct implementation. Bisimulation is stronger: it says the impl not only avoids forbidden behaviours but can exhibit every behaviour the spec intends.

Why both directions matter for conformance

From the MongoDB 2020 conformance-checking experiment (Source: sources/2025-06-02-mongodb-conformance-checking-at-mongodb-testing-that-our-code-matches-our-tla-specs):

An implementation refines a spec if Bimpl ⊂ Bspec. If the converse is also true, if Bspec ⊂ Bimpl, then this is called bisimulation, and it's a nice property to have, though not always necessary for a correctly implemented system. You can test each direction.

The two conformance-checking techniques map onto the two directions:

Direction Technique What failure means
Bimpl ⊂ Bspec patterns/trace-checking impl does something spec forbids → impl bug or spec is wrong
Bspec ⊂ Bimpl patterns/test-case-generation-from-spec spec has a behaviour impl can't exhibit → impl is incomplete or buggy

Running both gives bisimulation. Running one gives refinement only.

When refinement is sufficient

A spec typically models the externally observable behaviour of a system. Internal optimisations (caches, parallel work, replica fan-out) are acceptable if their external effect matches the spec. The impl "refines" the spec — does everything the spec says + some permitted internal extras.

When the externally observable behaviour is all that matters — the usual case for consumers of a distributed system's API — refinement suffices. Bisimulation becomes interesting when:

  • A spec claims to be executable / a reference implementation (every valid spec behaviour should be reachable by the impl, otherwise the spec is too permissive).
  • Testing aims for coverage — if Bspec ⊂ Bimpl fails, some spec behaviour is dead code in the impl.
  • Safety properties are expressed as "every spec action happens" (rare; usually safety is stated as "bad spec actions never happen" which is the refinement direction).
  • Equivalence of state machines — two machines with different internal structure that produce the same observable behaviours are bisimilar; internal state shapes may differ.
  • Trace equivalence — weaker than bisimulation; two machines with the same trace set but different branching structure are trace-equivalent but may not be bisimilar (bisimulation requires matched branching at each step, not just matched overall traces).
  • Refinement (uni-directional) — Bimpl ⊆ Bspec; the impl lies inside the spec; the impl may underspecify the spec.

For most industrial conformance-checking work refinement is the target and bisimulation is mentioned as an optional stronger guarantee — that's the stance of the MongoDB paper.

Seen in

Last updated · 200 distilled / 1,178 read