LTL Model Checker Demo

Introduction

Every digital system lives in time. A traffic light cycles through states. A network protocol sends, waits, and retries. A CPU fetches, executes, and writes back — again and again, forever. The bugs that matter most are not crashes but misbehaviors over time: a lock that is never released, a message that is sent but never acknowledged, a safety valve that stays open when it should eventually close.

Ordinary logic says "this is true now." Temporal logic lets us say things like "this will always be true," "this will eventually be true," and "whenever this happens, that will happen later." Two flavors dominate the field:

LTL (Linear Temporal Logic) imagines time as a single infinite path — the one execution you happen to be watching. It adds operators G ("globally / always"), F ("finally / eventually"), X ("next"), and U ("until"). A formula like G(request → F grant) means: on every step of this path, if a request is seen, some later step will see a grant.
CTL (Computation Tree Logic) imagines time as a tree of all possible futures branching out from the current state. It combines path quantifiers A ("for all paths") and E ("there exists a path") with the same temporal operators. AG(request → AF grant) means: on every path and at every state, if a request occurs, some future state on every continuation will grant it.

These two languages look almost identical. The difference is whether you reason along one fixed path or across all possible paths. That gap — which seems philosophical — turns out to matter enormously for how hard the verification problem is.

Model checking is the algorithmic question: given a finite system (a Kripke structure — states, transitions, and labels) and a formula, does the system satisfy the formula? In the 1980s Clarke, Emerson, and Sifakis invented efficient algorithms for CTL and shared the 2007 Turing Award. But LTL model checking, despite looking similar, is harder — it is PSPACE-complete (proven by Sistla and Clarke in 1985), while CTL model checking runs in polynomial time.

Try It

Below is a small Kripke structure — five states connected by transitions. Each state can have labels: R (request pending) and G (grant issued). Select a formula and press Check to see which states satisfy it. The demo traces paths and highlights violating states in red.

<p class="hint">A small <b>Kripke structure</b>: five states connected by transitions. Each state carries
    labels <b>R</b> (request) and/or <b>G</b> (grant). Pick a formula and press <b>Check</b> to see
    which states satisfy it — green = satisfied, red = violated.</p>
<div id="canvas-wrap"><canvas id="kripke" width="480" height="230"></canvas></div>
<div class="controls">
  <label for="formula">Formula:</label>
  <select id="formula">
    <option value="GRF">G(R → F G)  — LTL: every request is eventually granted</option>
    <option value="FG">F G  — LTL: grant is eventually seen</option>
    <option value="GnotR">G ¬R  — LTL: no request ever</option>
    <option value="EFG">EF G  — CTL: there exists a path reaching a grant state</option>
    <option value="AGR">AG R  — CTL: on all paths, R holds everywhere</option>
  </select>
  <button id="check" type="button">Check</button>
  <button id="reset" type="button" class="ghost">Reset</button>
</div>
<div id="result" class="result"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .6rem; line-height: 1.45; }
#canvas-wrap { border: 1px solid #cdd9e3; border-radius: 10px; overflow: hidden;
               background: #f5f8fa; margin-bottom: .6rem; }
