Well, there are many ways how to solve that exercise. The task was to generate an automaton that is equivalent to [a SU b] with an acceptance condition of the form Fq. Following the semantics of [a SU b], it holds if there is a point of time where b holds and until then a must hold. Thus, we may start in a state {} with a self-loop for a&!b and a transition to state {q} when b holds. Clearly, we have to reach state {q}. There is no transition for !a&!b in state {} since then [a SU b] would be false, so that transition is missing intentionally. Once reached state {q}, nothing else has to be demanded, but we must consume further inputs which are don't cares. Hence, there is a self-loop on {q} for any input.
We can now write down the transitions as single midterms
- ¬q & a & ¬b & ¬q'
- ¬q & b & q'
- q & q'
The disjunction of these yields the above transition relation.
