Fix attention on equality atoms.
Given an orbit-finite, deterministic automaton on the alphabet of atoms, a Brzozowski phase amounts to:
- reversing the direction of all transition arrows and swapping initial and accepting states,
- determinising the result, and
- cutting to the reachable part.
In other words, given an automaton
one constructs an automaton with:
- subsets of as states,
- as the initial state,
- as accepting states, those for which ,
- for any , the inverse image along as the transition function at .
The result of this may be orbit-infinite even after restricting to the reachable part; for example, consider as the minimal automaton for the language
However, the resulting automaton is always locally finite: any fixed finite set of atoms supports only finitely many states.
I conjecture that, moreover, any reachable state with a small support can be reached by a word with a small support. More formally:
Conjecture. For any automaton there exists a computable function such that, in the automaton obtained from by a Brzozowski phase, every reachable state with support of size is reachable by a word with support of size at most .
The function should be computable for any , and, as a mathematical object, it should also be computable from .
My guess is that , where depends only on and not on .
PRIZE! I offer a bottle of nice Barbadian rum to the first person who will prove or disprove this conjecture.
Edit [April 8, 2014]: The conjecture has been now disproved by Mikołaj Bojańczyk, who gets the bottle. Thanks Mikołaj!