I built, stress-tested, and cross-validated a complete implementation. The final self-contained document is at ~/ltl-checker/SOLUTION.md; its full content follows.
Implement an LTL model checker that
holds together with the number of explored states.The reference implementation below is written for Node.js (>= 18) and has no dependencies.
The class of failures this problem targets comes from four distinct places. Each was reproduced and then eliminated:
An LTL tableau creates one acceptance set per until sub-formula. For φ = a U b the acceptance set is
F_φ = { s | b ∈ s OR φ ∉ s }
A naive checker uses a single "accepting" predicate (e.g. "the node contains some right-hand side"), so a cycle that discharges one pending until but never discharges another is wrongly accepted. Fix: degeneralize with a modulo-k counter: from state (q, c), advance to c+1 when q ∈ F_c; a state is accepting iff q ∈ F_c. A run is accepting iff the counter wraps infinitely often, which forces every F_c to be visited infinitely often.
A common shortcut is to look for a state q that can reach an accepting state and is reachable from it, or to stop at the first back-edge in DFS. That accepts a partial SCC: two different SCCs can each satisfy a different acceptance set without any single cycle satisfying all of them. Reproduced with three states A→C→A, A→B→B, F_0={A}, F_1={B} — all reachable, yet no accepting cycle. Fix: the emptiness check must find one cycle on which the degeneralized counter returns to its initial value (equivalently: a reachable non-trivial SCC containing an accepting state). The degeneralized nested DFS does exactly this.
The inner DFS must (a) start at an accepting state, (b) only traverse states currently on the outer DFS stack, and (c) return to the same seed state. If the inner search ignores the outer stack, or stops at any accepting state, it can report a path that is not a closed cycle. Fix: innerIter below only recurses into onStack states and terminates only when it reaches the seed again, then emits the closed cycle.
Returning only the cycle, or concatenating prefix and cycle with the shared state duplicated, gives an invalid lasso. Fix: keep the outer DFS parent tree; prefix is the tree path from an initial state to the accepting seed; cycle is the inner-DFS path seed → … → seed. The lasso is prefix ++ cycle[1..], so prefix.at(-1) === cycle[0] === cycle.at(-1).
A stack-recursive DFS overflows on long products. Fix: both DFSs are implemented iteratively with explicit stacks.
ltl.js)'use strict';
/*
* On-the-fly LTL model checker (tableau GBA + degeneralization + nested DFS).
*
* Pipeline:
* 1. parse LTL formula -> AST
* 2. NNF + negation -> negation-normal form of !phi
* 3. tableau expansion -> generalized Buchi automaton (on demand)
* 4. product with Kripke structure -> GBA (on demand)
* 5. degeneralize + nested DFS -> accepting cycle / counterexample lasso
*
* Public API:
* findAcceptingCycle(gba) generic emptiness check for a (generalized) Buchi
* automaton; returns { hasAcceptingCycle, prefix,
* cycle, statesExplored }
* checkLTL(model, formula) full LTL model check; returns
* {
* result: 'holds' | 'violated',
* status: 'holds' | 'violated', // alias
* holds: boolean,
* statesExplored: number, // distinct product (model,tableau) states
* prefix: string[], // model states, initial .. cycle entry
* cycle: string[], // model states, entry .. entry (closed)
* lasso: string[], // prefix + cycle[1..]
* counterexample: string[] // alias of lasso
* }
*
* Accepted model shapes:
* explicit: { initial: [...], transitions: { s: [t,...] }, labels: { s: [atom,...] } }
* functional: { initialStates: [...], successors(s)->[...], labels(s)->[...] }
*/
/* ------------------------------------------------------------------ */
/* 1. Parser */
/* ------------------------------------------------------------------ */
function tokenize(src) {
const toks = [];
let i = 0;
while (i < src.length) {
const c = src[i];
if (/\s/.test(c)) { i++; continue; }
if (c === '(' || c === ')') { toks.push({ type: c }); i++; continue; }
if (c === '!' || c === '~' || c === '\u00ac') { toks.push({ type: 'not' }); i++; continue; }
if (c === '&' || c === '\u2227') { toks.push({ type: 'and' }); i += c === '&' && src[i + 1] === '&' ? 2 : 1; continue; }
if (c === '|' || c === '\u2228') { toks.push({ type: 'or' }); i += c === '|' && src[i + 1] === '|' ? 2 : 1; continue; }
if (c === '/' && src[i + 1] === '\\') { toks.push({ type: 'and' }); i += 2; continue; }
if (c === '\\' && src[i + 1] === '/') { toks.push({ type: 'or' }); i += 2; continue; }
if (c === '-' && src[i + 1] === '>') { toks.push({ type: 'imp' }); i += 2; continue; }
if (c === '\u2192') { toks.push({ type: 'imp' }); i++; continue; }
if (/[A-Za-z_]/.test(c)) {
let j = i;
while (j < src.length && /[A-Za-z0-9_]/.test(src[j])) j++;
toks.push({ type: 'id', value: src.slice(i, j) });
i = j;
continue;
}
throw new Error(`LTL parse error: unexpected character '${c}' at ${i}`);
}
return toks;
}
function parse(src) {
const toks = tokenize(src);
let pos = 0;
const peek = () => toks[pos];
const eat = (t) => { if (!peek() || peek().type !== t) throw new Error(`LTL parse error: expected ${t}`); return toks[pos++]; };
const isId = (v) => peek() && peek().type === 'id' && peek().value === v;
// precedence: imp < U/R < or < and < unary
function pImp() {
const left = pUntil();
if (peek() && peek().type === 'imp') { pos++; return { type: 'imp', left, right: pImp() }; }
return left;
}
function pUntil() {
let left = pOr();
while (isId('U') || isId('R')) {
const op = toks[pos++].value;
const right = pOr();
left = { type: op === 'U' ? 'until' : 'release', left, right };
}
return left;
}
function pOr() {
let left = pAnd();
while (peek() && peek().type === 'or') { pos++; left = { type: 'or', left, right: pAnd() }; }
return left;
}
function pAnd() {
let left = pUnary();
while (peek() && peek().type === 'and') { pos++; left = { type: 'and', left, right: pUnary() }; }
return left;
}
function pUnary() {
const t = peek();
if (!t) throw new Error('LTL parse error: unexpected end of input');
if (t.type === 'not') { pos++; return { type: 'not', arg: pUnary() }; }
if (t.type === '(') { pos++; const e = pImp(); eat(')'); return e; }
if (t.type === 'id') {
if (t.value === 'X') { pos++; return { type: 'X', arg: pUnary() }; }
if (t.value === 'F') { pos++; return { type: 'F', arg: pUnary() }; }
if (t.value === 'G') { pos++; return { type: 'G', arg: pUnary() }; }
if (t.value === 'true' || t.value === 'True') { pos++; return { type: 'true' }; }
if (t.value === 'false' || t.value === 'False') { pos++; return { type: 'false' }; }
pos++;
return { type: 'lit', name: t.value, neg: false };
}
throw new Error(`LTL parse error: unexpected token ${JSON.stringify(t)}`);
}
const f = pImp();
if (pos !== toks.length) throw new Error('LTL parse error: trailing tokens');
return f;
}
/* ------------------------------------------------------------------ */
/* 2. Negation normal form */
/* ------------------------------------------------------------------ */
function nnf(f, neg) {
switch (f.type) {
case 'true': return neg ? { type: 'false' } : { type: 'true' };
case 'false': return neg ? { type: 'true' } : { type: 'false' };
case 'lit': return { type: 'lit', name: f.name, neg: neg ? !f.neg : f.neg };
case 'not': return nnf(f.arg, !neg);
case 'and':
return neg
? { type: 'or', left: nnf(f.left, true), right: nnf(f.right, true) }
: { type: 'and', left: nnf(f.left, false), right: nnf(f.right, false) };
case 'or':
return neg
? { type: 'and', left: nnf(f.left, true), right: nnf(f.right, true) }
: { type: 'or', left: nnf(f.left, false), right: nnf(f.right, false) };
case 'imp':
return neg
? nnf({ type: 'and', left: f.left, right: { type: 'not', arg: f.right } }, false)
: nnf({ type: 'or', left: { type: 'not', arg: f.left }, right: f.right }, false);
case 'X': return { type: 'X', arg: nnf(f.arg, neg) };
case 'F': return nnf({ type: 'until', left: { type: 'true' }, right: f.arg }, neg);
case 'G': return nnf({ type: 'release', left: { type: 'false' }, right: f.arg }, neg);
case 'until':
return neg
? { type: 'release', left: nnf(f.left, true), right: nnf(f.right, true) }
: { type: 'until', left: nnf(f.left, false), right: nnf(f.right, false) };
case 'release':
return neg
? { type: 'until', left: nnf(f.left, true), right: nnf(f.right, true) }
: { type: 'release', left: nnf(f.left, false), right: nnf(f.right, false) };
default: throw new Error(`nnf: unknown node ${f.type}`);
}
}
/* ------------------------------------------------------------------ */
/* 3. Formula helpers */
/* ------------------------------------------------------------------ */
function fkey(f) {
switch (f.type) {
case 'true': return 'T';
case 'false': return 'F';
case 'lit': return (f.neg ? '!' : '') + f.name;
case 'and': return '(' + fkey(f.left) + '&' + fkey(f.right) + ')';
case 'or': return '(' + fkey(f.left) + '|' + fkey(f.right) + ')';
case 'X': return 'X' + fkey(f.arg);
case 'until': return '(' + fkey(f.left) + 'U' + fkey(f.right) + ')';
case 'release': return '(' + fkey(f.left) + 'R' + fkey(f.right) + ')';
default: return '?';
}
}
function dedupe(formulas) {
const seen = new Set();
const out = [];
for (const f of formulas) {
const k = fkey(f);
if (!seen.has(k)) { seen.add(k); out.push(f); }
}
return out;
}
function collectAtoms(f, out) {
out = out || new Set();
switch (f.type) {
case 'lit': out.add(f.name); break;
case 'and': case 'or': case 'until': case 'release':
collectAtoms(f.left, out); collectAtoms(f.right, out); break;
case 'X': collectAtoms(f.arg, out); break;
default: break;
}
return out;
}
function collectUntils(f, out) {
out = out || [];
switch (f.type) {
case 'until':
collectUntils(f.left, out); collectUntils(f.right, out);
if (!out.some(u => fkey(u) === fkey(f))) out.push(f);
break;
case 'release':
collectUntils(f.left, out); collectUntils(f.right, out);
break;
case 'and': case 'or':
collectUntils(f.left, out); collectUntils(f.right, out); break;
case 'X': collectUntils(f.arg, out); break;
default: break;
}
return out;
}
/* ------------------------------------------------------------------ */
/* 4. Tableau expansion (transition relation of the GBA) */
/* ------------------------------------------------------------------ */
function expand(todo) {
todo = dedupe(todo);
if (todo.length === 0) return [{ current: [], next: [] }];
const f = todo[0];
const rest = todo.slice(1);
switch (f.type) {
case 'true': return expand(rest);
case 'false': return [];
case 'and': return expand([f.left, f.right].concat(rest));
case 'or':
return expand([f.left].concat(rest)).concat(expand([f.right].concat(rest)));
case 'lit':
return expand(rest).map(n => ({ current: [f].concat(n.current), next: n.next }));
case 'X':
return expand(rest).map(n => ({ current: [f].concat(n.current), next: [f.arg].concat(n.next) }));
case 'until': {
// f = right OR (left AND X f)
const a = expand([f.right].concat(rest));
const b = expand([f.left, { type: 'X', arg: f }].concat(rest));
return a.concat(b).map(n => ({ current: [f].concat(n.current), next: n.next }));
}
case 'release': {
// f = right AND (left OR X f)
const a = expand([f.right, f.left].concat(rest));
const b = expand([f.right, { type: 'X', arg: f }].concat(rest));
return a.concat(b).map(n => ({ current: [f].concat(n.current), next: n.next }));
}
default: throw new Error(`expand: unknown node ${f.type}`);
}
}
function normalizeNode(node) {
const current = dedupe(node.current);
if (current.some(f => f.type === 'false')) return null;
const lits = new Map();
for (const f of current) {
if (f.type !== 'lit') continue;
const positive = !f.neg;
if (lits.has(f.name) && lits.get(f.name) !== positive) return null;
lits.set(f.name, positive);
}
return { current, next: dedupe(node.next) };
}
function nodeKey(node) {
const c = node.current.map(fkey).sort().join(',');
const n = node.next.map(fkey).sort().join(',');
return `[${c}]#[${n}]`;
}
function nodesFromSeed(seed) {
const seen = new Set();
const out = [];
for (const raw of expand(seed)) {
const n = normalizeNode(raw);
if (!n) continue;
const k = nodeKey(n);
if (seen.has(k)) continue;
seen.add(k);
out.push(n);
}
return out;
}
/* ------------------------------------------------------------------ */
/* 5. Model normalization */
/* ------------------------------------------------------------------ */
function normalizeModel(model) {
if (!model || typeof model !== 'object') throw new Error('model must be an object');
if (typeof model.successors === 'function') {
return {
initialStates: (model.initialStates || model.initial || []).slice(),
successors: (s) => model.successors(s) || [],
labels: (s) => new Set(typeof model.labels === 'function' ? (model.labels(s) || []) : []),
};
}
const transitions = model.transitions || {};
const labelObj = model.labels || {};
const states = new Set([
...Object.keys(transitions),
...Object.keys(labelObj),
...(model.initial || model.initialStates || []),
]);
const norm = {};
for (const s of states) norm[s] = (transitions[s] || []).slice();
return {
initialStates: (model.initial || model.initialStates || []).slice(),
successors: (s) => norm[s] || [],
labels: (s) => new Set(labelObj[s] || []),
};
}
/* ------------------------------------------------------------------ */
/* 6. Generic generalized-Buchi emptiness via nested DFS */
/* ------------------------------------------------------------------ */
/*
* gba = {
* initial: [state, ...],
* successors: (state) => [state, ...], // may be on-the-fly
* acceptingSets: [ (state) => boolean, ... ], // empty => all accepting
* key: (state) => string
* }
* returns { hasAcceptingCycle, prefix, cycle, statesExplored }
* prefix: base states from an initial state to the cycle entry
* cycle: base states, closed (cycle[0] === cycle[last])
*/
function findAcceptingCycle(gba) {
const keyOf = gba.key || ((s) => String(s));
const sets = (gba.acceptingSets && gba.acceptingSets.length) ? gba.acceptingSets : [() => true];
const k = sets.length;
const baseSeen = new Set();
const succCache = new Map();
function succ(state, c) {
const sk = keyOf(state);
baseSeen.add(sk);
// Degeneralize: advance the counter only in states accepting the current set.
const acc = sets[c](state);
const c2 = (acc ? (c + 1) % k : c) % k;
let list = succCache.get(sk);
if (!list) {
list = gba.successors(state) || [];
succCache.set(sk, list);
}
return { c2, list };
}
const visited = new Set(); // outer DFS
const onStack = new Set();
const degInfo = new Map(); // degKey -> { state, c }
const parentOuter = new Map();
const degKey = (state, c) => keyOf(state) + '\u0001' + c;
// ---- iterative nested DFS ----
function outerIter(rootKey) {
const stack = [{ v: rootKey, i: 0, entered: false, s: null, c: 0 }];
while (stack.length) {
const fr = stack[stack.length - 1];
if (!fr.entered) {
fr.entered = true;
const info = degInfo.get(fr.v);
fr.s = info.state; fr.c = info.c;
visited.add(fr.v);
onStack.add(fr.v);
const { list } = succ(fr.s, fr.c);
fr.list = list; fr.i = 0;
}
if (fr.i < fr.list.length) {
const w = fr.list[fr.i++];
// current counter value after taking this edge from fr
const acc = sets[fr.c](fr.s);
const wc = (acc ? (fr.c + 1) % k : fr.c) % k;
const wKey = degKey(w, wc);
if (!degInfo.has(wKey)) degInfo.set(wKey, { state: w, c: wc });
if (!visited.has(wKey)) {
parentOuter.set(wKey, fr.v);
stack.push({ v: wKey, i: 0, entered: false, s: w, c: wc });
}
continue;
}
// post-order: an accepting state seeds the inner DFS
if (sets[fr.c](fr.s)) {
const cyc = innerIter(fr.v, fr.s, fr.c);
if (cyc) return { seedKey: fr.v, cycleKeys: cyc };
}
onStack.delete(fr.v);
stack.pop();
}
return null;
}
// inner DFS: path from seed back to seed through outer-stack states
function innerIter(seedKey, seedState, seedC) {
const seen = new Set([seedKey]);
const pathKeys = [seedKey];
const stack = [{ s: seedState, c: seedC, list: null, i: 0 }];
while (stack.length) {
const fr = stack[stack.length - 1];
if (fr.list === null) {
fr.list = succ(fr.s, fr.c).list;
fr.i = 0;
}
if (fr.i < fr.list.length) {
const w = fr.list[fr.i++];
const acc = sets[fr.c](fr.s);
const wc = (acc ? (fr.c + 1) % k : fr.c) % k;
const wKey = degKey(w, wc);
if (!degInfo.has(wKey)) degInfo.set(wKey, { state: w, c: wc });
if (wKey === seedKey) return pathKeys.concat([seedKey]);
if (onStack.has(wKey) && !seen.has(wKey)) {
seen.add(wKey);
pathKeys.push(wKey);
stack.push({ s: w, c: wc, list: null, i: 0 });
}
continue;
}
stack.pop();
pathKeys.pop();
}
return null;
}
let found = null;
for (const s0 of gba.initial) {
baseSeen.add(keyOf(s0));
const rootKey = degKey(s0, 0);
if (!degInfo.has(rootKey)) degInfo.set(rootKey, { state: s0, c: 0 });
if (visited.has(rootKey)) continue;
found = outerIter(rootKey);
if (found) break;
}
const statesExplored = baseSeen.size;
if (!found) return { hasAcceptingCycle: false, prefix: [], cycle: [], statesExplored };
// prefix: initial -> seed through outer DFS tree
const prefixKeys = [];
for (let cur = found.seedKey; cur !== undefined; cur = parentOuter.get(cur)) prefixKeys.push(cur);
prefixKeys.reverse();
const prefix = prefixKeys.map(x => degInfo.get(x).state);
const cycle = found.cycleKeys.map(x => degInfo.get(x).state);
return { hasAcceptingCycle: true, prefix, cycle, statesExplored };
}
/* ------------------------------------------------------------------ */
/* 7. LTL model checking */
/* ------------------------------------------------------------------ */
function checkLTL(model, formula, options) {
options = options || {};
const m = normalizeModel(model);
if (m.initialStates.length === 0) throw new Error('model has no initial states');
const target = nnf({ type: 'not', arg: formula }, false); // automaton for !phi
const atoms = [...collectAtoms(target)];
const untils = collectUntils(target);
const succMemo = new Map();
const productStates = new Map();
function seedFor(mState, node) {
const labels = m.labels(mState);
const seed = node ? node.next.slice() : [target];
for (const a of atoms) seed.push({ type: 'lit', name: a, neg: !labels.has(a) });
return nodesFromSeed(seed);
}
function getProduct(mState, node) {
const key = mState + '\u0000' + nodeKey(node);
let ps = productStates.get(key);
if (!ps) {
ps = { key, model: mState, node };
productStates.set(key, ps);
}
return ps;
}
function productSuccessors(ps) {
let s = succMemo.get(ps.key);
if (s !== undefined) return s;
s = [];
const seen = new Set();
for (const m2 of m.successors(ps.model)) {
for (const node2 of seedFor(m2, ps.node)) {
const p2 = getProduct(m2, node2);
if (!seen.has(p2.key)) { seen.add(p2.key); s.push(p2); }
}
}
succMemo.set(ps.key, s);
return s;
}
function satisfies(node, u) {
const uk = fkey(u);
const rk = fkey(u.right);
let hasU = false, hasR = false;
for (const f of node.current) {
const kk = fkey(f);
if (kk === uk) hasU = true;
else if (kk === rk) hasR = true;
}
return !hasU || hasR;
}
const init = [];
const initSeen = new Set();
for (const s0 of m.initialStates) {
for (const node0 of seedFor(s0, null)) {
const ps = getProduct(s0, node0);
if (!initSeen.has(ps.key)) { initSeen.add(ps.key); init.push(ps); }
}
}
const gba = {
initial: init,
successors: productSuccessors,
acceptingSets: untils.map(u => (ps) => satisfies(ps.node, u)),
key: (ps) => ps.key,
};
const res = findAcceptingCycle(gba);
if (!res.hasAcceptingCycle) {
return {
result: 'holds', status: 'holds', holds: true,
statesExplored: res.statesExplored,
prefix: [], cycle: [], lasso: [], counterexample: [],
};
}
const prefix = res.prefix.map(ps => ps.model);
const cycle = res.cycle.map(ps => ps.model);
const lasso = prefix.concat(cycle.slice(1));
return {
result: 'violated', status: 'violated', holds: false,
statesExplored: res.statesExplored,
prefix, cycle, lasso, counterexample: lasso,
};
}
/* ------------------------------------------------------------------ */
/* 8. Exports */
/* ------------------------------------------------------------------ */
module.exports = {
parse,
nnf,
fkey,
expand,
collectAtoms,
collectUntils,
normalizeModel,
findAcceptingCycle,
checkLTL,
};
const { checkLTL, parse, findAcceptingCycle } = require('./ltl');
checkLTL(model, formula);
// -> { result: 'holds'|'violated', status, holds,
// statesExplored, prefix, cycle, lasso, counterexample }
findAcceptingCycle({ initial, successors, acceptingSets, key });
// generic (generalized) Büchi emptiness; -> { hasAcceptingCycle, prefix, cycle, statesExplored }
Models may be explicit
{ initial: ['s0'],
transitions: { s0: ['s0','s1'], s1: ['s1'] },
labels: { s0: ['p'], s1: ['q'] } }
or functional
{ initialStates: ['s0'],
successors: s => [...],
labels: s => [...] }
Formula syntax: ! ~ & && | || ->, X, F, G, U, R, true, false, ( ) and atoms. Precedence (loosest to tightest): ->, U/R, |, &, unary ! X F G.
An independent checker was used to validate the NDFS: it builds the full reachable product, degeneralizes explicitly, and decides emptiness with Tarjan SCC (accepting cycle ⇔ reachable non-trivial SCC containing an accepting state). The fuzzer also has an independent LTL-on-lasso evaluator that confirms the emitted counterexample actually satisfies !φ.
$ node test1.js
G p on always-p {"result":"holds","statesExplored":1}
G p on toggle {"result":"violated","prefix":["s0","s1","s0","s1"],"cycle":["s1","s0","s1"]}
F q on always-p {"result":"violated","prefix":["s0"],"cycle":["s0","s0"]}
G F p on toggle {"result":"holds","statesExplored":3}
p U q always-p {"result":"violated","prefix":["s0"],"cycle":["s0","s0"]}
F G p on toggle {"result":"violated","prefix":["s0","s1"],"cycle":["s1","s0","s1"]}
F G p on eventually-p{"result":"holds","statesExplored":3}
$ node gba-test.js
trap (disjoint sets) {"hasAcceptingCycle":false} <- must NOT accept
genuine A->B->A {"hasAcceptingCycle":true, "prefix":["A","B"], "cycle":["B","A","B"]}
shared SCC {"hasAcceptingCycle":true}
no accepting state {"hasAcceptingCycle":false}
self loop {"hasAcceptingCycle":true, "cycle":["A","A"]}
no sets (all accepting) {"hasAcceptingCycle":true}
DAG holds {"hasAcceptingCycle":false}
unreachable accepting loop{"hasAcceptingCycle":false}
A stronger trap with all states reachable still returns false:
$ node extra.js
real trap: {"hasAcceptingCycle":false,"prefix":[],"cycle":[],"statesExplored":3}
Random Kripke structures (1–4 states, random transitions/labels over p,q) and random depth-4 LTL formulas (nested U, F, G, boolean structure) were checked:
$ node fuzz.js
{ N: 4000, mismatches: 0, badTrace: 0, badLasso: 0 }
$ node fuzz2run.js # denser graph, 2-4 states, depth-4 formulas
{ N: 3000, mismatches: 0, badTrace: 0, badLasso: 0 }
mismatches – NDFS verdict ≠ Tarjan verdict (0).badTrace – returned prefix/cycle is not a real path/closed cycle in the model (0).badLasso – the emitted lasso does not satisfy !φ according to the independent evaluator (0).$ node extra.js
scale: violated explored 200000 ms 1351 prefix 200000 cycle 2
An iterative DFS over a 200 000-state product terminates without stack overflow.
# files: ltl.js, brute.js, test1.js, fuzz.js, fuzz2run.js, gba-test.js, extra.js
node test1.js
node gba-test.js
node fuzz.js
node fuzz2run.js
node extra.js
expand computes the standard Gerth–Peled–Vardi–Wolper tableau; each node is a maximally consistent set of closure formulas, and next contains the temporal obligations for successors. Contradictory literal sets are dropped.c ∈ {0..k-1}, the only accepting states are those in the current acceptance set F_c; visiting one necessarily advances c. Hence infinitely many accepting visits ⇔ every F_c is visited infinitely often, which is exactly GBA acceptance.v is completed, the inner DFS searches, restricted to states still on the outer stack, for a path back to v. If an accepting SCC exists, its DFS-root is completed while the whole SCC is on the stack, so a closed accepting cycle is found; conversely the inner DFS only returns a closed path through accepting states, so it cannot fabricate one.prefix is the outer-tree path initial → seed; cycle is the inner path seed → seed. Concatenating prefix with cycle[1..] yields a well-formed ultimately-periodic counterexample that was independently confirmed to satisfy !φ.Files on disk: ~/ltl-checker/{ltl.js,brute.js,test1.js,fuzz.js,fuzz2run.js,gba-test.js,extra.js,SOLUTION.md}. The code embedded above was diffed byte-for-byte against the verified ltl.js.
# Evidence - Problem class: js-ltl-on-the-fly-buchi-nested-dfs-emptiness - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-10-03T16:57:24.937Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Implement an on-the-fly LTL model checker: translate an LTL formula to a generalized Buchi automaton via a tableau construction, then run nested-DFS emptiness checking to produce a counterexample lasso when the property is violated. It must handle multiple acceptance conditions (fairness), detect genuinely accepting cycles rather than partial SCCs, and emit the exact prefix/cycle split of the lasso. Report 'holds' with the explored state count when no accepting cycle exists.", "environment": "node20", "language": "js", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "js-ltl-on-the-fly-buchi-nested-dfs-emptiness", "provider": "openrouter", "solved_at": "2026-10-03T16:57:24.942Z", "version": "20"}