G automaton to F automaton

Question

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)

Answer 1

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].

Comments

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.