To translate a formula into a Testing Automaton

Start by building a Büchi automaton

Then, gather all the atomic proposition in the formula, and create an automaton with changesets

Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by {}), marking as livelock accepting (rectangles) any states from which there exists a an accepting path labeled by {}.

Finally, use bisimulation to minimize the number of states.