Introduction

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.

Match the Moves

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.

<!-- Two labeled transition systems side by side for the bisimulation game -->
<div class="controls">
  <button id="btn-example1" class="ex-btn active" type="button">Example 1: bisimilar</button>
  <button id="btn-example2" class="ex-btn" type="button">Example 2: not bisimilar</button>
</div>
<p class="hint" id="hint-text">Systems A and B <strong>are bisimilar</strong>: every move has a matching reply. Click any arrow to play as the Attacker — the Defender replies automatically.</p>
<div class="arena">
  <div class="lts-panel">
    <div class="lts-title">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">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">Click an arrow on either side to fire a move as the Attacker.</div>
<div class="btns">
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>

/* Layout for the bisimulation demo */
* { 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; }
/* SVG node and edge styling for the LTS diagrams */
.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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Bisimulation game — Attacker fires a transition, Defender replies with a matching one
// in the other system. If the Defender can always reply, the systems are bisimilar.

// Example 1: bisimilar pair — branching collapse
const EXAMPLES = [
  {
    // System A: two branches both looping on b; System B: one state looping on b
    A: {
      states: [{id:'s0',x:100,y:30},{id:'s1',x:40,y:110},{id:'s2',x:160,y:110}],
      edges: [{from:'s0',to:'s1',label:'a'},{from:'s0',to:'s2',label:'a'},
              {from:'s1',to:'s1',label:'b'},{from:'s2',to:'s2',label:'b'}],
      init: 's0'
    },
    B: {
      states: [{id:'t0',x:100,y:30},{id:'t1',x:100,y:110}],
      edges: [{from:'t0',to:'t1',label:'a'},{from:'t1',to:'t1',label:'b'}],
      init: 't0'
    },
    // Bisimulation relation: s1~t1, s2~t1 (both loop on b)
    bisim: [['s0','t0'],['s1','t1'],['s2','t1']]
  },
  {
    // Example 2: NOT bisimilar — different options after a
    A: {
      states: [{id:'p0',x:100,y:30},{id:'p1',x:60,y:110},{id:'p2',x:140,y:110}],
      edges: [{from:'p0',to:'p1',label:'a'},{from:'p0',to:'p2',label:'a'},
              {from:'p1',to:'p1',label:'b'},{from:'p2',to:'p2',label:'c'}],
      init: 'p0'
    },
    B: {
      states: [{id:'q0',x:100,y:30},{id:'q1',x:100,y:110}],
      edges: [{from:'q0',to:'q1',label:'a'},{from:'q1',to:'q1',label:'b'},
              {from:'q1',to:'q1',label:'c'}],
      init: 'q0'
    },
    bisim: [] // no bisimulation exists
  }
];

let exIdx = 0;
let curA, curB;
let firedEdge = null, repliedEdge = null;

function isBisimilar(a, b, ex) {
  // Check if (a,b) is in the bisimulation relation for this example
  return ex.bisim.some(([x, y]) => x === a && y === b);
}

