Büchi automata with acceptance strategy

Theoretical Computer Science Asked on November 26, 2020

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.

2 Answers

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

Also here is a more recent work showing that such Büchi automata can be recognized in polynomial time.

Correct answer by Denis on November 26, 2020

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: 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.

Answered by Sudeep on November 26, 2020

Add your own answers!

Ask a Question

Get help from others!

© 2024 All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP