How to prove that { : M1 and M2 are two DFAs and L(M1) $\neq$ L(M2)} is in NL?
Yuval's answer describes the main component. For the sake of completeness I'll precise a couple of details.
First, $L(M_1) \neq L(M_2)$ means that there is a string that is accepted by one of the automaton but not the other. Let's &quot;build&quot; an automaton $M$ that accepts precisely such strings, and we will then want to check whether it accepts a least one string. Then $M$ has states $(q^1_i, q^2_j)$ for each state $q_i$ of $M_1$ and $q_j$ of $M_2$. A state $(q^1_i, q^2_j)$ of $M$ is accepting if and only if $q_i$ is accepting in $M_1$ and $q_j$ is not accepting in $M_2$ or vice versa. Now, in order to tell if $M$ accepts a string, we need to know if there's an accepting node that is reachable from $(q^1_0, q^2_0)$. We can first guess such a state $(q^1_m, q^2_n)$ as its representation uses only a logarithmic number of bits. Then we can, one step at a time, guess a path of states from $(q^1_0, q^2_0)$ leading to $(q^1_m, q^2_n)$. Of course after each guess we need to actually verify that there is an edge in $M$ from the previous state to the recently guessed one. In order to do that we can always keep two states in memory, the current one and the state we just guessed as the next one, this uses logarithmic memory still.