I'm reviewing some notes about tree automata and I'm trying to conclude a proof that the professor left incomplete. The statement is:

Let $A = \{a,b\}$ and $T = \{t \in T_A^{\omega} \mid \text{every path in $t$ contains a finite number of $a$}\}$. Prove that $T$ isn't Buchi recognizable.

Now we can define the following subsets of trees $t_n \subseteq T$ where $t \in t_n$ has one $a$ at positions: $\epsilon, 1^{m_1}0, 1^{m_1}01^{m_2}0, \ldots, 1^{m_1}01^{m_2}0\ldots1^{m_n}0$ with $m_i > 0$.

Now assume that $\mathcal{A} = (Q, A, \Delta, q_0, F)$ is the Buchi automaton that recognizes $T$ with $|Q| = n+1$ and $q_0$ appears only at the root of its computations. Let $t \in t_n$ and $r$ be a successful run of $\mathcal{A}$ on $t$.

Claim: $\color{red}{\text{There exists $u \leq v < w$ such that $r(u) = r(w) = s \in F$ and $t(v) = a$.}}$

Obviously if we show that the claim is true we can prove the initial statement: take the subtree $t_v$ and obtain a $t' \in t_{n+1}$ by replacing the subtree $t_w$ with $t_v$. We have that there exist a run $r'$ which is identical to $r$ up to the position for $w$ and will follow the same sequence of states at $w$ as it did at $v$, and hence is accepting. Repeat the process and you obtain a branch with infinite $a$s that is accepted by $\mathcal{A}$. (This is just the rough idea, it requires a bit of formalism, but it's not the point of the question.)

My question is: how do I prove the claim?

I can show that there exist a $t' \in t_{2n}$ with that property (which is actually good enough for the rest of the proof), but not that given a fixed $t_n$ the statement holds for any successful run.

My idea is simply: given that $r$ is accepting there must exist a $s \in F$ repeated infinite times in a path passing through $1^{m_1}01^{m_2}0\ldots1^{m_n}0$. Then take a tree $t'' \in t_{n+1}$ that is identical to $t_n$ up to the position $x$ where $r(x) = s$ on that path, and add an $a$ below such position. Now this tree is still accepted by the automaton and there exist an accepting run $r'$ identical to $r$ up to the position $x$, but then $r'$ cannot reuse $s$ for accepting that same path (otherwise we have found the three states of the claim) and so it must use a different state $s'$. Repeat for all final states and you have that $t_{2n}$ must have a run with that property.

Is there any way to apply this kind of reasoning to $t_{n-1}$, $t_{n-2}$ etc to obtain the result for $t_n$? It looks like at most I may be able to prove that there exist a $t'' \in t_n$ with a run with that property, while the claim is stronger. Or am I going in the wrong direction?


1 Answer 1


The idea is to play with the $m_i$'s, as follows.

Consider a tree $t_1$, which has $a$ in $\epsilon$, and nowhere else. Look at the path $1^\omega$ — an accepting run on it has infinitely many accepting states. Wait until such an accepting state was reached, and only then put $a$ at $1^{m_1}0$, where $m_1$ is large enough.

Now look at the path $1^{m_1}01^\omega$, again, it has an accepting state eventually, denote the length up to it by $m_2$, put an $a$ at $1^{m_1}01^{m_2}0$ and look at $1^{m_1}01^{m_2}01^\omega$. By now you have almost what you wanted - two accepting states with an $a$ between them (informally speaking). But you are not yet guaranteed that both accepting states are equal. To enforce the latter, we repeat the process for $n$ times, thus exhausting the number of accepting states, and by the pigeonhole principle, two accepting states must be equal.

  • $\begingroup$ You don't even need to consider the number of states - just note that this approach gives you (for any given automaton $A$) an infinite sequence $m_1,m_2,\ldots$ such that for each $k$, $A$ reaches an accepting state $k$ times on $1^{m_1}01^{m_2}0\ldots 1^{m_k}0$, and therefore the limit $1^{m_1}01^{m_2}0\ldots$ will be accepted despite having infinitely many $0$s. $\endgroup$ Feb 28, 2016 at 10:47
  • $\begingroup$ Right, but the OP specifically wanted to bound the number of $m_i$'s by $n+1$, for which you do need the number of states. $\endgroup$
    – Shaull
    Feb 28, 2016 at 11:00
  • $\begingroup$ This is more or less what I was thinking about, however it proves something a little weaker than the claim. With this you prove that $\exists t \in t_n$ and $\exists r$ succesful run of $\mathcal{A}$ on $t$ such that <claim>. While in the proof as stated by the professor you have $\forall t \in t_n$ and $\forall r$ succesful run of $\mathcal{A}$ over $t$ ti holds <claim>. The problem is that if you have $t$ fixed you cannot really play with those $m_i$s as you wish. Now I wonder whether the claim as stated by the professor is actually true or whether this is the best we can achieve. $\endgroup$
    – Bakuriu
    Feb 28, 2016 at 14:19
  • 1
    $\begingroup$ For every successful run the claim is clearly false, since the automaton can have a component which guesses a point from which $a$ is never encountered again. Clearly every $t\in t_n$ will have at least one such accepting run... $\endgroup$
    – Shaull
    Feb 28, 2016 at 14:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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