Omega Automata Feb 2019 Exam paper

Question

A question had been asked in the Feb 2019 exam paper to transform FGa∧G¬b into an Lω formula with Co-Büchi (FG) acceptance condition. It said the acceptance condition of the NDetF automaton obtained in the previous question can be modified to FG without changing its meaning: FGa =A∃ ({p}, ¬p, p → a ∧ p', FGp). I am not sure how FGa = A∃ ({p}, ¬p, p → a ∧ p', Fp)  obtained in the previous question has been transformed to FGa =A∃ ({p}, ¬p, p → a ∧ p', FGp) without changing its meaning. Is it because the acceptance condition does not matter here?

Answer 1

Have a look at the automaton with initial condition !p and transition relation p → a ∧ p':

Hence, we may either loop forever in the initial state or once we switched to state s1, we are only able to continue with reading input a, so !a can no longer be read. The first acceptance condition is Fp which means that at some time we have to switch to p, and looking at the automaton, we cannot leave from s1:{p} any more. Hence, saying FGp, which means that after some time, we are only in state s1:{p} is no different to saying Fp in this case. So, in this case (not in general), the acceptance conditions Fp and FGp (and also GFp) are equivalent.