Omega automata to LO2

Question

For this question we are meant to convert the omega automata

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

 to LO2, can we just use the formula that was given in slide 25 of the predicate logic slides so the answer in LO2 would be

∃q,p. ΘLO2(0, !p&!q )∧ (∀t. ΘLO2(t, ϕR)) ∧ (∀t1.∃t2.t1 < t2 ∧ ΘLO2(t2, GFp ))

where ϕR = (Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q))

Answer 1

That formula is fine, but you need to negate it to get a universal quantification. The final answer should be 

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

Comments

The negation only applies to the first existential quantifier right ? In your answer the negation was only applied to the quantifier ∃ in ∃q,p.

---

Don't know what you mean. What I wanted to say is that the given formula A∀({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), GFp) may be first converted to ¬A∃({q, p}, ¬q ∧ ¬p,(Xq ↔ (¬q ∧ ¬a)) ∧ (Xp ↔ (¬p → q)), ¬GFp) so that you can apply the conversion to LO2 you mentioned. After that (it is not needed), you can drive in the negation and should get the formula I posted above.

---

when we had ΘLO2((Xq ↔ (¬q ∧ ¬a)), it was simplified to
(ΘLO2(Xq) ↔ ΘLO2((¬q ∧ ¬a)), is there a rule for this ?

---

Not really, but you can see that ΘLO2 leave propositional logic as it is, and just adds quantifiers, and applications to a time variable where needed.

---

oh okay, thanks