Bisimulation

Imagine two vending machines. One is brand-new; the other is a refurbished unit with twice as many internal components. Both accept a coin and dispense coffee. From the outside, you cannot tell them apart.

That intuition — observable behavior is what matters, not internal structure — is the heart of bisimulation. Two systems are bisimilar if each can permanently mimic the other: every action one system can take, the other can take too, and after the step the resulting states are again bisimilar.

The concept was developed independently by David Park (1981) and Robin Milner (1980s) in the context of process algebra and concurrency theory. Milner's CCS (Calculus of Communicating Systems) made bisimulation the canonical notion of equivalence for concurrent programs — and it remains the gold standard today.

Unlike simpler notions such as trace equivalence (matching only the sequences of visible actions), bisimulation also captures branching structure: it distinguishes a system that can choose between two options from one that is forced down only one path, even when both produce the same traces.

Below are two small labeled transition systems (LTS). States are circles; arrows are labeled actions. The bisimulation game works like this: the Attacker picks a system and fires a transition; the Defender must reply with a matching transition in the other system — same action label, landing in states that are still bisimilar. If the Defender can always reply, the two systems are bisimilar.

<!-- {{c_html_intro}} -->
<div class="controls">
  <button id="btn-example1" class="ex-btn active" type="button">{{btn_ex1}}</button>
  <button id="btn-example2" class="ex-btn" type="button">{{btn_ex2}}</button>
</div>
<p class="hint" id="hint-text">{{hint_bisimilar}}</p>
<div class="arena">
  <div class="lts-panel">
    <div class="lts-title">{{lbl_system_a}}</div>
    <svg id="svg-a" class="lts-svg" viewBox="0 0 200 160"></svg>
  </div>
  <div class="divider">&#8596;</div>
  <div class="lts-panel">
    <div class="lts-title">{{lbl_system_b}}</div>
    <svg id="svg-b" class="lts-svg" viewBox="0 0 200 160"></svg>
  </div>
