Notebook 19: Ultimately-Periodic Witnesses

Every non-empty ω-regular language contains an ultimately-periodic word u·vω, read off a reachable accepting cycle (a lasso). Pick a loop and extract the witness, with |u|,|v| bounded by the number of states.

The Ultimately-Periodic Fingerprint

A Büchi automaton is non-empty iff it has a reachable accepting cycle — a lasso: a stem from the initial state to an accepting state \(f\), then a cycle from \(f\) back to \(f\). Reading the stem once and the cycle forever gives an accepted word of the shape \[ \alpha = u\cdot v^{\omega},\qquad u = \text{stem},\ v = \text{cycle}, \] an ultimately-periodic word. Because a shortest stem and a shortest cycle each stay within the automaton, one can always find such a witness with \[ |u| < |Q| \quad\text{and}\quad |v| \le |Q|. \]

This is the fingerprint behind emptiness (Notebook 14): non-emptiness is not just a yes/no answer — it comes with a concrete, finitely-described infinite witness.

The automaton below is the editor that saves infinitely often (initial open, then it accepts iff save recurs forever). Pick a loop through the accepting checkpoint \(f\) and read off the witness.

Widget: read a witness off a lasso

Automaton: "infinitely many saves"

open edit,idle save edit,idle save q_b q f

Choose a loop through f

Witness

stem  u =
loop  v =
α = ·()ω

Run of α (stem + 3 loops)

The loop (save) gives the shortest witness open·(save)ω = open save save save …; the loop (edit save) gives open·(edit save)ω. Both are accepted, both are ultimately periodic, and both fit inside the state bound. Different lassos, same language — the witness is never unique, but one always exists whenever the language is non-empty.