Notebook 24: Saturation → the Complement Automaton
Building the Complement
All the pieces now combine. Because \(\approx_{\mathcal A}\) is a finite-index congruence that saturates \(L(\mathcal A)\), and the Ramsey decomposition writes every \(\omega\)-word as some class product \(U\,V^{\omega}\) (with \(V\) idempotent), each such product is entirely inside \(L(\mathcal A)\) or entirely disjoint from it. The complement is then just the union of the disjoint ones: \[ \overline{L(\mathcal A)} \;=\; \bigcup\bigl\{\,U\,V^{\omega} \;:\; U\,V^{\omega}\cap L(\mathcal A)=\emptyset \,\bigr\}, \] a finite union. The classes can be enumerated, their products formed, and each intersection with \(L(\mathcal A)\) tested for emptiness — an effective construction.
We test products on the chapter’s automaton \(\mathcal A\) (accepts “\(ab\) infinitely often, separated by \(c\)’s”). Pick a prefix \(U\) and an idempotent block \(V\); the widget runs the representative \(u\cdot v^{\omega}\) and reports whether that whole product sits in \(L\) or in \(\overline{L}\).
A note on the running example. The chapter’s Example on saturation states \(\alpha=a(abc)^{\omega}\) is accepted with \(U=[a]\). On the deterministic \(\mathcal A\) that run actually dies — after \(a\) the automaton is in \(s_1\), which has no outgoing \(a\). The correct accepted witness is \(ab(abc)^{\omega}\), i.e. \(U=[ab]\) (the prefix must reach \(s_2\), where the \(abc\)-block loops). The widget below uses that verified witness.
Widget: classify class products
Run of u·vω on 𝒜 (prefix + 3 blocks)
Enumerated class products → the complement
This is the whole complementation theorem in miniature: no state-flipping trick (that failed back in Notebook 16), but a finite algebra of class products, each decided in or out by an emptiness test, with the “out” ones assembled into a Büchi automaton for \(\overline{L(\mathcal A)}\). Decidable inclusion — and hence \(\omega\)-regular model checking — follows.