Proving NFA accepts reverse string of DFA

[prov]

I have seen descriptions for an algorithm that can take a regular deterministic finite automata and create a non-deterministic finite automata that is guaranteed to generate the reverse of string accepted by the DFA. Does anyone know of a "formal" proof that shows this is true in all cases? Guessing induction would be used to prove?

The algorithm goes something like this:

Take original DFA, and change the initial state to the final state
Reverse all accepting states in DFA to non-accepting states
Set original starting state to accepting state and reverse all transitions
Any thoughts would be greatly appreciated!

 

[Future Bruno]

A formal proof of this algorithm would involve constructing a mathematical proof, showing that the algorithm produces a non-deterministic finite automata that is guaranteed to generate the reverse of strings accepted by the DFA. This proof could be constructed by induction. First, it should be noted that the algorithm produces a non-deterministic finite automaton with exactly the same number of states and transitions as the original DFA. This can be shown by proving that each transition from the original DFA is reversed in the new automaton, and that each original state is either reversed or kept unchanged.Next, it should be shown that the resulting automaton generates the reverse of strings accepted by the original DFA. This can be done by considering the two paths taken by the automaton when accepting a string in the original DFA, and showing that they are reversed in the new automaton. Namely, if the original DFA started at the initial state and progressed through a series of transitions before reaching an accepting state, then the new automaton will start at the final state, reverse those transitions, and reach the initial state. Finally, it should be shown that the resulting automaton is guaranteed to generate the reverse of strings accepted by the original DFA. This can be done by proving that, for any string accepted by the original DFA, the new automaton will always take the same reversed path and thus produce the reverse of the string. Additionally, it should be shown that the new automaton does not accept any strings that are not accepted by the original DFA. In summary, a formal proof that the algorithm produces a non-deterministic finite automata that is guaranteed to generate the reverse of strings accepted by the DFA can be constructed by induction. It should show that the algorithm produces an automaton with the same number of states and transitions and that it produces the reverse of strings accepted by the original DFA. Finally, it should show that the new automaton is guaranteed to generate the reverse of strings accepted by the original DFA and that it does not accept any strings that are not accepted by the original DFA.