function drawLTS(svgEl, lts, curState, firedId, repliedId) {
  // Draw all edges first (below nodes), then nodes on top
  svgEl.innerHTML = '';
  const ns = 'http://www.w3.org/2000/svg';
  function mk(tag, attrs) {
    const el = document.createElementNS(ns, tag);
    for (const [k, v] of Object.entries(attrs)) el.setAttribute(k, v);
    return el;
  }
  // Draw edges
  for (const e of lts.edges) {
    const sf = lts.states.find(s => s.id === e.from);
    const st = lts.states.find(s => s.id === e.to);
    const isSelf = e.from === e.to;
    const g = mk('g', { class: 'edge-btn' + (e.id === firedId ? ' fired' : e.id === repliedId ? ' replied' : '') });
    g.dataset.edgeId = e.id;
    if (isSelf) {
      // Self-loop arc above the node
      const cx = sf.x, cy = sf.y;
      const path = mk('path', { class: 'edge', d: `M${cx-8},${cy-14} C${cx-28},${cy-38} ${cx+28},${cy-38} ${cx+8},${cy-14}` });
      const arrow = mk('polygon', { points: `${cx+8},${cy-14} ${cx+4},${cy-22} ${cx+14},${cy-20}`, fill: '#4a7fa5', stroke: 'none', class: (e.id === firedId ? 'fired' : e.id === repliedId ? 'replied' : '') });
      if (e.id === firedId) { arrow.setAttribute('fill','#e63946'); } else if (e.id === repliedId) { arrow.setAttribute('fill','#0a7d33'); }
      const lbl = mk('text', { class: 'edge-label', x: cx, y: cy - 42, 'text-anchor': 'middle' });
      lbl.textContent = e.label;
      g.append(path, arrow, lbl);
    } else {
      // Straight directed edge with arrowhead
      const dx = st.x - sf.x, dy = st.y - sf.y, len = Math.hypot(dx, dy);
      const ux = dx / len, uy = dy / len;
      const r = 14;
      const x1 = sf.x + ux * r, y1 = sf.y + uy * r;
      const x2 = st.x - ux * r, y2 = st.y - uy * r;
      const path = mk('path', { class: 'edge', d: `M${x1},${y1} L${x2},${y2}` });
      const ax = x2 - ux*7 - uy*5, ay = y2 - uy*7 + ux*5;
      const bx = x2 - ux*7 + uy*5, by = y2 - uy*7 - ux*5;
      const arrow = mk('polygon', { points: `${x2},${y2} ${ax},${ay} ${bx},${by}`, fill: '#4a7fa5', stroke: 'none' });
      if (e.id === firedId) { arrow.setAttribute('fill','#e63946'); } else if (e.id === repliedId) { arrow.setAttribute('fill','#0a7d33'); }
      const mx = (x1 + x2) / 2 - uy * 9, my = (y1 + y2) / 2 + ux * 9;
      const lbl = mk('text', { class: 'edge-label', x: mx, y: my, 'text-anchor': 'middle' });
      lbl.textContent = e.label;
      g.append(path, arrow, lbl);
    }
    svgEl.appendChild(g);
  }
  // Draw state nodes on top of edges
  for (const s of lts.states) {
    const g = mk('g', { class: 'node', transform: `translate(${s.x},${s.y})` });
    const cls = s.id === curState ? 'current' : (s.visited ? 'visited' : 'plain');
    const c = mk('circle', { r: 14, class: cls, stroke: '#4a7fa5', 'stroke-width': 1.5 });
    const t = mk('text', { 'text-anchor': 'middle', dy: '0.35em' });
    t.textContent = s.id;
    g.append(c, t);
    svgEl.appendChild(g);
  }
}

function assignEdgeIds(lts, prefix) {
  // Assign stable string IDs to edges for fired/replied tracking
  lts.edges.forEach((e, i) => { e.id = prefix + '_e' + i; });
}

function setStatus(msg, cls) {
  const el = document.getElementById('status-bar');
  el.textContent = msg;
  el.className = 'status-bar ' + cls;
}

function loadExample(idx) {
  exIdx = idx;
  const ex = EXAMPLES[idx];
  assignEdgeIds(ex.A, 'A');
  assignEdgeIds(ex.B, 'B');
  curA = ex.A.init;
  curB = ex.B.init;
  firedEdge = null; repliedEdge = null;
  ex.A.states.forEach(s => { s.visited = false; });
  ex.B.states.forEach(s => { s.visited = false; });
  const isB = ex.bisim.length > 0;
  document.getElementById('hint-text').innerHTML = isB ? 'Systems A and B <strong>are bisimilar</strong>: every move has a matching reply. Click any arrow to play as the Attacker — the Defender replies automatically.' : 'Systems A and B <strong>are NOT bisimilar</strong>: after action <em>a</em>, System A must choose between <em>b</em> and <em>c</em>, while System B can do both from the same state. The Attacker wins by firing <em>a</em> to the branch the Defender cannot match.';
  setStatus('Click an arrow on either side to fire a move as the Attacker.', 'info');
  render();
}

