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?
