Testing DFA Equivalence with Union-Find Instead of a Product Table

Deciding whether two deterministic automata accept the same language is the most common question asked of a machine when a lexer table is regenerated: an optimiser rewrote the table, a specification was revised, a lexer was rebuilt. The straightforward method is to build the product machine, mark the pairs where one component accepts and the other does not, and search for a reachable marked pair. That method is correct and it costs a table of size |Q₁| · |Q₂|, which for two machines of 50,000 states is 2.5 billion entries.

The union-find method answers the same question without ever materializing the product. It explores reachable pairs one at a time, merges pairs that are already known to be equivalent, and stops at the first pair that is not. Its running time is near-linear in the size of the two machines, and its memory is a disjoint-set forest over pairs rather than a dense table.

The invariant behind the search

Equivalence of two states means: for every input string, both reach an accepting state or neither does. The search maintains a set of pairs that are assumed equivalent, and checks the assumption for consistency. If (p, q) is assumed equivalent, then for every symbol a the pair (δ₁(p, a), δ₂(q, a)) must also be equivalent, and p and q must agree on acceptance. The assumption is consistent exactly when the closure of the start pair under this rule contains no acceptance mismatch.

This is the same coinductive argument that underlies bisimulation checking, and it has the same shape as the partition refinement of a single machine: two states are equivalent when their acceptance labels match and their successors on every symbol are equivalent. The difference is that the relation here spans two machines rather than one, so the objects being merged are pairs rather than states.

The algorithm is a worklist over pairs:

1. Merge the start pair (q₁, q₂) into one equivalence class.
2. Pop a pair from the worklist. If the components disagree on acceptance, report non-equivalence.
3. For each symbol a, form the successor pair and merge it with the current pair’s class. If the merge joined two previously distinct classes, push the newly joined pair for processing.

The merge step is where union-find enters. Each class of pairs represents an obligation: all pairs in the class must be equivalent. When a successor pair joins a class, the obligation propagates, and processing that class once discharges all its members.

def equivalent(m1, m2, nsym):
    parent = {}
    def find(x):
        while parent[x] != x:
            parent[x] = parent[parent[x]]
            x = parent[x]
        return x
    def union(a, b):
        ra, rb = find(a), find(b)
        if ra == rb:
            return None
        parent[rb] = ra
        return (a, b)

    start = (m1.start, m2.start)
    parent[start] = start
    work = [start]
    while work:
        p, q = work.pop()
        if m1.accept[p] != m2.accept[q]:
            return False                      # an assumed-equivalent pair disagrees
        for a in range(nsym):
            s = (m1.delta[p][a], m2.delta[q][a])
            if s not in parent:
                parent[s] = s
                work.append(s)
                continue
            merged = union((p, q), s)
            if merged is not None:
                work.append(s)                # new obligation: process the joined pair
    return True

The parent dictionary is doing double duty: it is the union-find forest and the visited set. A pair that has never been seen gets its own singleton class and is pushed immediately, because its obligation has not been checked. A pair that has been seen gets merged, and only a merge that actually joined two classes produces new work.

Why the merge is the whole trick

Without the union step, the algorithm is the product construction with a lazy exploration order, and its cost is the number of reachable pairs, which can be |Q₁| · |Q₂|. The merge is what collapses that: when a successor pair is already known to be in the same class as the current pair, there is nothing new to check, and the pair is not pushed.

The effect is most visible on machines that are equivalent but structurally different. Suppose both machines are minimal DFAs for the same language, with |Q| states each. Then they are isomorphic, and every pair visited by the search is of the form (p, φ(p)) for a fixed bijection φ. The search reaches |Q| distinct pairs, one per state, and the work is |Q| · |Σ| successor computations rather than the |Q|² · |Σ| that a full product table would imply.

When the machines are not equivalent, the search stops at the first reachable pair with mismatched acceptance. That pair is a witness: the input string spelled by the path from the start pair to it is accepted by exactly one machine. Reporting the witness is a matter of keeping a parent pointer from each pair to the pair that generated it, which is a second forest over the same nodes.

Complexity and the constant that matters

With union by rank and path compression, a sequence of m operations on n elements costs O(m α(n)), where α is the inverse Ackermann function and is below 5 for any input that fits in memory. The number of merges is bounded by the number of pairs discovered, and the number of pairs discovered is bounded by the number of reachable pairs in the product. So the algorithm’s time is O(r · |Σ| · α(r)) where r is the number of reachable pairs, and its memory is O(r).