</div>
<div class="status-bar" id="status-bar">{{status_pick}}</div>
<div class="btns">
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; margin: 0; padding: 0; }
body { font-family: system-ui, sans-serif; color: #222; }
.controls { display: flex; gap: .4rem; margin-bottom: .6rem; }
.ex-btn { font: 600 13px system-ui; padding: .3rem .75rem; border: 1px solid #1d3557;
          background: #fff; color: #1d3557; border-radius: 6px; cursor: pointer; }
.ex-btn.active { background: #1d3557; color: #fff; }
.hint { font-size: .85rem; color: #444; margin-bottom: .5rem; line-height: 1.45; }
.arena { display: flex; align-items: center; gap: .5rem; }
.lts-panel { flex: 1; min-width: 0; }
.lts-title { font-size: .8rem; font-weight: 700; text-align: center; color: #555;
             margin-bottom: .2rem; letter-spacing: .04em; text-transform: uppercase; }
.lts-svg { width: 100%; border: 1px solid #d0d9e3; border-radius: 8px; background: #f7f9fb; }
.divider { font-size: 1.4rem; color: #aaa; user-select: none; }
.status-bar { font-size: .9rem; font-weight: 600; min-height: 1.4em;
              margin: .5rem 0; padding: .3rem .5rem; border-radius: 6px; }
.status-bar.ok   { background: #d4f5dc; color: #0a5c23; }
.status-bar.bad  { background: #fde8ea; color: #9b2335; }
.status-bar.info { background: #e8f0fb; color: #1a3a6b; }
.btns { margin-top: .4rem; }
button { font: 600 13px system-ui; padding: .4rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
/* {{c_css_svg}} */
.node circle { cursor: pointer; transition: fill .15s; }
.node circle.current { fill: #1d3557; stroke: #1d3557; }
.node circle.visited { fill: #e8eef3; stroke: #4a7fa5; }
.node circle.plain   { fill: #fff; stroke: #4a7fa5; }
.node text { font: 700 11px ui-monospace, monospace; fill: #1d3557; pointer-events: none; }
.node circle.current + text { fill: #fff; }
.edge { stroke: #4a7fa5; stroke-width: 1.5; fill: none; }
.edge-label { font: 600 11px ui-monospace, monospace; fill: #2a5f87; }
.edge-btn { cursor: pointer; }
.edge-btn:hover .edge { stroke: #c92f3c; }
.edge-btn:hover .edge-label { fill: #c92f3c; }
.edge-btn.fired .edge { stroke: #e63946; }
.edge-btn.fired .edge-label { fill: #e63946; }
.edge-btn.replied .edge { stroke: #0a7d33; }
.edge-btn.replied .edge-label { fill: #0a7d33; }

// Code not found

Click a transition on either side to play as the Attacker. The demo plays the Defender's best reply automatically. Notice that System A and System B are bisimilar: every move has a matching answer. To see a non-bisimilar pair, switch to the second example — System C can perform action $a$ and then be forced into $b$, while System D can choose after $a$; the Attacker exploits that branch to win.

How hard is it to decide whether two systems are bisimilar?

• Finite-state systems: the classic partition refinement algorithm (Kanellakis–Smolka 1983; Paige–Tarjan 1987) decides bisimilarity in $O(m \log n)$ time, where $n$ is the number of states and $m$ the number of transitions. For practical model sizes this is very fast.
• Bisimulation vs. trace equivalence: trace equivalence (do the two systems produce the same sequences of visible actions?) is weaker — two trace-equivalent systems need not be bisimilar. Bisimulation is strictly finer, and modal logic (specifically the modal $\mu$-calculus) captures it exactly: two states are bisimilar iff they satisfy exactly the same modal $\mu$-calculus formulas.
• Pushdown and context-free systems: for systems with a stack (pushdown automata), bisimilarity is still decidable but becomes much harder — it is EXPTIME-complete. For context-free processes the result is also decidable (a deep result by Senizergues, 1998, Stirling, 2002).
• Probabilistic bisimulation: when transitions carry probabilities, the Larsen–Skou definition (1991) generalizes bisimulation; checking it on finite Markov chains remains polynomial but the algorithms are more intricate.
• Infinite-state systems: in general, bisimilarity is undecidable — the halting problem reduces to it. The frontier between decidable and undecidable is an active research area.

The practical takeaway: for the finite-state systems that arise in hardware and protocol verification, bisimulation checking is fast and fully automated. Its computational elegance is one reason it became foundational in automata minimization and concurrency theory.

Bisimulation is not an abstract curiosity — it is the engine behind many tools you rely on:

• Model checking: tools like CADP, mCRL2 and UPPAAL reduce huge state spaces by quotienting bisimilar states together before verification — sometimes shrinking millions of states to thousands.
• Compiler optimization: two program fragments are safe to swap if they are bisimilar; this justifies many loop and concurrency transformations without requiring full functional equivalence.
• Protocol verification: checking that a protocol implementation is bisimilar to its specification proves it can never exhibit a behavior the spec forbids — and vice versa.
• Process algebra and programming language semantics: CCS, CSP, and ACP use bisimulation as their equivalence notion; every equation in those algebras is justified by a bisimulation argument.
• Database query optimization: certain query rewriting rules are sound precisely because the rewritten query is bisimilar to the original over the relevant fragment of the data model.

Understand bisimulation and you hold the key to a whole family of equivalences: strong bisimulation, weak bisimulation (ignoring internal $\tau$ steps), branching bisimulation, and probabilistic bisimulation are all variations on the same mirroring idea. See also automata minimization for how the same partition-refinement algorithm computes the minimal DFA.

Bisimulation answers a deceptively simple question: when are two systems truly the same? Not when they share the same code, not when they produce the same output on every input — but when they can forever mirror each other's moves, step for step, choice for choice.

That precision is what makes it powerful. It is strict enough to distinguish a system that can choose from one that must act, yet computable enough to be automated for the finite systems we build every day.

The next time you compile a concurrent program, verify a protocol, or minimize a finite automaton, there is a good chance that bisimulation — or one of its cousins — is working quietly in the background, certifying that your transformation preserved every observable behavior. Two vending machines, one coin, one coffee: automata minimization starts exactly here.