Notebook 14: Büchi Emptiness — The Lasso Test
Büchi Emptiness — The Lasso Test
For a Büchi automaton \(\mathcal{A}\), the language \(L(\mathcal{A})\) is non-empty if and only if there exists an accepting state \(q_f \in F\) that is: 1. Reachable from an initial state. 2. On a cycle (reachable from itself).
If such a state \(q_f\) exists, the path from the initial state to \(q_f\) is called the stem (\(u\)), and the cycle from \(q_f\) back to \(q_f\) is called the period (\(v\)). The automaton then accepts the ultimately periodic \(\omega\)-word \(\alpha = u \cdot v^\omega\). This structure is called a lasso, and finding one is the core algorithm used in model checking to find counterexamples.
The first preset applies this directly to the running editor monitor: one reachable cycle containing the accepting save-checkpoint proves that at least one infinite execution saves forever.
Widget: Find a Lasso
Select a Büchi automaton and click Step \(\rightarrow\) to search for a reachable accepting state on a cycle.