FG automaton

Question

Here, we have to create a FG automaton, 

[a SU b] = Aexists({q},1, q<->b|a&next(q), q & FG!q) , can we use this formula to solve it? I am not sure how the !q came as the initial state? 

Answer 1

The equivalence [a SU b] = Aexists({q},1, q<->b|a&next(q), q & FG!q) is not valid: Look, for all points of time, you may have a=0, b=1 and q=1. Then,  [a SU b] is always true, but this is not an accepting run of the automaton on the right hand side. Why do you think that the two formulas are equivalent?

Comments

We need to convert [a SU b] to FG automaton, but in that Temporal logic chapter slide 115 has the formula for SU to a FG automaton. Then how can i convert [a SU b] to a FG automaton?

---

Check slide 115: [a SU b] = Aexists({q},q, q->b|a&next(q), FG!q). Note that this is not valid for <-> in the transition relation but it does hold for -> as explained in the lecture notes. The remaining formula, in the above case q, is then the set of initial states.

---

[a SU b] = Aexists({q},q, q->b|a&next(q), FG!q), but in the solution the it's given as initial state as !q and acceptance state as FGq . How !q came to initial state and what about FG!q?

---

The solution is a different automaton, yes. It has other transitions and initial states, but that may still be equivalent to [a SU b]. It is not the case that there is a unique automaton.

---

Thanks for the clarification, i understood it.