Büchi automata with acceptance strategy

The problem

Let $A=langle Sigma, Q, q_0,F,Deltarangle$ be a Büchi automaton, recognizing a language $LsubseteqSigma^omega$.
We assume that $A$ has an acceptance strategy in the following sense : there is a function $sigma:Sigma^*to Q$ which can be used to pilot runs of $A$. We formalize this by the following conditions :

• $sigma(epsilon)=q_0$

• for all $uinSigma^*$ and $ainSigma$, $(sigma(u),a,sigma(ua))inDelta$

• for all $w=a_0a_1a_2dotsin L$, the run piloted by $sigma$ is accepting, i.e. the sequence $sigma(epsilon),sigma(a_0),sigma(a_0a_1),sigma(a_0a_1a_2),dots$ has infinitely many elements in $F$.

To subsume the conditions, $A$ can accept any word of its language without having to guess anything about the future.

Then, under these assumptions on $A$, is it true that $A$ can be determinized just by removing transitions ? In other words, can we always choose the next transition depending only on the current state and letter ? Is there any reference on the subject ? The same question can then be asked on co-Büchi automata, and more generally on parity automata.

What is known

Here are some partial results.

First, we can restrict $sigma$ to nondeterminstic choices between states having the same residual. Indeed, if $L(q)$ is the language accepted from $q$, an accepting strategy cannot choose $q_1$ over $q_2$ at some point, if there is $win L(q_2)setminus L(q_1)$.

Notice that the remaining choices do matter, so despite the intuition, this is not enough to get rid of the nondeterminism. This is because it is possible to stay ad infinitum in a good residual (i.e. the remaining of the word is in the residual), but reject the word because not infinitely many Büchi states are seen. This is the main difficulty of the problem : an infinite run can be wrong, without making any fatal mistake at some point.

Second, the problem is solved if $L=Sigma^omega$, i.e. all words are accepted by $A$. In this case, we can view $A$ as a Büchi game where Player I chooses input letters and Player II chooses transitions. Then we can use positional determinacy of Büchi games to extract a positional strategy for Player II. This arguments even works in the more general case of parity automata. The difficulty of this problem comes from the fact that some words are not in $L$, and in this case the strategy $sigma$ can have any behaviour.

Third, here is a proof that under the assumptions, the language $L$ is in the class of deterministic Büchi languages, witnessed by an automaton with states $2^Q$.
Notice that this implies that $L$ cannot be any $omega$-regular language, for instance if $L=(a+b)^*a^omega$, no strategy $sigma$ matching the conditions can exist.

We start by restricting the transitions according to the first remark : the only choices we can make do not impact on the residual language. We only take successors with the maximum residual, they must exist because $sigma$ exists.

Then, we build $A’=langle Sigma, 2^Q, { q_0},F’,Delta’rangle$ in the following way. $A’$ is the subset automaton of $A$, but every time a Büchi state $q$ appears in the component, all other states can be removed from the component, and we start again from the singleton ${ q}$. Then we can set $F’={{ q} : qin F}$. We can verify that $A’$ is a deterministic Büchi automaton for $L$.

Finally, by putting together the second and the third remarks, we can always obtain a finite memory-strategy $sigma$, by using a positional strategy for Player II in the game $Atimes A’$ where Player I chooses letters, Player II chooses transitions in $A$ and wins if $A$ accepts whenever $A’$ accepts.