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?

Aim

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.

Cock

Graph isomorphism is not known to be NP-complete, and in fact, is believed not to be. – Impercipient

You're absolutely right, my mistake. I have edited the post to fix that. – Cock

Answer 2

Suppose you have two FSMs with O(n) states. Then you can make an FSM of size O(n²) that recognizes only the symmetric difference of their accept languages. (Make an FSM that has states that correspond to a pair of states, one from each FSM. Then on each step, update each part of the pair simultaneously. A state in the new FSM is an accept state iff exactly one of the pair was an accept state.) Now minimize this FSM and see if it is the same as the trivial one-state FSM that rejects everything. Minimizing an FSM with m states takes time O(m log m), so overall you can do everything in time O(n² log n).

@Agor correctly states that Sipser is a good reference for these sorts of things. The key point of my answer is that you can do this in polynomial time, even with a small exponent.

Impercipient