# How to prove that {<M1, M2> : M1 and M2 are two DFAs and L(M1) $\neq$ L(M2)} is in NL?

My idea is to find a turing machine which recognizes this language in $$\log N$$ space, could anyone give me some clue on how to find such turing machine?

Let $$M = M_1 \times M_2$$ be the product automaton for $$L(M_1) \Delta L(M_2)$$. Then $$L(M_1) \neq L(M_2)$$ iff some accepting state is reachable from the initial state. Finally, directed reachability is in $$\mathsf{NL}$$ (in fact, $$\mathsf{NL}$$-complete).