What is the algorithm for a decider to get the language accepted by a DFA? I am trying to understand the larger problem of the decidability of the equality of two DFAs. I understand that this problem can be solved using minimizing DFAs, but my textbook states this can be done using symmetric difference.

Theorem: Let $EQ$ be a language, where $EQ$ = $\{&lt;A,B&gt; \mid \text{A and B are both DFAs and L(A) = L(B)}\}$. 
In my notation, $L(X)$ stands for the language that DFA $X$ recognizes. 

Prove that $EQ$ is decidable. This relies on the symmetric difference of 2 sets.

Proof: Let $Q$ be a decider defined as: 

On input $&lt;A,B&gt;$ do: 


Construct a DFA $C$ such that $L(C) = (L(A) \cap \overline{L(B)}) \cup (\overline{L(A)} \cap L(B)) $
Run $&lt;C&gt;$ on the algorithm used to determine if the language recognized by a DFA is $\emptyset$  (We proved this is decidable before, and I have no issues with that).
If that algorithm accepts, then $Q$ accepts
If that algorithm rejects, then $Q$ rejects


For $Q$ to be a decider, we must prove that $Q$ will halt. Since we have proven that the algorithm used in step 2 is decidable, it will halt. So I have no problems with steps 2-4.

But the first step, how can I prove that constructing $C$ in that way will halt? I understand that the symmetric difference will result in a regular language because of the closure properties, but how can a decider actually carry out this process and be guaranteed to halt?

So this is my primary question, what is the algorithm for determining the language that a DFA accepts? I.e. given DFA $X$, how can I determine $L(X)$ (Again, this must halt, so we can't try every string in existence or something like that).

Some follow up questions are: What if the DFA in question accepts an infinite set of strings, how can we possibly represent that on the decider's tape (or if the complement of $L(A)$ is infinite, etc.)? How can a decider determine the compliment of a set? And if $L(C)$ ends up being an infinite set of strings, how can we process that so that we can construct DFA $C$? 

My book simply states


  These constructions are algorithms that can be carried out by Turing
  machines.


which drives me nuts! Prove it.
Suppose that $A,B$ are two DFAs on a common alphabet $\Sigma$ with states $Q_A,Q_B$, initial states $q_{0A},q_{0B}$, final states $F_A,F_B$, and transition functions $\delta_A,\delta_B$. We define a product DFA as follows:


$Q = Q_A \times Q_B$.
$q_0 = \langle q_{0A}, q_{0B} \rangle$.
$F$ consists of all pairs $(q_A,q_B)$ such that either $q_A \in F_A$ and $q_B \notin F_B$ or $q_A \notin F_A$ and $q_B \in F_B$.
$\delta(\langle q_A,q_B \rangle, \sigma) = \langle \delta_A(q_A, \sigma), \delta_B(q_B, \sigma) \rangle$.


You can prove by induction that $\delta(q_0, w) = \langle \delta_A(q_{0A}, w), \delta_B(q_{0B}, w) \rangle$, and so our definition of $F$ guarantees that the language of this DFA is the symmetric difference of $L(A)$ and $L(B)$.

In order to know whether $L(A) = L(B)$, we have to check whether their symmetric difference is empty. This happens exactly when no accepting state is reachable from the initial state in the product DFA, a condition which we can check using BFS/DFS.