Hi,

I have a doubt regarding LTL to omega automaton,

[a SU b] to and F-automaton.

Since, we don't have direct formula for [a SU b] to F automaton, I have taken the negation of [a SU b] to a G automaton, then from there I reduced to a F automaton, But something went wrong in-between, got stuck here. Could you please help me to solve this?

but the answer for this one is , [a U b] = Aexist ({q}, ¬q, ¬q ^ a ^ ¬b ^ ¬q0 | (q | b) ^ q0 , Fq)