I was learning about Büchi Automata and couldn't understand a part where they were describing "Non-empty $\omega$-regular languages contain periodic strings"

Let $A$ be a Büchi automaton and $s ∈ L^\omega(A)$. There is an accepting run $r$ of $A$ on $s$ such that $q ∈ \text{Inf}(r)$, for some $q$. Then, there exist finite strings $s_0$ and $s_1$ such that $s_0s_1$ is a prefix of $s$, and such that $A$, after processing $s_0$ is in $q$, and after processing $s_0s_1$ is also in $q$. Then, the periodic string $s' = s_0s_1s_1s_1 \dotsm$ is accepted by $A$ since there is a run on $s'$ that contains $q$ infinitely many times.

I bolded the part I'm having trouble understanding. Why is it that we can say after running a prefix like $s_0$ we are in an accept state $q$? It seems to me a prefix could easily end in some not accepting state (i.e not in $\text{Inf}(r)$).


Actually, it doesn't say that $q$ is an accepting state, though it should do! $\mathrm{Inf}(r)$ is the set of states visited infinitely often during the run $r$. The acceptance condition of Büchi automata is that $\mathrm{Inf}(r)$ contains an accepting state.

The correct proof is as follows, with explanation added. Note also that, while your title says that the automaton is deterministic, the proof applies to nondeterministic automata, too, since it talks about the existence of a run with a particular property, rather than saying that the unique run has that property.

Let $A$ be a Büchi automaton and let $s\in L^\omega(A)$. Since $A$ accepts $s$, there must be a run $r$ of $a$ on $s$ that has an accepting state $q\in \mathrm{Inf(r)}$ because a Büchi automaton accepts if, and only if, some accepting state is visited infintely often. Let $s_0$ be any prefix of $s$ such that $A$ is in state $q$ after reading $s_0$. Since $r$ visits $q$ infinitely often, it must return to $q$ when processing $s$, say after processing the prefix $s_0s_1$. In particular, if the automaton is in state $q$ and reads string $s_1$, there is a run in which it returns to $q$. Therefore, the automaton has a run that visits $q$ infinitely often when processing the string $s_0\,{s_1}^\omega = s_0s_1s_1s_1\dots$.

  • $\begingroup$ You just reproduced my answer. $\endgroup$ – J.-E. Pin Mar 13 '15 at 8:07
  • 1
    $\begingroup$ No I didn't. Not even close. My answer is literally ten times the length of yours. I point out that the proof in the question is incorrect; you don't. I supply a correct, more detailed proof; you don't. I point out that the proof is for nondeterministic automata as well; you don't. $\endgroup$ – David Richerby Mar 13 '15 at 8:14

It may be worth noting that referring to any particular automaton is not really needed to prove the statement in the title. The standard definition of an $\omega$-regular language is as a finite union

$L=A_1B_1^\omega\cup\dots\cup A_nB_n^\omega$,

where all $A_i$ and $B_i$ are regular. If $L$ is nonempty, then there is at least one $i$ with $A_i,B_i$ nonempty; picking any $u\in A_i,v\in B_i$, it is clear that $uv^\omega\in L$.


By definition, a run $r$ is accepting if there is a final state such that $q \in \text{Inf}(r)$.

EDIT (to please david-richerby).

The standard definition of an accepting run says that a run $r$ is accepting if there is a final state such that $q \in \text{Inf}(r)$.

  • $\begingroup$ But that doesn't mean that $q$ is accepting. Actually, the proof in the question is incorrect, precisely because it doesn't say that $q$ is accepting. $\endgroup$ – David Richerby Mar 13 '15 at 7:55
  • $\begingroup$ This is exactly what I am saying. $\endgroup$ – J.-E. Pin Mar 13 '15 at 8:03
  • $\begingroup$ It doesn't seem to be what you're saying at all. You say nothing about the state $q$ in the question and you don't say that the proof in the question is incorrect. So, in fact, you say neither of the things that I said in my comment. $\endgroup$ – David Richerby Mar 13 '15 at 8:12
  • $\begingroup$ I just say "by definition", a rather precise mathematical term. $\endgroup$ – J.-E. Pin Mar 13 '15 at 9:15
  • 2
    $\begingroup$ Does this answer really offer anything to the OP? $\endgroup$ – Louis Mar 13 '15 at 9:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.