Notebook 15: Parity of Blocks Between a’s
Parity Between Occurrences
This notebook makes concrete the automaton of the chapter’s parity example (adapted from Wolfgang Thomas). Over \(\Sigma=\{a,b,c\}\) we recognise:
Between any two consecutive occurrences of \(a\), there is an even number of \(b\) and \(c\) symbols combined.
For instance \(a\,b\,c\,a\) is accepted (two symbols between the \(a\)’s), while \(a\,b\,b\,b\,a\) is rejected (three). Words with no \(a\), or only one \(a\), satisfy the condition vacuously.
The point of the example is that each state carries a precise invariant:
- \(q_0\) — before the first \(a\) (or no \(a\) at all). Accepting.
- \(q_1\) — an even number of \(b/c\) since the last \(a\) (zero counts as even). Accepting.
- \(q_2\) — an odd number of \(b/c\) since the last \(a\). Non-accepting.
Reading \(a\) from \(q_2\) would close an odd gap and violate the property: that transition is simply undefined, so the run dies. Notice \(q_2\) need not be accepting — see the widget’s note below.
Widget: Run \(\alpha = u\cdot v^{\omega}\)
Automaton (deterministic, partial)
Why q₂ is not accepting: if no further $a$ ever comes, the run bounces $q_1\leftrightarrow q_2$ forever and visits $q_1\in F$ infinitely often anyway — $q_1$ alone witnesses acceptance. If an $a$ does come while in $q_2$, the transition is undefined and the run dies. Either way $q_2$ carries no acceptance information.
Run trace ρ (stem + 3 periods)
Related: Notebook 12 — Büchi Automaton Runner runs the simpler “infinitely many saves” automaton; here the state set encodes a genuine counting invariant (parity), which is why the automaton stays deterministic with only three states.