The LTL formula that is translated there is F [a WU b] ∨ [a SB (F c)]. The first step of the translation is done by abbreviating the elementary subformulas (those starting with a temporal logic operator):
- q0<->[a WU b]
- q1<->(F q0)
- q2<->(F c)
- q3<->[a SB q2]
and the remaining formula q1∨q3 remains as initial condition. Then, we use the equivalences you find on the slides to "implement" the above abbreviations by transition relations and GF-acceptance constraints for the introduced variables:
- q0<->b|a&next(q0) with GF(a->q0)
- q1<->q0|next(q1) with GF(q1->q0)
- q2<->c|next(q2) with GF(q2->c)
- q3<->!q2&(a|next(q3)) with GF(q3->a)
So, these are four constraints that you expected, and the automaton constructed with the four GF-constraints is equivalent to the given LTL formula. It would be a fine solution for the mentioned exam problem.
As you can read on the slides in the temporal logic chapter after that translation, it is possible that we can omit some of the GF-constraints, since these are redundant (they don't harm the correctness, but are useless): The constraints of positive occurrences of weak operators and negative occurrences of strong operators can be omitted. Hence, the constraint GF(a->q0) for the WU and the constraint GF(q2->c) for the F(c) are skipped.
The before operators are a bit nasty here, since like negations, they change the sign of the occurrence of their second arguments. This is best seen when replacing the SB by a WU:
[a SB (F c)] = ¬[(¬a) WU (F c)]
Now you see that the positive occurrence of the subformula [a SB (F c)] becomes a negative one for (F c), and a positive one for a.
