General proof of equivalence of two FSMs in finite time?

Question

Does a general proof exist for the equivalence of two (deterministic) finite state machines that always takes finite time? That is, given two FSMs, can you prove that given the same inputs they will always produce the same outputs without actually needing to execute the FSMs (which could be non-terminating?). If such a proof does exist, what is the time complexity?

Answer 1

There is a proof, though I don't know it. Look for Sipser's textbook on the subject, that's where I know of it from.

Scrounging my memory: basically, there is a unique minimal DFA for a given DFA, and there is a minimization algorithm that always terminates. Minimize both A and B, and see if they have the same minimal DFA. I don't know the complexity of the minimization, though its not too bad (I think its polynomial). Graph isomorphism is pretty hard to compute, but because there's a special starting node, it may hopefully be somewhat easier. You may not even require graph isomorphism, to be honest.

But no, you don't ever need to actually run the DFAs, just analyze their structure.