Temporal logic formulas can often be better understood when these are translated to deterministic automata. F[a SU b] cannot be translated to Det-G but to Det-F. However, if you use the standard translation, you will get two GF-constraints, However, determinizing Büchi automata is very difficult.

Hence, we use the following workaround: We translate !F[a SU b] to a NDet-G automaton, determinize it to a Det-G automaton, and negate it to get a Det-F automaton equivalent to F[a SU b].