Well. The transitions formula is already in the solutions. It's ¬q∧a∧¬b∧¬q′∨(q∨b)∧q'.
Actually, when I designed the solution. I first drew the automaton, and then extracted the transition relation from that. The transition formula is a formula over the state variables, the alphabet, and the primed variables. Precisely the formulas satisfying assignments are the transitions that are in the relation. I divided the transitions into two parts. The incoming transitions of {}, and the ones of {q}. The transition to {} comes from q itself, and goes to {}. That's why we have ¬q∧¬q'. The condition of that transition is a∧¬b. If we add that as a conjunction, we get ¬q∧a∧¬b∧¬q′. The transitions to {q} both come from {q} itself with no condition and from {} with the condition b. If we write down these cases explicitly, we get the two formulas ¬q∧b∧q' and q∧q'. I simplified that as (q∨b)∧q'.
Symbolic transition relations were our topic in the Transition Systems chapter starting from slide 55.
How did I obtain the automaton itself? It is an NDetF automaton. So once we reach an accepting state on any infinite path corresponding to the input, we accept this input word. Thus, the initial state should rather not be accepting and we need at least one accepting state. The paths described by [a SU b] have three parts. First, they can not satisfy b for arbitrarily (including zero) steps but they need to satisfy a in every of these steps. Then they satisfy b for at least one state. And in the third part, they may do whatever they want. The waiting for the second part is implemented by having a self-loop at the non-accepting initial state. The condition of this self-loop is a∧¬b. As that's how the first part looks like. If our path doesn't satisfy this condition at any step, there is just no run in the automaton, and thus we don't accept. That's just the magic of non-determinism. The second part is just checked by this singled transition with the condition b from the non-accepting to the accepting state. Pretty straight-forward. Any accepting run needs to cross this transition at least once. Thus, we ensure that our input path satisfies b at least once (that's the strong about the strong until). For the third part of our input, we have no requirements. It can be any infinite suffix. Thus, we have a self-loop with no condition.
Did that make it clearer?
The deterministic version of the automaton (task c and d) is obtained in a similar way. As I said, we used the magic of non-determinism by just not offering any transition if we want to reject the input. In a deterministic world, we have to provide precisely one infinite run for any input. It just may not contain an accepting state. Thus, we just add a non-accepting (and non-initial) state with a self-loop with no condition. This fail state is reached by the remaining transition from the initial state. Thus, the transition from the initial to the fail state has the condition ¬a∧¬b.
In order to label the new state, I needed to introduce the fresh variable r. This actually produces two states {q} and {q,r}. For the unreachable state {q,r}, I just added any transition I found easy to write down in the symbolic variant.