Hope someone can point me to the right direction to solve this problem.

Premise. I call quasi-deterministic Büchi automaton (qDBA) a Büchi automaton $B = \langle S, \Sigma, S_0, \delta, F \rangle$, where $S$ is the set of states, $\Sigma$ the alphabet of transition labels, $S_0 \subseteq S$ the set of initial states, $\delta: S \times \Sigma \rightarrow S$ a partial transition function, and $F \subseteq S$ the set of accepting states. That is, a Büchi automaton where the only place of nondeterminism is in the initial state, while the transition function is deterministic. An $\omega$-word is accepted by $B$ iff any of the infinite runs induced by the word on $B$ passes infinitely many times through some states of $F$.

Given a qDBA $B$ and a state $s \in S$, let $B/s = \langle S, \Sigma, s, \delta, F \rangle$ denote the deterministic Büchi automaton accepting all the $\omega$-words inducing runs of $B$ starting from $s$ (where $s$ may also be a non-initial state in B). Two states $s_1$ of the qDBA $B_1$ and $s_2$ of the qDBA $B_2$ are equivalent iff the language of the $\omega$-words accepted by $B_1/s_1$ is the same as the one accepted by $B_2/s_2$.

Finally, I say that $B$ is strongly connected if for any two states $s_1$ and $s_2$ there is a finite path connecting $s_1$ to $s_2$ and vice versa.

Question. Let $B_1 = \langle S_1, \Sigma, S_{0,1}, \delta_1, F_1 \rangle$ and $B_2 = \langle S_2, \Sigma, S_{0,2}, \delta_2, F_2 \rangle$ be two strongly connected qDBAs accepting the same $\omega$-language, $L(B_1) = L(B_2) = L$. I want to prove that for every state $s_1 \in S_1$ there exists at least one state $s_2 \in S_2$ equivalent to $s_1$.

Does this property hold in general? I tried to construct counterexamples to this property, but in every case I could think of, in order to falsify the conclusion, I always needed either to drop the assumption that $\delta_2$ was a deterministic transition function, or that $B_2$ was strongly connected.

I have a strong sense this property should hold. It might even be trivial, but maybe I am using the wrong vocabulary and I cannot find this result.

My intuition so far. Suppose there are two $\omega$-words $w'$ and $w''$ accepted by $B_1/s_1$. Since $B_1$ is strongly connected, one can construct accepted words by starting with the first symbols of $w'$, then taking a path back to $s_1$, then continuing with some symbols from $w''$, then back to $s_1$, and again following $w'$ in any combination. Since $B_2$ also accepts all of these combinations but has a finite number of states, the runs corresponding to these words must eventually reach some state $s_2$ from which both $w'$ and $w''$ are possible continuations of the runs. This must hold for every set of words accepted by $B_1/s_1$. But I am not able to turn this (possibly wrong) reasoning in general, formal terms. Could you please help me do so, if possible?


Your property does not hold.

Consider the following languages over $\Sigma = \{a,b\}$:

  • There are infinitely many $a$s at even positions in a word
  • There are infinitely many $a$s at odd positions in a word

Both are representation as DBAs with the same set of states (of size 3). We can build DBAs for them that only differ in their initial states.

If we want to build an automaton for the disjunction of these languages, we can do so by taking both initial states for both of them as new initial states. This gives us a qDBA $B_1$.

The disjuction is equivalent to the language "there are infinitely many $a$s", for which a DFA $B_2$ only needs two states, each of which have the same language.

Now, $B_1$ and $B_2$ are a counter-example to your conjecture.

| cite | improve this answer | |
  • $\begingroup$ Thank you very much. You are definitely right. I wonder if there are additional constraints under which my conjecture holds. For instance, if the two qDBAs also have the same number of states. $\endgroup$ – Davide Apr 16 at 15:48

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.