canvas { display: block; max-width: 100%; }
.controls { display: flex; flex-wrap: wrap; gap: .5rem; align-items: center; margin-bottom: .5rem; }
label { font-size: .88rem; font-weight: 600; }
select { font: 14px system-ui,sans-serif; padding: .35rem .5rem; border: 1px solid #adb1b8;
         border-radius: 7px; background: #fff; flex: 1; min-width: 200px; }
button { font: 600 13px system-ui,sans-serif; padding: .4rem .85rem; border-radius: 7px;
         border: 1px solid #1d3557; background: #1d3557; color: #fff; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.result { font-size: .93rem; font-weight: 600; min-height: 1.4em; padding: .3rem 0; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }
.result.info { color: #1d3557; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Kripke structure: 5 states, transitions, labels.
// Label R = request, G = grant.
// s0 = initial state (double border).
const STATES = [
  { id: 0, name: 's0', x: 60,  y: 115, R: false, G: false },
  { id: 1, name: 's1', x: 160, y: 55,  R: true,  G: false },
  { id: 2, name: 's2', x: 280, y: 55,  R: true,  G: true  },
  { id: 3, name: 's3', x: 390, y: 115, R: false, G: true  },
  { id: 4, name: 's4', x: 220, y: 175, R: false, G: false }
];
// Directed transitions (every state has at least one successor)
const TRANS = [
  [0,1],[0,4],    // s0 → s1, s4
  [1,2],          // s1 → s2
  [2,3],[2,1],    // s2 → s3, s1  (can loop back: request repeats)
  [3,0],[3,4],    // s3 → s0, s4
  [4,4]           // s4 → s4  (sink: no R, no G, loops forever)
];

const succ = STATES.map(() => []);
TRANS.forEach(([a,b]) => succ[a].push(b));

let highlight = null; // null = unchecked; [{id, ok}] after check

// ── Drawing ─────────────────────────────────────────────────────────────────────────
const canvas = document.getElementById('kripke');
const ctx = canvas.getContext('2d');
const RN = 22; // node radius

function stateColor(s) {
  if (!highlight) return '#e8eef3';
  const h = highlight.find(h => h.id === s.id);
  return h ? (h.ok ? '#c8f0d3' : '#fcd0d0') : '#e8eef3';
}

function arrowHead(x, y, angle) {
  const sz = 7;
  ctx.beginPath();
  ctx.fillStyle = '#778';
  ctx.moveTo(x, y);
  ctx.lineTo(x - sz * Math.cos(angle - 0.38), y - sz * Math.sin(angle - 0.38));
  ctx.lineTo(x - sz * Math.cos(angle + 0.38), y - sz * Math.sin(angle + 0.38));
  ctx.closePath();
  ctx.fill();
}

function drawEdge(a, b) {
  ctx.beginPath();
  ctx.strokeStyle = '#778';
  ctx.lineWidth = 1.4;
  if (a === b) {
    // self-loop: small circle above the node
    const lx = STATES[a].x, ly = STATES[a].y - RN - 13;
    ctx.arc(lx, ly, 13, 0.25, Math.PI - 0.25, false);
    ctx.stroke();
    const ex = lx + 13 * Math.sin(0.25), ey = ly + 13 * (1 - Math.cos(0.25));
    arrowHead(ex, ey, Math.PI / 2 - 0.25);
    return;
  }
  const sx = STATES[a].x, sy = STATES[a].y;
  const ex = STATES[b].x, ey = STATES[b].y;
  const dx = ex - sx, dy = ey - sy, len = Math.hypot(dx, dy);
  const ux = dx / len, uy = dy / len;
  // shorten by radius
  const x1 = sx + ux * RN, y1 = sy + uy * RN;
  const x2 = ex - ux * RN, y2 = ey - uy * RN;
  // slight curve (offset perpendicular)
  const cx = (x1 + x2) / 2 - uy * 16, cy = (y1 + y2) / 2 + ux * 16;
  ctx.moveTo(x1, y1);
  ctx.quadraticCurveTo(cx, cy, x2, y2);
  ctx.stroke();
  arrowHead(x2, y2, Math.atan2(y2 - cy, x2 - cx));
}

function draw() {
  ctx.clearRect(0, 0, canvas.width, canvas.height);
  // edges
  TRANS.forEach(([a, b]) => drawEdge(a, b));
  // nodes
  STATES.forEach(s => {
    ctx.beginPath();
    ctx.arc(s.x, s.y, RN, 0, 2 * Math.PI);
    ctx.fillStyle = stateColor(s);
    ctx.strokeStyle = '#1d3557';
    ctx.lineWidth = s.id === 0 ? 2.6 : 1.6;
    ctx.fill(); ctx.stroke();
    // label
    ctx.fillStyle = '#1d3557';
    ctx.font = 'bold 11px system-ui,sans-serif';
    ctx.textAlign = 'center';
    ctx.textBaseline = 'middle';
    ctx.fillText((s.R ? 'R' : '') + (s.G ? 'G' : '') || '∅', s.x, s.y);
    // state name below node
    ctx.font = '10px system-ui,sans-serif';
    ctx.fillStyle = '#555';
    ctx.fillText(s.name, s.x, s.y + RN + 11);
  });
  // initial arrow into s0
  ctx.beginPath();
  ctx.moveTo(STATES[0].x - RN - 18, STATES[0].y);
  ctx.lineTo(STATES[0].x - RN, STATES[0].y);
  ctx.strokeStyle = '#1d3557'; ctx.lineWidth = 1.6; ctx.stroke();
  arrowHead(STATES[0].x - RN, STATES[0].y, 0);
}

// ── LTL model checking via lassos ────────────────────────────────────────────────
// Every infinite path in a finite Kripke structure is a lasso:
//   prefix[0..p-1] followed by cycle[0..c-1] repeated forever.
// We enumerate all lassos from a given start state via DFS.

function allLassos(start) {
  const lassos = [];
  function dfs(path, onStack) {
    const cur = path[path.length - 1];
    for (const n of succ[cur]) {
      if (onStack.has(n)) {
        // back-edge: cycle starts at first occurrence of n
        const ci = path.indexOf(n);
        lassos.push({ prefix: path.slice(0, ci), cycle: path.slice(ci) });
      } else {
        onStack.add(n);
        path.push(n);
        dfs(path, onStack);
        path.pop();
        onStack.delete(n);
      }
    }
  }
  const stack = new Set([start]);
  dfs([start], stack);
  return lassos;
}

// Check G(R → F G) on a lasso: on the infinite path, every R is followed by G.
// We look ahead into the cycle (≥2 repetitions) to handle R at cycle tail.
function lassoGRFG({ prefix, cycle }) {
  const full = [...prefix, ...cycle, ...cycle]; // 2 cycle unrolls covers all cases
  for (let i = 0; i < prefix.length + cycle.length; i++) {
    if (STATES[full[i]].R) {
      const found = full.slice(i).some(id => STATES[id].G);
      if (!found) return false;
    }
  }
  return true;
}

// F G: grant appears somewhere on the lasso
function lassoFG({ prefix, cycle }) {
  return [...prefix, ...cycle].some(id => STATES[id].G);
}

// G ¬R: no request anywhere on the lasso
function lassoGnotR({ prefix, cycle }) {
  return ![...prefix, ...cycle].some(id => STATES[id].R);
}

// LTL check: formula holds at startId iff it holds on ALL lassos from startId
function ltlCheck(startId, lassoFn) {
  return allLassos(startId).every(l => lassoFn(l));
}

// ── CTL model checking via fixpoint / reachability ────────────────────────────────────
// EF G: exists a path eventually reaching a G-state (BFS reachability)
function checkEFG(startId) {
  const vis = new Set([startId]);
  const q = [startId];
  while (q.length) {
    const cur = q.shift();
    if (STATES[cur].G) return true;
    succ[cur].forEach(n => { if (!vis.has(n)) { vis.add(n); q.push(n); } });
  }
  return false;
}

// AG R: on all reachable states, R holds (if any reachable state lacks R → false)
function checkAGR(startId) {
  const vis = new Set([startId]);
  const q = [startId];
  while (q.length) {
    const cur = q.shift();
    if (!STATES[cur].R) return false;
    succ[cur].forEach(n => { if (!vis.has(n)) { vis.add(n); q.push(n); } });
  }
  return true;
}

const CHECKERS = {
  GRF:   id => ltlCheck(id, lassoGRFG),
  FG:    id => ltlCheck(id, lassoFG),
  GnotR: id => ltlCheck(id, lassoGnotR),
  EFG:   id => checkEFG(id),
  AGR:   id => checkAGR(id)
};

const FORMULA_LABELS = {
  GRF:   'G(R → F G)',
  FG:    'F G',
  GnotR: 'G ¬R',
  EFG:   'EF G',
  AGR:   'AG R'
};

function runCheck() {
  const fid = document.getElementById('formula').value;
  const fname = FORMULA_LABELS[fid];
  highlight = STATES.map(s => ({ id: s.id, ok: CHECKERS[fid](s.id) }));
  const sat = highlight.filter(h => h.ok).map(h => STATES[h.id].name);
  const vio = highlight.filter(h => !h.ok).map(h => STATES[h.id].name);
  const res = document.getElementById('result');
  if (vio.length === 0) {
    res.textContent = fmt('✓ %fname% is satisfied at every state.', { fname: fname });
    res.className = 'result ok';
  } else if (sat.length === 0) {
    res.textContent = fmt('✗ %fname% is violated at every state.', { fname: fname });
    res.className = 'result bad';
  } else {
    res.textContent = fmt('%fname% holds at: %sat% | fails at: %vio%', { fname: fname, sat: sat.join(', '), vio: vio.join(', ') });
    res.className = 'result info';
  }
  console.log('Formula:', fname, '| sat:', sat, '| violated:', vio);
  draw();
}

document.getElementById('check').addEventListener('click', runCheck);
document.getElementById('reset').addEventListener('click', () => {
  highlight = null;
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
  draw();
});

draw();

<p class="hint">A small <b>Kripke structure</b>: five states connected by transitions. Each state carries
    labels <b>R</b> (request) and/or <b>G</b> (grant). Pick a formula and press <b>Check</b> to see
    which states satisfy it — green = satisfied, red = violated.</p>
<div id="canvas-wrap"><canvas id="kripke" width="480" height="230"></canvas></div>
<div class="controls">
  <label for="formula">Formula:</label>
  <select id="formula">
    <option value="GRF">G(R → F G)  — LTL: every request is eventually granted</option>
    <option value="FG">F G  — LTL: grant is eventually seen</option>
    <option value="GnotR">G ¬R  — LTL: no request ever</option>
    <option value="EFG">EF G  — CTL: there exists a path reaching a grant state</option>
    <option value="AGR">AG R  — CTL: on all paths, R holds everywhere</option>
  </select>
  <button id="check" type="button">Check</button>
  <button id="reset" type="button" class="ghost">Reset</button>
</div>
<div id="result" class="result"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .6rem; line-height: 1.45; }
#canvas-wrap { border: 1px solid #cdd9e3; border-radius: 10px; overflow: hidden;
               background: #f5f8fa; margin-bottom: .6rem; }
canvas { display: block; max-width: 100%; }
.controls { display: flex; flex-wrap: wrap; gap: .5rem; align-items: center; margin-bottom: .5rem; }
label { font-size: .88rem; font-weight: 600; }
select { font: 14px system-ui,sans-serif; padding: .35rem .5rem; border: 1px solid #adb1b8;
         border-radius: 7px; background: #fff; flex: 1; min-width: 200px; }
button { font: 600 13px system-ui,sans-serif; padding: .4rem .85rem; border-radius: 7px;
         border: 1px solid #1d3557; background: #1d3557; color: #fff; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.result { font-size: .93rem; font-weight: 600; min-height: 1.4em; padding: .3rem 0; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }
.result.info { color: #1d3557; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Kripke structure: 5 states, transitions, labels.
// Label R = request, G = grant.
// s0 = initial state (double border).
const STATES = [
  { id: 0, name: 's0', x: 60,  y: 115, R: false, G: false },
  { id: 1, name: 's1', x: 160, y: 55,  R: true,  G: false },
  { id: 2, name: 's2', x: 280, y: 55,  R: true,  G: true  },
  { id: 3, name: 's3', x: 390, y: 115, R: false, G: true  },
  { id: 4, name: 's4', x: 220, y: 175, R: false, G: false }
];
// Directed transitions (every state has at least one successor)
const TRANS = [
  [0,1],[0,4],    // s0 → s1, s4
  [1,2],          // s1 → s2
  [2,3],[2,1],    // s2 → s3, s1  (can loop back: request repeats)
  [3,0],[3,4],    // s3 → s0, s4
  [4,4]           // s4 → s4  (sink: no R, no G, loops forever)
];

const succ = STATES.map(() => []);
TRANS.forEach(([a,b]) => succ[a].push(b));

let highlight = null; // null = unchecked; [{id, ok}] after check

// ── Drawing ─────────────────────────────────────────────────────────────────────────
const canvas = document.getElementById('kripke');
const ctx = canvas.getContext('2d');
const RN = 22; // node radius

function stateColor(s) {
  if (!highlight) return '#e8eef3';
  const h = highlight.find(h => h.id === s.id);
  return h ? (h.ok ? '#c8f0d3' : '#fcd0d0') : '#e8eef3';
}

function arrowHead(x, y, angle) {
  const sz = 7;
  ctx.beginPath();
  ctx.fillStyle = '#778';
  ctx.moveTo(x, y);
  ctx.lineTo(x - sz * Math.cos(angle - 0.38), y - sz * Math.sin(angle - 0.38));
  ctx.lineTo(x - sz * Math.cos(angle + 0.38), y - sz * Math.sin(angle + 0.38));
  ctx.closePath();
  ctx.fill();
}

function drawEdge(a, b) {
  ctx.beginPath();
  ctx.strokeStyle = '#778';
  ctx.lineWidth = 1.4;
  if (a === b) {
    // self-loop: small circle above the node
    const lx = STATES[a].x, ly = STATES[a].y - RN - 13;
    ctx.arc(lx, ly, 13, 0.25, Math.PI - 0.25, false);
    ctx.stroke();
    const ex = lx + 13 * Math.sin(0.25), ey = ly + 13 * (1 - Math.cos(0.25));
    arrowHead(ex, ey, Math.PI / 2 - 0.25);
    return;
  }
  const sx = STATES[a].x, sy = STATES[a].y;
  const ex = STATES[b].x, ey = STATES[b].y;
  const dx = ex - sx, dy = ey - sy, len = Math.hypot(dx, dy);
  const ux = dx / len, uy = dy / len;
  // shorten by radius
  const x1 = sx + ux * RN, y1 = sy + uy * RN;
  const x2 = ex - ux * RN, y2 = ey - uy * RN;
  // slight curve (offset perpendicular)
  const cx = (x1 + x2) / 2 - uy * 16, cy = (y1 + y2) / 2 + ux * 16;
  ctx.moveTo(x1, y1);
  ctx.quadraticCurveTo(cx, cy, x2, y2);
  ctx.stroke();
  arrowHead(x2, y2, Math.atan2(y2 - cy, x2 - cx));
}

function draw() {
  ctx.clearRect(0, 0, canvas.width, canvas.height);
  // edges
  TRANS.forEach(([a, b]) => drawEdge(a, b));
  // nodes
  STATES.forEach(s => {
    ctx.beginPath();
    ctx.arc(s.x, s.y, RN, 0, 2 * Math.PI);
    ctx.fillStyle = stateColor(s);
    ctx.strokeStyle = '#1d3557';
    ctx.lineWidth = s.id === 0 ? 2.6 : 1.6;
    ctx.fill(); ctx.stroke();
    // label
    ctx.fillStyle = '#1d3557';
    ctx.font = 'bold 11px system-ui,sans-serif';
    ctx.textAlign = 'center';
    ctx.textBaseline = 'middle';
    ctx.fillText((s.R ? 'R' : '') + (s.G ? 'G' : '') || '∅', s.x, s.y);
    // state name below node
    ctx.font = '10px system-ui,sans-serif';
    ctx.fillStyle = '#555';
    ctx.fillText(s.name, s.x, s.y + RN + 11);
  });
  // initial arrow into s0
  ctx.beginPath();
  ctx.moveTo(STATES[0].x - RN - 18, STATES[0].y);
  ctx.lineTo(STATES[0].x - RN, STATES[0].y);
  ctx.strokeStyle = '#1d3557'; ctx.lineWidth = 1.6; ctx.stroke();
  arrowHead(STATES[0].x - RN, STATES[0].y, 0);
}

// ── LTL model checking via lassos ────────────────────────────────────────────────
// Every infinite path in a finite Kripke structure is a lasso:
//   prefix[0..p-1] followed by cycle[0..c-1] repeated forever.
// We enumerate all lassos from a given start state via DFS.

function allLassos(start) {
  const lassos = [];
  function dfs(path, onStack) {
    const cur = path[path.length - 1];
    for (const n of succ[cur]) {
      if (onStack.has(n)) {
        // back-edge: cycle starts at first occurrence of n
        const ci = path.indexOf(n);
        lassos.push({ prefix: path.slice(0, ci), cycle: path.slice(ci) });
      } else {
        onStack.add(n);
        path.push(n);
        dfs(path, onStack);
        path.pop();
        onStack.delete(n);
      }
    }
  }
  const stack = new Set([start]);
  dfs([start], stack);
  return lassos;
}

// Check G(R → F G) on a lasso: on the infinite path, every R is followed by G.
// We look ahead into the cycle (≥2 repetitions) to handle R at cycle tail.
function lassoGRFG({ prefix, cycle }) {
  const full = [...prefix, ...cycle, ...cycle]; // 2 cycle unrolls covers all cases
  for (let i = 0; i < prefix.length + cycle.length; i++) {
    if (STATES[full[i]].R) {
      const found = full.slice(i).some(id => STATES[id].G);
      if (!found) return false;
    }
  }
  return true;
}

// F G: grant appears somewhere on the lasso
function lassoFG({ prefix, cycle }) {
  return [...prefix, ...cycle].some(id => STATES[id].G);
}

// G ¬R: no request anywhere on the lasso
function lassoGnotR({ prefix, cycle }) {
  return ![...prefix, ...cycle].some(id => STATES[id].R);
}

// LTL check: formula holds at startId iff it holds on ALL lassos from startId
function ltlCheck(startId, lassoFn) {
  return allLassos(startId).every(l => lassoFn(l));
}

// ── CTL model checking via fixpoint / reachability ────────────────────────────────────
// EF G: exists a path eventually reaching a G-state (BFS reachability)
function checkEFG(startId) {
  const vis = new Set([startId]);
  const q = [startId];
  while (q.length) {
    const cur = q.shift();
    if (STATES[cur].G) return true;
    succ[cur].forEach(n => { if (!vis.has(n)) { vis.add(n); q.push(n); } });
  }
  return false;
}

// AG R: on all reachable states, R holds (if any reachable state lacks R → false)
function checkAGR(startId) {
  const vis = new Set([startId]);
  const q = [startId];
  while (q.length) {
    const cur = q.shift();
    if (!STATES[cur].R) return false;
    succ[cur].forEach(n => { if (!vis.has(n)) { vis.add(n); q.push(n); } });
  }
  return true;
}

const CHECKERS = {
  GRF:   id => ltlCheck(id, lassoGRFG),
  FG:    id => ltlCheck(id, lassoFG),
  GnotR: id => ltlCheck(id, lassoGnotR),
  EFG:   id => checkEFG(id),
  AGR:   id => checkAGR(id)
};

const FORMULA_LABELS = {
  GRF:   'G(R → F G)',
  FG:    'F G',
  GnotR: 'G ¬R',
  EFG:   'EF G',
  AGR:   'AG R'
};

function runCheck() {
  const fid = document.getElementById('formula').value;
  const fname = FORMULA_LABELS[fid];
  highlight = STATES.map(s => ({ id: s.id, ok: CHECKERS[fid](s.id) }));
  const sat = highlight.filter(h => h.ok).map(h => STATES[h.id].name);
  const vio = highlight.filter(h => !h.ok).map(h => STATES[h.id].name);
  const res = document.getElementById('result');
  if (vio.length === 0) {
    res.textContent = fmt('✓ %fname% is satisfied at every state.', { fname: fname });
    res.className = 'result ok';
  } else if (sat.length === 0) {
    res.textContent = fmt('✗ %fname% is violated at every state.', { fname: fname });
    res.className = 'result bad';
  } else {
    res.textContent = fmt('%fname% holds at: %sat% | fails at: %vio%', { fname: fname, sat: sat.join(', '), vio: vio.join(', ') });
    res.className = 'result info';
  }
  console.log('Formula:', fname, '| sat:', sat, '| violated:', vio);
  draw();
}

document.getElementById('check').addEventListener('click', runCheck);
document.getElementById('reset').addEventListener('click', () => {
  highlight = null;
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
  draw();
});

draw();

Result

Console

Notice: checking G(R → F G) requires following every infinite path that starts from each state. Even on this tiny five-state system the checker must reason about infinitely long behaviors — it does so by finding cycles. Increasing the state count even modestly makes the path set explode. That exponential character is exactly what puts LTL model checking in PSPACE.

Compare with EF G (a CTL formula: "there exists a path on which G is eventually true"). The checker answers that by a simple reachability search — no path enumeration needed — which is why CTL stays polynomial.

The Real Complexity

The complexity gap between LTL and CTL is one of the cleanest lessons in formal verification:

CTL model checking is in PTIME. Emerson and Clarke (1981) gave an algorithm that marks states bottom-up in the formula's syntax tree. Each operator adds one pass over the state graph. Total time is O(|formula| × |states + transitions|) — polynomial in the input size.
LTL model checking is PSPACE-complete. Sistla and Clarke (1985) proved both directions. The key insight: to check an LTL formula φ on a system M, you build the product of M with a Büchi automaton for ¬φ (an automaton that accepts exactly the paths violating φ). The automaton can be exponentially large in |φ|, and the reachability problem on the product requires PSPACE. Conversely, PSPACE-hard problems (like QBF — quantified Boolean formulas) can be encoded as LTL model-checking instances.
The culprit is path quantification. LTL implicitly says "for all paths." Checking that universally over a system with cycles means reasoning about all infinite paths at once. CTL's explicit path quantifiers (A, E) allow the algorithm to handle them one-by-one with local fixpoint computations, avoiding the blowup.
Satisfiability is even harder. Deciding whether an LTL formula has any model at all (not tied to a fixed system) is also PSPACE-complete. CTL satisfiability is EXPTIME-complete.

The takeaway: adding time to logic does not automatically make verification hard, but which paths you quantify over — and how — determines whether you stay in P or climb to PSPACE. This same tension appears in the halting problem: asking "does this program halt on this input" is undecidable, but asking "does some short program halt" is much more tractable.

Where It Matters

Temporal logic is not academic exercise — it is the engine of industrial correctness:

Hardware verification: Intel, AMD, and ARM use CTL-based model checkers to find design bugs before tape-out. The famous Pentium FDIV bug (1994) cost Intel $475 million and accelerated adoption of formal verification. Modern processor designs are routinely checked against tens of thousands of CTL properties.
Protocol verification: Network and security protocols are modeled as finite state machines and checked against LTL safety and liveness properties. Tools like SPIN (Gerard Holzmann) use LTL on-the-fly to verify protocols like the sliding-window protocol and the ISO OSI layers.
Reactive systems and operating systems: Properties like "the scheduler will eventually give every process CPU time" (a fairness property) or "a mutex is never held by two threads simultaneously" (a safety property) are expressed in LTL or CTL and checked against models of the OS kernel.
Autonomous and safety-critical systems: Aerospace and automotive standards (DO-178C, ISO 26262) increasingly require formal verification of control software. NASA's Mars rovers and flight software are checked against temporal specifications.
Software model checkers: Tools like Java PathFinder and CBMC check Java and C programs against LTL properties by treating the program's state space as a Kripke structure — bridging the gap between theory and everyday engineering.

The PSPACE barrier for LTL means industrial tools use clever abstractions, partial-order reduction, and symbolic methods (BDDs, SAT/SMT) to handle systems far too large for naive enumeration. See also the related challenge in SAT — both fields share the same algorithmic tricks for taming exponential-seeming problems in practice.

Conclusion

LTL and CTL are twins separated by a single design choice: does the logic reason along one fixed path, or does it explicitly branch over all futures? That choice moves the model-checking problem from polynomial time (CTL) to PSPACE-complete (LTL) — a gap that, under standard complexity assumptions, represents an exponential difference in resources.

The lesson is broader than temporal logic. How you quantify over possibilities — whether you commit to one path, range over all paths, or let the formula choose — is often what makes a problem easy or intractably hard. LTL and CTL sit at opposite ends of that spectrum while looking almost identical to the eye.

Model checking began in the early 1980s as a theoretical curiosity and became one of the most impactful tools in modern engineering. Every CPU you use has been checked against thousands of temporal properties. The next time a traffic light behaves correctly, or a network packet arrives in order, or a safety-critical system holds its invariant under stress — there is a good chance that some descendant of LTL or CTL model checking played a role in making that guarantee.

Comments

Loading comments...

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

Cookies & privacy

LTL and CTL

When 'always eventually' hides a PSPACE-complete question