Deterministic finite automata (DFAs) are perhaps one of the simplest models of computation. A classic result is that if two automata with n states are language inequivalent, then there is a word of length at most n that is accepted by only one of the automata, i.e. the word is distinguishing. In a sense this distinguishing word proofs/explains/witnesses why the DFAs are inequivalent. We are interested in explaining DFA inequivalence with more sophisticated properties such as: “all words with an even number of a’s are accepted”, which in turn is only satisfied in one of the DFAs. In this talk we’ll look at distinguishing DFAs which can act as such witnesses.