omega automaton

Question

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)

Answer 1

To translate [a SU b] to an equivalent F-automaton, you may note that [a SU b] holds if we have a&!b for a some finite time until b holds at some time. This leads to the automaton shown on page 69 of VRS-07-TemporalLogic which is a F-automaton. It is not deterministic, since some transitions are missing, but if these are added (leading to an additional sink state), you got your automaton.

Note, however, that this automaton is only equivalent to [a SU b] at the initial point of time and also until the first point of time where b holds, but no afterwards. If you want an automaton that is always equivalent to [a SU b], then you need a GF-automaton.