the DFA equivalence problem
Suppose someone gives you two finite automata that look different — different states, different wiring — and asks: do they actually recognize exactly the same language? This is the equivalence question, EQ_DFA = {(A, B) : A and B are DFAs and they recognize the same language}. It sounds like you would have to compare their behaviour on infinitely many strings, but there is an elegant way to reduce it to a single emptiness test.
The key idea is the symmetric difference. Two sets are equal exactly when nothing belongs to one but not the other — that is, when their symmetric difference (the strings accepted by A but not B, together with those accepted by B but not A) is empty. The symmetric difference of two regular languages is itself regular, and you can build a DFA C for it directly using the product construction together with complementation: C = (A ∩ not-B) ∪ (not-A ∩ B). Constructing C is a finite, mechanical job. Then A and B are equivalent if and only if the language of C is empty, which you settle with the DFA emptiness procedure (a finite reachability search). Accept (A, B) into EQ_DFA exactly when C's language turns out empty.
So EQ_DFA is DECIDABLE — equivalence of finite automata is algorithmically tame. This matters because it means you can mechanically verify that two finite-state designs (two regex engines, two circuits, two protocol specs) behave identically on all inputs, something you cannot do for richer models. The contrast is sharp and worth flagging: equivalence is decidable for DFAs but UNDECIDABLE for context-free grammars and for Turing machines. Finite memory is what makes equality checkable; once a model can use unbounded memory, comparing two of them for equality slips beyond reach.
To check if A and B agree on all inputs, build C accepting exactly the strings on which they DISAGREE (in A xor in B). Run the emptiness test on C: if C's language is empty, no string distinguishes them, so they are equivalent; if some string reaches an accept state of C, that string is a concrete counterexample.
Equality of languages = emptiness of their symmetric difference — a finite, decidable check.
Equivalence is decidable for DFAs but UNDECIDABLE for CFGs and Turing machines. The reduction to one emptiness test works only because finite automata have finite memory.