Omega automaton to LO2

Question

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.

Answer 1

There is not really a need to convert the automaton to an existential one, but if so, you should not forget about negating the acceptance condtion, i.e.,

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

Then, you could proceed as follows (there was a mistake in your solution):

    !∃ 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]

which is already LO2, but if we want to push the negation inwards, we get

    ∀ 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]

You could directly write down the above from the initial formula. 

Comments

I understood the idea. But I have a small question ,why "!∀t1.∃t2. t1<t2 ∧ p[t2]" this part didn't change the quantifier? Usually, if we negate the quantifier,  it will change the quantifier(ex to uni or uni to ex). But why it did not change here?

---

Well, if we drive in the negation, it will change the quantifier, but the acceptance condition was !GFp and since GFp is equivalent to ∀t1.∃t2. t1<t2 ∧ p[t2], I just wrote the negation of the latter (since we will negate it again soon).

---

Note that A∀(Q, I, R, phi) =  ¬A∃(Q, I, R, ¬phi)

---

Thanks for clarifying the doubt.