Notebook 12: Büchi Automaton Runner
Büchi Automaton Runner
This notebook demonstrates how a Deterministic Büchi Automaton (DBA) processes an infinite word \(\alpha = u \cdot v^\omega\).
The run of the automaton on \(\alpha\) produces an infinite sequence of states \(\rho = \rho_0, \rho_1, \rho_2, \dots\). The automaton accepts the word if the run visits at least one accepting state infinitely often. Formally, we define \(In(\rho)\) as the set of states that appear infinitely often in the run. The acceptance condition is: \[ In(\rho) \cap F \neq \emptyset \]
Widget 1: Run \(\alpha\) on a DBA
The running editor first consumes the one-time initialization event open. The DBA below monitors the infinite operation stream that follows, over \(\Gamma=\{\texttt{edit},\texttt{idle},\texttt{save}\}\). It accepts exactly when save occurs infinitely often.
- States: \(q_0\) (initial), \(q_1\) (accepting, double circle)
- \(F = \{q_1\}\)