function render() {
  const ex = EXAMPLES[exIdx];
  drawLTS(document.getElementById('svg-a'), ex.A, curA, firedEdge, repliedEdge);
  drawLTS(document.getElementById('svg-b'), ex.B, curB, firedEdge, repliedEdge);
  // Re-attach click listeners after every redraw
  attachListeners(document.getElementById('svg-a'), 'A', ex.A);
  attachListeners(document.getElementById('svg-b'), 'B', ex.B);
}

function findReply(fromSystem, toSystem, fromState, label, ex) {
  // Defender strategy: find an edge with the same label from the defender's current state
  // The Defender looks for an edge with the same label from toSystem's current state
  // such that the reached states are bisimilar to the attacker's target.
  const attEdge = fromSystem.edges.find(e => e.id === firedEdge);
  if (!attEdge) return null;
  const targetState = attEdge.to;
  for (const e of toSystem.edges) {
    if (e.from !== (toSystem === ex.A ? curA : curB)) continue;
    if (e.label !== label) continue;
    // Check that the reached pair is in the bisimulation relation
    const aState = toSystem === ex.A ? e.to : targetState;
    const bState = toSystem === ex.A ? targetState : e.to;
    if (isBisimilar(aState, bState, ex)) return e;
  }
  return null;
}

function attackFrom(side, edgeId, ex) {
  // Player fires a transition; defender auto-replies with best move
  const attSystem = side === 'A' ? ex.A : ex.B;
  const defSystem = side === 'A' ? ex.B : ex.A;
  const edge = attSystem.edges.find(e => e.id === edgeId);
  if (!edge) return;
  const curSrc = side === 'A' ? curA : curB;
  if (edge.from !== curSrc) {
    setStatus('That transition does not start from the current state.', 'bad'); return;
  }
  firedEdge = edgeId;
  // Advance attacker's current state
  if (side === 'A') { curA = edge.to; } else { curB = edge.to; }
  render();

  // Defender chooses a reply edge with matching label landing in a bisimilar pair
  const reply = findReply(attSystem, defSystem, edge.from, edge.label, ex);
  if (reply) {
    repliedEdge = reply.id;
    if (side === 'A') { curB = reply.to; } else { curA = reply.to; }
    setStatus(i18nFmt('Matched! Action '%label%' answered — systems still bisimilar.', { label: edge.label }), 'ok');
    render();
  } else {
    if (ex.bisim.length === 0) {
      setStatus(i18nFmt('No reply for action '%label%' — the Defender is stuck. Not bisimilar!', { label: edge.label }), 'bad');
    } else {
      setStatus(i18nFmt('No reply for action '%label%' — the Defender is stuck. Not bisimilar!', { label: edge.label }), 'bad');
    }
  }
}

function attachListeners(svgEl, side, lts) {
  // Attach click handlers to every edge group in the SVG
  for (const g of svgEl.querySelectorAll('.edge-btn')) {
    g.addEventListener('click', () => {
      attackFrom(side, g.dataset.edgeId, EXAMPLES[exIdx]);
    });
  }
}

document.getElementById('btn-example1').addEventListener('click', () => {
  document.querySelectorAll('.ex-btn').forEach(b => b.classList.remove('active'));
  document.getElementById('btn-example1').classList.add('active');
  loadExample(0);
});
document.getElementById('btn-example2').addEventListener('click', () => {
  document.querySelectorAll('.ex-btn').forEach(b => b.classList.remove('active'));
  document.getElementById('btn-example2').classList.add('active');
  loadExample(1);
});
document.getElementById('btn-reset').addEventListener('click', () => loadExample(exIdx));

loadExample(0);
Result
Console

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 aa and then be forced into bb, while System D can choose after aa; the Attacker exploits that branch to win.

The Real Complexity

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(mlog⁡n)O(m \log n) time, where nn is the number of states and mm 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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/bisimulation/Content licensed under CC BY-NC 4.0.