Why does partition refinement alone fail to give the smallest deterministic acceptor when some of its states are unreachable?

A firmware team runs a minimizer over their door controller, sees the state count drop, and concludes the machine is minimal. It usually is not, and the reason is a gap between two different notions that both feel like `unnecessary state`. ## Two independent defects, one symptom | Defect | What it means | Which step removes it | |---|---|---| | Redundant states | Two or more states agree on every suffix | Partition refinement merges them | | Unreachable states | No input sequence from the start state visits it | A reachability search deletes them | Refinement answers only the first question. Its entire mechanism is a comparison of futures: it groups states whose behaviour on every remaining input agrees. Reachability is a fact about the past — about which states the start state can get to — and no amount of suffix comparison observes it. ## A concrete leftover Take the badge controller that unlocks on the second valid scan, and suppose an earlier revision left behind a maintenance state `M` that nothing points at any more: `M` is non-accepting, a valid scan `v` keeps it in `M`, and a rejected scan `x` sends it straight to the unlocked accepting state. Is `M` mergeable with anything live? The suffix `x` accepts from `M`, but from every live non-accepting state a single rejected scan leaves the machine non-accepting. The empty suffix separates `M` from the accepting states. So `M` is distinguishable from every other state, refinement keeps it in a block of its own, and the result has four states where the language needs three. The accepted language is untouched — no input reaches `M`, so it can never influence a verdict. That is precisely why this defect survives a test suite: every behavioural test passes. ## Order: cost, not correctness The habit is to trim first, and it is a good habit, but be precise about why. Distinguishability is defined by the transition function and the accepting set alone, so the presence of unreachable states cannot split two reachable states that are equivalent and cannot merge two that are not. Consequences: - **Trim then refine** — the conventional order, and the cheaper one, because refinement runs over a smaller machine. - **Refine then trim** — also correct: discard the blocks the quotient machine cannot reach and you land on the same minimal machine. - **Refine and never trim** — the actual bug. The machine still accepts the right language, so nothing fails, and it is quietly larger than minimal. ## Why the extra state matters even though the language is right The practical payoff of minimization is canonicity: for a given language the minimal machine is unique up to renaming states, so two teams can compare machines instead of arguing. An untrimmed result is not that object. Two teams who each skip the trim, and each carry different leftovers, will get two different `minimal` machines for one language and will read that difference as a specification disagreement that does not exist. There is also the ordinary engineering cost: dead state entries in a transition table, code paths that no fuzzer will ever cover, and a diagram whose reader has to work out that a whole branch is decoration. ## The lookalike that is not a defect A **trap state** — sometimes called a dead state — is a non-accepting state with all its transitions pointing back at itself, entered once a sequence can no longer be completed. It is reachable, it is entered by real input, and in a complete deterministic acceptor it is a legitimate and usually necessary state: it is the class of all inputs with no accepting extension. Do not confuse it with an unreachable state. Only if you allow a partial transition function may the trap be dropped, and then the machine is no longer complete and refinement's assumption of total transitions no longer holds. ## How to find the unreachable states Search forward from the start state — breadth-first or depth-first over the transition function, marking as you go. Every state left unmarked is unreachable. Checking for missing incoming edges is not the same test: a group of unreachable states can point at each other happily, each with an incoming edge, and none of them reachable from the start.