The problem

Let $A=\langle \Sigma, Q, q_0,F,\Delta\rangle$ be a Büchi automaton, recognizing a language $L\subseteq\Sigma^\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 $u\in\Sigma^*$ and $a\in\Sigma$, $(\sigma(u),a,\sigma(ua))\in\Delta$

  • for all $w=a_0a_1a_2\dots\in 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 $w\in 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\} : q\in 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 $A\times A'$ where Player I chooses letters, Player II chooses transitions in $A$ and wins if $A$ accepts whenever $A'$ accepts.

  • $\begingroup$ Write $A_\sigma$ for the (deterministic) automaton with transitions removed. Let $w=w_0w_1\cdots$ be a word in $L$. Then by your conditions $\sigma(w_0)\sigma(w_0w_1)\cdots$ is a run of $A_\sigma$ and is accepting, thus $L\subseteq L(A_\sigma)$. Conversely, any accepting run of $A_\sigma$ is in particular an accepting run of $A$, thus $L(A_\sigma)\subseteq L$. $\endgroup$ – Sylvain May 9 '12 at 15:01
  • $\begingroup$ @Sylvain: Which transitions are removed? $\endgroup$ – Dave Clarke May 9 '12 at 15:02
  • 1
    $\begingroup$ I'm assuming you call $A_\sigma$ the automaton $A$ restricted to transitions used in the strategy $\sigma$. The problem is you don't have any guarantee that $A_\sigma$ is deterministic. For instance assume $\sigma(a)=\sigma(\epsilon)=q_0$ and $\sigma(aa)=q_1$, then $A_\sigma$ is not deterministic. $\endgroup$ – Denis May 9 '12 at 15:06
  • $\begingroup$ I'm also posting it on mathOverflow, with more details on the previous work here: mathoverflow.net/questions/97007/…, is it ok ? $\endgroup$ – Denis May 15 '12 at 14:51
  • $\begingroup$ Generally cross posting is not allowed, unless one has not received an answer after a sufficient amount of time. Given that there is an open bounty on this question, I would wait a few days. You can delete the other posting and open it in a few days. (Also, the other posting should link to this one.) $\endgroup$ – Dave Clarke May 15 '12 at 19:19

It turns out the answer is no, some counter-examples can be found in this paper.

  • $\begingroup$ thx for update, but vague! what team? did they publish? plan to? how did you hear? how did they find it? is there a reason they were looking for it? is this a theoretical curiosity or connected to some bigger problem or application? etc $\endgroup$ – vzn May 28 '12 at 15:14
  • $\begingroup$ see this answer for more details: cstheory.stackexchange.com/a/24918/8953 $\endgroup$ – Denis Mar 14 '17 at 22:47

As you pointed out, non-deterministic and deterministic Buchi automata accept different languages. The most famous 'determinization' for a Buchi automaton is given by Safra (search "Safra's construction" on web. Here's one document that comes up: www.cs.cornell.edu/courses/cs686/2003sp/Handouts/safra.pdf). The procedure is quite intricate and involves transforming given Buchi automaton into a deterministic Rabin automaton (having 'accepting' F states and 'rejecting' G states: \sigma has only finitely many states in G). Safra's construction involves much more than simply removing transitions and/or usual subset construction.

  • $\begingroup$ I know this, the question is about a special class of Büchi automata, namely the one that admit acceptance strategies $\sigma$. I already showed that this class has same power than the class of deterministic Büchi automata, and I described a simplified determinization procedure (in the "what is known" section). The conjecture is that there is a much simpler determinization procedure for this class, which consists just in removing some transitions. $\endgroup$ – Denis May 15 '12 at 17:40

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.