# G automaton to F automaton

I have a doubt regarding this, I want to convert [a SU b] to a F-automaton. Since, we don't have the direct relation, I have converted [a SU b] to ![a SU b] , which is a G-automaton. I am not sure , what i have done is correct. Could you please help on this? I got stuck here. I think , i need to determinize this then take the negation of the Acceptance State.

Also, if it's a safety automaton all states are accepted , is that correct ? ( i have added some shades inside the states)

+1 vote

What you have done makes sense to me.

![a SU b] = Aexists({q},!q, q<->b|a&next(q),G true)

We have two states {} and {q}, both are accepting (safe) states, and {} is the single initial state. We then have to determinize it with the subset construction so that we can then negate it again to obtain a DetF automaton for [a SU b].
by (166k points)
selected by
Aexists({q},!q, q<->b|a&next(q),G true) , can we use implies instead of the equivalence ? It's mentioned that we can use equivalence instead of implies, if i use implies is it correct ?
Yes, you can do that as shown on page 115 and page 116.
Thanks for the clarification.