Introduction

Software and hardware bugs can kill. A single mistake in an aircraft's flight-control code, a pacemaker's firmware, or a chip's cache-coherence protocol can be catastrophic — and traditional testing can only check the cases you thought to write down.

Model checking is a radically different approach: instead of testing samples, a computer exhaustively explores every state a system can reach and checks whether a given property holds in all of them. If the property fails anywhere, the tool hands you a concrete counterexample — the exact sequence of events that triggers the bug.

The technique was independently invented in the early 1980s by Edmund Clarke and E. Allen Emerson at Harvard/MIT and by Joseph Sifakis in Grenoble. In 2007, all three received the Turing Award — computer science's highest honour — for this work.

The key ingredients are two: a Kripke structure (a directed graph whose nodes are system states and edges are transitions, with each node labelled by facts that hold there) and a temporal-logic formula that expresses what should always or eventually be true. The checker traverses the graph and decides whether the formula holds — automatically, rigorously, and without a single line of manual proof.

Try It

The demo below models a classic two-process mutual-exclusion protocol. Each process cycles through three phases: Idle → Trying → Critical. The safety property to verify is AG ¬(crit1crit_{1} ∧ crit2crit_{2}) — "in every reachable state, it is never the case that both processes are in the critical section simultaneously".

<p class="hint">
  A <b>Kripke structure</b> for a 2-process mutual-exclusion protocol.<br>
      Each process: <em>Idle(I) → Trying(T) → Critical(C)</em>.<br>
      Property: <code>AG ¬(crit₁ ∧ crit₂)</code> — both never in critical at once.
</p>
<div id="graph-area">
  <canvas id="canvas" width="560" height="280"></canvas>
