I have a doubt regarding conversion to LO2. In this question :

**A∀({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp)**, the automaton is given as universal quantified.

which can be converted to Existential quantified by negation,

A∀({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp) = ! A∃ ({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp)

can we represent it like this?

**!∃ p,q. ¬q[0] ∧ ¬p[0] ∧ ∀t. (q[t+1] ↔ (¬q[t] ∧ ¬a[t])) ∧ (p[t+1] ↔ (¬p[t] → q[t])) → ∀t1.∃t2. t1<t2 ∧ p[t2]**

**It will be converted to :**

∀**p,q. ¬q[0] ∧ ¬p[0] ∧ ∀t. (q[t+1] ↔ (¬q[t] ∧ ¬a[t])) ∧ (p[t+1] ↔ (¬p[t] → q[t])) → ∀t1.∃t2. t1<t2 ∧ p[t2]) **

OR

Taking negation to inside, so it will change the Acceptance state. Like this :

! A∃ ({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp) = A∃ ({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), !GFp) = A∃ ({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), FG!p)

**(∃ p,q. ¬q[0] ∧ ¬p[0] ∧ ∀t. (q[t+1] ↔ (¬q[t] ∧ ¬a[t])) ∧ (p[t+1] ↔ (¬p[t] → q[t])) → ∀t1.∃t2. t1<t2 ∧ !p[t2])**

I am not sure which method I have to take. Since, on slide number 25 (Predicate Logic), the automaton is given as Buchi (GF), and this LO2 is given as: ∃q1 . . . qn. ΘLO2(0, ϕI )∧ (∀t. ΘLO2(t, ϕR)) ∧ (∀t1.∃t2.t1 < t2 ∧ ΘLO2(t2, ϕF ))

Is it only applicable to Buchi automaton? And which approach do we have to take to solve this question? Kindly please clarify the above.