Exam Paper: 2019.02.13 : Question 6b : omega Automata

Question

Can you please explain the below question? How do we get 'true' in the G(!b) formula here? 

Thank You!

Answer 1

An existential automaton demands that there must be an infinite run that fulfills the acceptance condition. If the acceptance condition is a safety condition, you can always put that into the transition relation which yields then the simple acceptance condition "true". Formally,

Aexists(Q,I,R,Gphi) = Aexists(Q,I,R&phi,true)

In the above case, the transition relation q&!b&q' was used with the initial state q. That means the automaton has only the state {q} with a self-loop that is only enabled if b is false. Hence, all infinite runs are those where b is always false, and therefore nothing else than the existence of such a run is needed.

Comments

Thank you! now I understood the G(!b). There is another doubt- please explain, In FGa, why have we written acceptance condition Fp to FGp directly?

---

If you consider the transition relation of that automaton, i.e., p -> a & p', you can see with the state transitions that in the initial state {}, you may either stay or leave to state {p} for any inputs. However, once you are in state {p} the only further transitions possible are those with a self-loop on {p} where input a has to be true.  Hence, switching once to {p} with Fp or remaining there forever with FGp is the same due to the special transition relation. Both Fp and FGp demand that we cannot remain in the initial state {} forever, and leaving it has then the same consequence.

---

yes, now I understood. Thank you very much.