Is the equality of two DFAs a decidable problem?

So given two DFAs, is the problem of finding if they generate the same language a Decidable problem?

I already know that Equality of two CFL is not Decidable

but what about Equality of two DFAs? considering most of the problems with DFAs are decidable, is this decidable as well ?

In order to decide whether the languages generated by two DFAs $A_1,A_2$ by the same, construct a DFA $A_\Delta$ for the symmetric difference $L(A_1) \Delta L(A_2) := (L(A_1) \setminus L(A_2)) \cup (L(A_2) \setminus L(A_1))$, and check whether $L(A_\Delta) = \emptyset$.

Here are some more details. You can construct $A_\Delta$ using the product construction: construct a product automaton, and use $(F_1 \times \overline{F_2}) \cup (\overline{F_1} \times F_2)$ as the set of accepting states.

In order to check whether $L(A_\Delta)$ is empty or not, it suffices to check whether some accepting state is reachable from the initial state, and this can be done using BFS/DFS.

StackExchange Computer Science Q#81813, answer score: 23