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 and a finitely supported (or even equivariant) subset , whether there exists a word that is accepted precisely from the states in .

That condition is equivalent to being reachable from in the automaton arising from 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 of initial states:

   

which, by definition, accept a word 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 is a word of pairwise distinct atoms. Indeed, consider a state , from whence a deterministic computation checks that all of the following hold:

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

Then a word is accepted from exactly the entire orbit of those states 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!