The Rum Conjecture is refuted

A conjecture I posted a while ago, concerning reachability of states in automata with atoms after a Brzozowski phase, has been refuted by Mikołaj Bojańczyk.

Mikołaj proved that it is undecidable, given a deterministic orbit-finite automaton {\cal A}=(Q,q_0,F,\to) and a finitely supported (or even equivariant) subset I\subseteq Q, whether there exists a word w that is accepted precisely from the states in I.

That condition is equivalent to I being reachable from F in the automaton arising from {\cal A} by a Brzozowski phase. My conjecture would imply that reachability after a Brzozowski phase is decidable, so the conjecture is hereby refuted.

Mikołaj’s construction resembles the one used by Neven, Schwentick and Vianu to prove undecidability of universality in nondeterministic register automata. It is most naturally phrased in terms of a variant of deterministic automata (call them Miktomata) with an equivariant set I\subseteq Q of initial states:


which, by definition, accept a word w iff it is accepted from every initial state. It is enough to show that the emptiness problem of miktomata is undecidable.

To this end, first show that a miktomaton can recognize the language of words of the form


where w\in\mathbb{A}^* is a word of pairwise distinct atoms. Indeed, consider a state (a,b)\in\mathbb{A}^2, from whence a deterministic computation checks that all of the following hold:

  • if some a in the input word is immediately followed by b then every a is immediately followed by b,
  • if some a is immediately followed by \# then every a is immediately followed by \#,
  • if some b is immediately preceded by \# then every b is immediately preceded by \#.

Then a word is accepted from exactly the entire orbit of those states (a,b) if and only if it is of the form above.

This, together with the easy fact that languages recognized by miktomata are closed under intersection, is enough to construct a miktomaton that recognizes encodings of accepting runs of Turing machines. (The atoms in a \#-separated word as above serve as pointers to corresponding cells on the machine tape, to provide control over neighboring configuration encodings).

As promised, Mikołaj gets a bottle of Barbadian rum for solving the problem which I had been puzzling over for a long while. Thanks Mikołaj!

This, by the way, implies that there is no hope of fully constructing the result of a single Brzozowski phase of a deterministic automaton with atoms, even if we restrict to states with small support. As a result, any kind of Brzozowski-like algorithm for automata with atoms will have to do something tricky in its first phase. We have a good idea of how this may be done; stay tuned!

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>