The translation is described on slides 71-75; examples are given on slides 76-79; and the correctness proof is given on slides 61-70. Have a look at that.
In a nutshell: The idea is to abbreviate sub formulas starting with a temporal logic operator with a new state variable of the automaton; and these abbreviations become then a part of the transition relation and yield a fairness constraint.
