go-mu-calculus-alternating-fixpoint-model-checker
Done. The verified solution is at ~/mucheck/SOLUTION.md (self-contained, 1180 lines, full source embedded). I also proved it's self-contained by extracting only the markdown's code blocks into /tmp/solution_extract, where gofmt, go vet, and go test all pass.
A fixpoint is a function of the enclosing environment, not a constant. The naive checker memoises each binder's result by formula identity, so the inner mu Y is solved once against X = S (because the outer nu X starts at the top). That freezes mu at a gfp-flavoured value and skips re-evaluation as X shrinks. In local/unfolding terms: without a progress/signature measure, mu cannot be distinguished from nu, so the infinite branch is accepted.
Global monotone iteration, re-evaluated from scratch each outer step, with unique binder ids:
case *Mu: // least fixpoint: start at bottom
cur := Set{}
for {
stats.Iter[n.ID]++ // per-binder audit counter
env2 := cloneEnv(env) // fresh env => correct scoping
env2[n.X] = cur
next := m.Eval(n.F, env2, stats) // inner fixpoints recomputed
if next.Equal(cur) { return cur }
cur = next
}
case *Nu: // greatest fixpoint: start at top
cur := m.all()
for { /* symmetric */ }
naive.go keeps the buggy memoised evaluator as a negative control; parser.go handles labelled modalities, free variables, and shadowing; CollectBinders + Stats.Iter produce the per-variable iteration audit.
| Check | Result |
|---|---|
gofmt -l . / go vet ./... |
clean |
go test ./... |
ok mucheck |
| lfp vs gfp, disjoint SCCs + self-loops | mu = {a,b} vs nu = {a,b,c,d} |
| differ by exactly one state | lfp {a,b}, gfp {a,b,c} → diff {c} |
alternation nu X. mu Y. ((p & <>Y) \| (q & <>X)) |
correct {}, naive {a} (off by one) |
audit: inner mu Y iterations |
4 (re-solved per outer step), outer nu X = 3 |
| shadowing vs alpha-renaming | identical sets |
free-variable env {F ↦ {c}} / {F ↦ {}} |
{a,b,c} / {} |
The audit output is the key diagnostic: a correctly alternating checker shows the inner mu evaluated multiple times (once per outer nu value), which is exactly what the memoised version collapses to one.
# Evidence - Problem class: go-mu-calculus-alternating-fixpoint-model-checker - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-18T10:24:17.838Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Implement a modal mu-calculus model checker over a finite labeled transition system: parse formulas with nested, alternating least and greatest fixpoints (nu X. mu Y. ...) including free-variable environments and bound-variable shadowing, and decide the exact set of states satisfying each subformula. The naive recursive expansion returns the greatest-fixpoint solution for an inner least-fixpoint subformula whenever nesting alternates, so correctness needs a real progress/signature measure (or a correct gfp/lfp iteration order with per-variable tracking) and must be demonstrated on graphs that separate lfp from gfp: disjoint SCCs, self-loops without exits, and formulas where the two differ by exactly one state. Report the satisfying set and, as a separate output, the number of fixpoint iterations per variable so the alternation ordering can be audited.", "environment": "go1.26", "language": "go", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "go-mu-calculus-alternating-fixpoint-model-checker", "provider": "openrouter", "solved_at": "2026-09-18T10:24:17.838Z", "version": "1.26"}Done. The verified solution is at ~/mucheck/SOLUTION.md (self-contained, 1180 lines, full source embedded). I also proved it's self-contained by extracting only the markdown's code blocks into /tmp/solution_extract, where gofmt, go vet, and go test all pass.
A fixpoint is a function of the enclosing environment, not a constant. The naive checker memoises each binder's result by formula identity, so the inner mu Y is solved once against X = S (because the outer nu X starts at the top). That freezes mu at a gfp-flavoured value and skips re-evaluation as X shrinks. In local/unfolding terms: without a progress/signature measure, mu cannot be distinguished from nu, so the infinite branch is accepted.
Global monotone iteration, re-evaluated from scratch each outer step, with unique binder ids:
case *Mu: // least fixpoint: start at bottom
cur := Set{}
for {
stats.Iter[n.ID]++ // per-binder audit counter
env2 := cloneEnv(env) // fresh env => correct scoping
env2[n.X] = cur
next := m.Eval(n.F, env2, stats) // inner fixpoints recomputed
if next.Equal(cur) { return cur }
cur = next
}
case *Nu: // greatest fixpoint: start at top
cur := m.all()
for { /* symmetric */ }
naive.go keeps the buggy memoised evaluator as a negative control; parser.go handles labelled modalities, free variables, and shadowing; CollectBinders + Stats.Iter produce the per-variable iteration audit.
| Check | Result |
|---|---|
gofmt -l . / go vet ./... |
clean |
go test ./... |
ok mucheck |
| lfp vs gfp, disjoint SCCs + self-loops | mu = {a,b} vs nu = {a,b,c,d} |
| differ by exactly one state | lfp {a,b}, gfp {a,b,c} → diff {c} |
alternation nu X. mu Y. ((p & <>Y) \| (q & <>X)) |
correct {}, naive {a} (off by one) |
audit: inner mu Y iterations |
4 (re-solved per outer step), outer nu X = 3 |
| shadowing vs alpha-renaming | identical sets |
free-variable env {F ↦ {c}} / {F ↦ {}} |
{a,b,c} / {} |
The audit output is the key diagnostic: a correctly alternating checker shows the inner mu evaluated multiple times (once per outer nu value), which is exactly what the memoised version collapses to one.
# Evidence - Problem class: go-mu-calculus-alternating-fixpoint-model-checker - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-18T10:24:17.838Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Implement a modal mu-calculus model checker over a finite labeled transition system: parse formulas with nested, alternating least and greatest fixpoints (nu X. mu Y. ...) including free-variable environments and bound-variable shadowing, and decide the exact set of states satisfying each subformula. The naive recursive expansion returns the greatest-fixpoint solution for an inner least-fixpoint subformula whenever nesting alternates, so correctness needs a real progress/signature measure (or a correct gfp/lfp iteration order with per-variable tracking) and must be demonstrated on graphs that separate lfp from gfp: disjoint SCCs, self-loops without exits, and formulas where the two differ by exactly one state. Report the satisfying set and, as a separate output, the number of fixpoint iterations per variable so the alternation ordering can be audited.", "environment": "go1.26", "language": "go", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "go-mu-calculus-alternating-fixpoint-model-checker", "provider": "openrouter", "solved_at": "2026-09-18T10:24:17.838Z", "version": "1.26"}