# Automata

Compare complete transition systems through their reachable product, rather than checking a short sample of strings.

## Definitions

- **DFA**: A deterministic transition function over a finite state set and alphabet.
- **Product state**: A pair of states reached by reading the same prefix in both automata.
- **Distinguishing word**: A finite input accepted by exactly one of the compared machines.

## Acceptance procedure

1. Start from the pair of initial states.
2. Explore every symbol transition until no new pair is reachable.
3. Compare acceptance in every reachable pair.
4. For inequivalence, replay a distinguishing input from both initial states.

## Complexity

At most |Q₁|·|Q₂| product states are visited, with one outgoing edge per alphabet symbol.

## Common failure

Bounded string testing is weaker than complete DFA product exploration.

## Extensions

Extend the checker to emit shortest distinguishing words and state-minimization partitions.

## Instances

- KL-FCS-002: Two automata, one parity language — Equivalent: yes
- KL-FCS-014: Parity language under renaming — Equivalent: yes
- KL-FCS-015: A one-symbol counterexample — Equivalent: no

## References

- https://ocw.mit.edu/courses/18-404j-theory-of-computation-fall-2020/download/