Lasso Trace Exists

Lemma 1. For any non-empty Buchi automaton \(A = (Q, \delta, q_0, F)\), there is \(w \in L (A)\) s.t. \(w = u v^{\omega}\) where \(u, v \in \Sigma^{\ast}\).


Since A is non-empty, we take an arbitrary infinite word \(w \in L (A)\). Suppose \(w = a_1 a_2 \cdots\).

From the acceptance condition of Buchi automaton, we know there must be at least one final state \(q_f \in F\) that occurs in \(w\) infinitely often. Assume at position i, after reading prefix \(a_1 \cdots a_i\), \(q_f\) is reached for the first time, and at position j it is reached for the second time.

Then consider the infinite word \(w' = a_1 \cdots a_i (a_{i + 1} \cdots a_j)^{\omega}\). Obviously \(w' \in L (A)\) and it satisfies the condition.