That bound is stated in terms of r rather than |Q₁| · |Q₂| because the search only visits reachable pairs. In the worst case r equals the product size, and no algorithm that must examine every reachable pair can do better. The practical gain is on the common case, where r is much smaller than the product and the memory is proportional to what was actually explored.

The |Σ| factor is unavoidable in the straightforward formulation: each processed pair generates one successor per symbol. For a 256-symbol alphabet and 10,000 processed pairs, that is 2.56 million successor computations, each a pair of indexed loads and a hash lookup. The hash lookup is usually the dominant cost, which is why implementations key pairs by a packed integer when the state counts are small enough to fit: p * |Q₂| + q fits in 32 bits when the product is below 2³², and an array-backed union-find over that range replaces the hash table with direct indexing. The array version needs an explicit “unvisited” marker such as -1 to tell a pair that has never been seen from one that is its own class, and it has to compress paths in find with a loop rather than the one-line parent update above, since the slot is a plain integer rather than a dictionary entry.

What the algorithm does not decide

Equivalence is not inclusion. The union-find search compares two machines that consume the same input and asks whether their verdicts always agree. Inclusion asks whether every string accepted by one is accepted by the other, which is the same as asking whether the first machine’s language is disjoint from the complement of the second. That question needs the complement, and complement needs a total transition function, as described in product constructions for boolean operations.

The same pair search answers inclusion with one change to its acceptance test: a pair (p, q) is a counterexample when p accepts and q rejects, and no other label combination produces a verdict. That asymmetry is sound as it stands, because the pairs the search explores are exactly the pairs reachable by one common input string: a reachable pair with p accepting and q rejecting is a string in the first language and outside the second. The equivalence test uses symmetric disagreement because it has to answer in both directions at once.

The asymmetry does cost the pruning that makes equivalence cheap on isomorphic machines, however. With p rejecting, the pair is not a counterexample, but its successors must still be explored, since some continuation of that same prefix could reach p′ accepting. Restricting exploration to accepting p is therefore not an option; the union-find classes still record which pairs have already been visited, but they no longer let the search skip a subtree. The usual implementation does not special-case this at all: it completes both machines with a dead state and runs the symmetric equivalence search on the first machine against the complement of the second, which reuses one code path at the cost of one extra state per machine.

Equivalence of nondeterministic machines is a different problem. Two NFAs can be equivalent while having no structural relationship at all, and the standard method is to determinize both and compare, which brings back the exponential. There is no union-find shortcut for the nondeterministic case, because the relation being checked is not a bisimulation: an NFA state’s behaviour is a set of possible futures, and matching sets requires the subset construction.

Reading the verdict

A true verdict from the search is a proof of equivalence. The union-find classes at the end are a bisimulation relation between the two machines’ reachable states, and the proof that it is a bisimulation is the invariant maintained at every merge: acceptance labels agree within a class, and successors of class members land in a common class. Equivalence of the two machines is the same statement as the two languages having the same right congruence classes, which is what the Myhill-Nerode theorem characterizes.

A false verdict is a counterexample. The witness string is the path in the search tree from the start pair to the mismatched pair, and its length is bounded by the number of pairs visited, since each step consumes one symbol. That bound is |Q₁| · |Q₂| in the worst case, which is also the bound on the length of the shortest distinguishing string between two non-equivalent machines with those state counts. A tool that reports the witness gives the user something actionable: the input on which the rewritten machine and the reference machine disagree.

The search order determines which witness is found. A depth-first worklist finds a witness whose length is bounded by the depth of the search tree, which can be long; a breadth-first worklist finds a shortest witness but needs a queue proportional to the frontier. For diagnostics, breadth-first is worth the memory, because the shortest counterexample is the one a user can read.

Where the check is worth running

The check is cheap enough to run on every regeneration. A lexer generator that emits a minimized table can compare it against the table from the previous run, and a difference means either a genuine change in the specification or a bug in the generator. The same check validates an optimiser: a transformation that rewrites the table is correct exactly when the result is equivalent to the input, and the union-find search is the cheapest available test of that property.

It is also the right primitive for comparing a hand-written machine against a machine emitted by a tool. The two will rarely be isomorphic, so a structural diff is useless, and the equivalence search answers the question that actually matters without requiring either machine to be minimized first. Minimization followed by isomorphism testing is the alternative, and it costs two refinement passes plus a canonical renumbering, which is more work than one lazy pair search on the machines as they stand.