Are there algorithms for proving two finite state machines are equivalent?

Suppose we call two finite state machines equivalent if they "perform the same computation" - they accept the same language, or they produce the same output for any given input. Is there an algorithm for checking if two finite state machines are equivalent?

Given two deterministic finite automata $A_1,A_2$, you can construct the product automaton $A_1 \times A_2$ using the product construction. Let a mixed state be one which is accepting in $A_1$ and rejecting in $A_2$, or vice versa. The two automata are equivalent iff no mixed stated is reachable from the initial state.