Two teams shipped different finite automata for one message-filter rule; how do you decide whether they accept exactly the same strings?

## Why testing strings is not an answer The tempting reply is "generate a few million messages and compare verdicts". That is a smoke test, not a decision: two machines can agree on every string shorter than some length and diverge immediately afterwards, and nothing in a random sample tells you where the boundary is. Equivalence of finite automata is **decidable**, exactly and cheaply, so an interviewer treats sampling as an admission that you do not know the construction. The second tempting reply — compare the transition tables — is also wrong. The same language admits machines with different state counts, different state names, unreachable junk and differently shaped loops. Structural equality implies language equality; the converse does not hold. ## Reduce equality to emptiness The standard move is to express the property you want as the **emptiness** of a language you can construct: - `L1 = L2` holds exactly when no string lies in one language but not the other. - The strings that do lie in exactly one are the **symmetric difference**: `(L1 minus L2)` united with `(L2 minus L1)`. - So `L1 = L2` holds exactly when the symmetric difference is empty. And the symmetric difference is one line of the product construction. Pair the two machines, keep the lockstep transitions, and mark `(p, q)` accepting when exactly one of the two components is accepting in its own machine. Nothing else about the product changes. Getting the accepting condition backwards is the most common error in this material. "Both accept" is intersection and answers a different question entirely; you want **exactly one**. ## Emptiness is a reachability search A finite automaton accepts nothing precisely when no accepting state is reachable from the start state. Acceptance means a path from the start to an accepting state whose edge labels spell the input, so no such path means no such input. The decision procedure is therefore an ordinary traversal of the transition graph — no automata theory beyond the reduction itself: 1. Start from the pair of start states. 2. Visit pairs breadth-first, expanding each pair on every alphabet symbol. 3. Stop at the first pair where exactly one component accepts. 4. If the search exhausts the reachable pairs without finding one, the machines are equivalent. Because you stop at the first disagreement, the search usually touches a tiny fraction of the worst-case pair count, and you never build the full product. ## The counterexample is the real payoff A yes/no verdict is worth much less than what the search hands you on the way. Carry the string spelled by the path alongside each pair in the queue, and the moment you hit a disagreeing pair you have a **concrete message** that one machine accepts and the other rejects. Breadth-first order makes it the shortest such message. That artefact goes straight into the regression suite, into the bug report, and into the conversation with whichever team owns the rule — it turns "your machines differ" into "they differ on this input, and here is what each does with it". ## Preconditions and costs | condition | why it matters | |---|---| | both machines deterministic | the pair must track one state per machine, not a set of them | | both machines total | a stuck component ends the joint run and can hide a disagreement | | same alphabet | pairs step on shared symbols; differing alphabets must be reconciled first | | lazy exploration | the reachable pairs are usually far fewer than the product bound | If one machine is nondeterministic, determinise the side that ends up being complemented before pairing — that is the step that can blow up exponentially, and it is worth arranging so it happens at most once. A second route to the same verdict reduces each machine to a canonical form and compares those directly; it answers the question but yields no counterexample, and the canonicalisation algorithm is a separate subject. ## What the interviewer is checking That you reach for a reduction rather than a test harness; that you name **emptiness** as the primitive and reachability as its implementation; that you get the accepting condition the right way round; and that you notice the failing path is itself the deliverable. A candidate who ends on "and then I have a counterexample string I can put in a test" has demonstrated the difference between knowing the theory and having used it.