Equivalence of infinite behavior of finite automata (Q1060562)

Working on an infinite word, a deterministic finite automaton generates a sequence of passed states. We say that a given word is accepted by a given automaton iff the above sequence has infinitely many occurrences of some terminal state. That definition can be easily transferred to non- deterministic automata by adding ''there exists such a sequence of passed states that has...''. Two automata are said to be equivalent iff their sets of accepted words are equal. The well-known Büchi's algorithm for deciding, given two finite automata, upon their equivalence, requires a computational time proportional to \((n^ 2)^{n^ 2}\) where n is the maximal number of states of two given automata. Here a new algorithm is proposed which requires only \(n^ 32^{3n(n+1)}\).