Notebook 18: Büchi Closure — Union & Intersection

Union of Büchi automata is trivial; intersection needs a two-phase product that cycles through F₁ then F₂. Build the product for ‘infinitely many a’ ∩ ‘infinitely many b’ and watch the phase flag.

Closure Under Union and Intersection

\(\omega\)-regular languages are closed under both operations, but the two constructions are not symmetric.

  • Union is trivial: put the two automata side by side (a disjoint sum). A word is accepted iff some component accepts it. No new idea is needed.
  • Intersection cannot just “accept when both accept”: each automaton has its own accepting set, and a single Büchi condition must witness that \(F_1\) and \(F_2\) are each hit infinitely often. The fix is a two-phase product: track a phase flag that says which accepting set we are currently waiting for, flip \(1\to2\) when we see \(F_1\) and \(2\to1\) when we see \(F_2\), and make the \(2\to1\) flip the accepting event. Completing the cycle infinitely often forces both sets to recur.

The running example over \(\Sigma=\{a,b\}\): \[ L_a = \text{"infinitely many } a\text{"}, \qquad L_b = \text{"infinitely many } b\text{"}, \qquad L_a\cap L_b = \text{"both infinitely often"}. \]

Each component is a one-state Büchi automaton that “checkpoints” on its letter. In the product, \(\alpha=u\cdot v^{\omega}\) is accepted iff the period \(v\) contains both an \(a\) and a \(b\).

Widget: the two-phase product

Product run — phase flag & accepting checkpoints

Try v = a (only a’s forever): the intersection rejects — the phase reaches \(2\) waiting for a \(b\) that never returns, so the checkpoint fires at most once. This asymmetry is exactly why intersection needs the phase flag while union does not. The same product underlies the reduction of model checking to emptiness — see Notebook 14.