The semantics of the until operator is really defined by the first automaton on your image which is the one taken from the lecture notes. To understand this, you should maybe distinguish between initial and global validity: Initial validity requires that a formula holds at initial time while global validity requires that the formula holds at any point of time. Maybe that is what bothers you since your automaton satisfies not only [a SU b] but even G[a SU b] (but it does not accept all paths that satisfy [a SU b]).
To understand that, consider the recursive law on your photo
[a SU b] = b | a & X[a SU b]
Hence, if we have a&!b, then
[a SU b] = X[a SU b]
which explains why we stay in the initial state if that input is seen there. You switch to another state which is equivalent to the initial state in the first automaton. That's why you demand that this input has to be initially given, but that is not required.
Assume now that we have another input, i.e., !(a&!b), i.e., we either have input b (with arbitrary a) or !a&!b.
- If b holds, the first automaton switches to the accepting state since then we have [a SU b] = true due to the above recursive law. The automaton then only demands that we continue with an infinite trace where any input can be given, since all what was needed was done to satisfy [a SU b].
- If !a&!b would hold, then [a SU b] = false and therefore the first automaton has no transition (which means that it cannot accept such a word). That is also the case in your automaton, but you also demand that after the first b occured which is not required.
Note that also the first automaton demands that there must be a point of time where b holds if we started with inputs a&!b for a while since the acceptance condition demands that eventually we have to switch to state q. Since that is only possible with input b, it implies that input b must be eventually there. If that happened, everything is done.
Another thing: if we have initially a&!b for a while, the `release' condition is just b and not !a&b as you suggested. It is allowed that at that point of time, we may also have a&b. And after that point of time, even everything is allowed, but there must be infinitely more inputs.