</div>
<div class="result-area" id="result"></div>
<div class="btns">
  <button id="btn-verify" type="button">Verify property</button>
  <button id="btn-bug" type="button" class="ghost">Inject bug</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="legend">
  <span class="leg-ok">■</span> Safe state &nbsp;
  <span class="leg-cex">■</span> Counterexample state &nbsp;
  <span class="leg-init">●</span> Initial state
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .85rem; color: #444; margin: 0 0 .6rem; line-height: 1.5; }
#graph-area { border: 1px solid #cdd9e3; border-radius: 8px; background: #f7f9fb; overflow: hidden; margin-bottom: .5rem; }
canvas { display: block; max-width: 100%; }
.result-area { min-height: 1.6em; font-weight: 600; font-size: .95rem; margin-bottom: .4rem; padding: .3rem .5rem; border-radius: 6px; }
.result-area.ok { background: #e6f4ec; color: #0a7d33; }
.result-area.bad { background: #fdecea; color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .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; }
.legend { font-size: .78rem; color: #555; }
.leg-ok { color: #3a8f5c; }
.leg-cex { color: #c92f3c; }
.leg-init { color: #1d3557; font-size: 1em; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ── Model: 2-process mutex (Peterson-style, simplified) ────────────────────
// State = (p1_phase, p2_phase)  where phase ∈ {I=0, T=1, C=2}
// Transitions: each process independently advances one step at a time.
// Guard for entering Critical: the OTHER process must NOT be in C (safe)
//   OR (bugged) no guard at all.
// We build the full Kripke structure and run CTL model checking for
//   AG ¬(p1==C ∧ p2==C)   ("never both critical")

const PHASE = ['I','T','C'];
let bugged = false;

function stateId(p1, p2) { return p1 * 3 + p2; }
function stateLabel(id) { return '(' + PHASE[Math.floor(id/3)] + ',' + PHASE[id%3] + ')'; }
function isCritical1(id) { return Math.floor(id/3) === 2; }
function isCritical2(id) { return id % 3 === 2; }

// Build transitions. Process 1 advances p1; process 2 advances p2.
// T→C requires the other process NOT in C (unless bugged).
function buildKripke() {
  const succ = Array.from({length: 9}, () => []);
  for (let p1 = 0; p1 < 3; p1++) {
    for (let p2 = 0; p2 < 3; p2++) {
      const s = stateId(p1, p2);
      // Process 1 takes a step
      let np1 = (p1 + 1) % 3;
      if (p1 === 1 && !bugged && p2 === 2) np1 = 1; // blocked: p2 in C
      if (np1 !== p1) succ[s].push(stateId(np1, p2));
      // Process 2 takes a step
      let np2 = (p2 + 1) % 3;
      if (p2 === 1 && !bugged && p1 === 2) np2 = 1; // blocked: p1 in C
      if (np2 !== p2) succ[s].push(stateId(p1, np2));
      // If deadlock prevention: always allow staying (self-loop when blocked)
      if (succ[s].length === 0) succ[s].push(s);
    }
  }
  return succ;
}

// CTL model checking: AG ¬(crit1 ∧ crit2)
// AG p  ≡  ¬EF ¬p  — no path reaches a state violating p.
// We compute EF(bad) via backward BFS from bad states.
function checkAGnoDoubleCrit(succ) {
  const n = 9;
  // Bad states: both critical
  const bad = new Set();
  for (let s = 0; s < n; s++) if (isCritical1(s) && isCritical2(s)) bad.add(s);

  // Reverse graph
  const pred = Array.from({length: n}, () => []);
  for (let s = 0; s < n; s++) for (const t of succ[s]) pred[t].push(s);

  // BFS: EF(bad) — states that can reach a bad state
  const efBad = new Set(bad);
  const queue = [...bad];
  while (queue.length) {
    const t = queue.shift();
    for (const s of pred[t]) {
      if (!efBad.has(s)) { efBad.add(s); queue.push(s); }
    }
  }
  return { efBad };
}

// ── Reachability from initial state (0,0) = (I,I) ────────────────────────
function reachable(succ) {
  const visited = new Set([0]);
  const queue = [0];
  while (queue.length) {
    const s = queue.shift();
    for (const t of succ[s]) if (!visited.has(t)) { visited.add(t); queue.push(t); }
  }
  return visited;
}

// ── Layout: 3×3 grid of states ────────────────────────────────────────
const PAD = 40, CELL = 80;
function statePos(id) {
  const p1 = Math.floor(id / 3), p2 = id % 3;
  return { x: PAD + p2 * CELL + CELL/2, y: PAD + p1 * CELL + CELL/2 };
}

let verifyResult = null;

function draw() {
  const canvas = document.getElementById('canvas');
  const ctx = canvas.getContext('2d');
  ctx.clearRect(0, 0, canvas.width, canvas.height);

  const succ = buildKripke();
  const reach = reachable(succ);
  let efBad = null;
  if (verifyResult) efBad = verifyResult.efBad;

  // Draw axes labels
  ctx.fillStyle = '#666'; ctx.font = '11px system-ui';
  ctx.fillText('p₁\\p₂', 4, 16);
  for (let i = 0; i < 3; i++) {
    ctx.fillText(PHASE[i], PAD + i * CELL + CELL/2 - 4, 26);
    ctx.fillText(PHASE[i], 8, PAD + i * CELL + CELL/2 + 4);
  }

  // Draw edges
  for (let s = 0; s < 9; s++) {
    if (!reach.has(s)) continue;
    const from = statePos(s);
    for (const t of succ[s]) {
      if (s === t) continue; // skip self-loops for clarity
      const to = statePos(t);
      drawArrow(ctx, from.x, from.y, to.x, to.y, 18);
    }
  }

  // Draw states
  for (let s = 0; s < 9; s++) {
    const { x, y } = statePos(s);
    const inReach = reach.has(s);
    const isBad = isCritical1(s) && isCritical2(s);
    const inCex = efBad && efBad.has(s) && inReach;

    ctx.beginPath();
    ctx.arc(x, y, 18, 0, 2 * Math.PI);
    if (!inReach) {
      ctx.fillStyle = '#e8eef3'; ctx.strokeStyle = '#cdd9e3';
    } else if (efBad && inCex) {
      ctx.fillStyle = isBad ? '#c92f3c' : '#fdecea'; ctx.strokeStyle = '#c92f3c';
    } else if (efBad) {
      ctx.fillStyle = '#e6f4ec'; ctx.strokeStyle = '#3a8f5c';
    } else {
      ctx.fillStyle = '#dde7f2'; ctx.strokeStyle = '#4a6fa5';
    }
    ctx.lineWidth = s === 0 ? 2.5 : 1.5;
    ctx.fill(); ctx.stroke();

    ctx.fillStyle = inReach ? '#1d3557' : '#aaa';
    ctx.font = 'bold 11px ui-monospace, monospace';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(stateLabel(s), x, y);
  }
  // Initial state indicator
  const init = statePos(0);
  ctx.font = 'bold 18px system-ui';
  ctx.fillStyle = '#1d3557';
  ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
  ctx.fillText('●', init.x - 28, init.y);
}

function drawArrow(ctx, x1, y1, x2, y2, r) {
  const dx = x2 - x1, dy = y2 - y1;
  const len = Math.sqrt(dx*dx + dy*dy);
  const ux = dx/len, uy = dy/len;
  const sx = x1 + ux*r, sy = y1 + uy*r;
  const ex = x2 - ux*(r+4), ey = y2 - uy*(r+4);
  ctx.beginPath();
  ctx.moveTo(sx, sy); ctx.lineTo(ex, ey);
  ctx.strokeStyle = '#6b8fa8'; ctx.lineWidth = 1.2; ctx.stroke();
  // Arrowhead
  const angle = Math.atan2(ey - sy, ex - sx);
  ctx.beginPath();
  ctx.moveTo(ex, ey);
  ctx.lineTo(ex - 7*Math.cos(angle-0.4), ey - 7*Math.sin(angle-0.4));
  ctx.lineTo(ex - 7*Math.cos(angle+0.4), ey - 7*Math.sin(angle+0.4));
  ctx.closePath();
  ctx.fillStyle = '#6b8fa8'; ctx.fill();
}

function setResult(msg, cls) {
  const el = document.getElementById('result');
  el.textContent = msg; el.className = 'result-area ' + cls;
}

document.getElementById('btn-verify').addEventListener('click', () => {
  const succ = buildKripke();
  const reach = reachable(succ);
  const { efBad } = checkAGnoDoubleCrit(succ);
  // Check if initial state (0) is in EF(bad) — property violated
  const violated = efBad.has(0);
  // Find a witness state in reach ∩ efBad for reporting
  const badStates = [...reach].filter(s => isCritical1(s) && isCritical2(s));
  verifyResult = { efBad };
  if (violated) {
    setResult(fmt('✗ COUNTEREXAMPLE found — %map% reachable from (I,I)', { map: badStates.map(stateLabel).join(', ') }), 'bad');
    console.log('Counterexample: EF(bad) states reachable:', [...efBad].filter(s => reach.has(s)).map(stateLabel).join(', '));
  } else {
    setResult(fmt('✓ VERIFIED — AG ¬(crit₁ ∧ crit₂) holds over all %size% reachable states', { size: reach.size }), 'ok');
    console.log('Verified: reachable states:', [...reach].map(stateLabel).join(', '));
  }
  draw();
});

document.getElementById('btn-bug').addEventListener('click', () => {
  bugged = true; verifyResult = null;
  setResult('Bug injected — guard removed. Click "Verify property" to see the counterexample.', '');
  draw();
});

document.getElementById('btn-reset').addEventListener('click', () => {
  bugged = false; verifyResult = null;
  setResult('', '');
  draw();
});

draw();
Result
Console

Click Verify property to run the CTL model checker over all reachable states. Click Inject bug to remove the mutual-exclusion guard and watch the checker find a counterexample automatically. Reset restores the correct protocol.

Notice how verification is instant regardless of which property you check — the checker visits every state exactly once. Adding a third process would expand the state space but the algorithm still terminates. The hard limit is memory: state spaces grow exponentially with the number of concurrent components.

The Real Complexity

Model checking sits in a sweet spot of decidability — but the state explosion problem is a constant adversary.

  • CTL model checking (the logic used in this article) runs in O(|M| × |φ|) time — linear in the product of the model size and the formula length. This is a celebrated result proved by Clarke and Emerson in 1981.
  • LTL model checking (linear temporal logic, which reasons about infinite paths) is PSPACE-complete — still decidable, but the constants are much larger in practice.
  • The state explosion problem: a system with n boolean variables has up to 2n2^{n} states. Two concurrent components with 10 states each give 100 combined states; ten components give 101010^{10}. The model grows exponentially in the number of parallel components.
  • Symbolic model checking (using BDDs — Binary Decision Diagrams) compresses the state space dramatically and was the key practical breakthrough of the 1990s, enabling verification of hardware designs with 1012010^{120} states.
  • Undecidability lurks nearby: model checking for infinite-state systems (real programs with unbounded stacks or heaps) is undecidable — a direct relative of the halting problem.

The status: model checking for CTL over finite-state systems is solved — it runs in polynomial time and has been deployed industrially for decades. The frontier is pushing those boundaries to larger and more realistic models.

Where It Matters

Model checking has moved from theory to the centre of industrial practice:

  • Hardware design: Intel used model checking after the infamous Pentium FDIV bug (1994) cost them $475 million. Today formal verification is standard in every major chip design flow.
  • Network protocols: the cache-coherence protocols in multicore CPUs — ensuring that two cores never see inconsistent memory — are routinely verified by model checkers.
  • Aerospace and safety-critical software: NASA's Jet Propulsion Laboratory used model checking to verify parts of the Mars rovers' software. Tools like SPIN and NuSMV are part of avionics certification pipelines.
  • Security protocols: TLS, OAuth, and cryptographic protocols have been analyzed with tools like ProVerif and Tamarin, which use model-checking ideas to find authentication flaws automatically.
  • Autonomous vehicles: the state machines governing lane-change decisions and emergency braking are natural candidates for model checking before deployment.

The common thread: any system you can describe as a finite graph with labeled states is a candidate. Related verification ideas also underpin program equivalence and program synthesis.

Conclusion

Model checking is one of computer science's great success stories: a technique born in academic papers in the early 1980s that now runs inside the verification flows of every major chip maker, aerospace company, and cloud-infrastructure team.

Its core insight is elegant — turn "does this system satisfy this property?" into a graph-reachability problem and solve it exhaustively. CTL model checking does so in time linear in the state space, producing either a proof or a concrete counterexample. The state explosion problem is real, but decades of engineering (BDDs, SAT-based bounded model checking, abstraction-refinement) have pushed the frontier far enough to verify systems with astronomical state counts.

The boundary with undecidability is always close — step outside finite-state systems and the halting problem reasserts itself. But within those boundaries, model checking is as close to automated correctness as computer science has ever achieved.

Share this article

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

Comments

Loading comments...

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