# Omega automata to LO2

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))

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

```∀p,q.
¬q ∧ ¬p ∧
∀t. (q[t+1] ↔ (¬q[t] ∧ ¬a[t])) ∧
(p[t+1] ↔ (¬p[t] → q[t]))
→ ∀t1.∃t2. t1<t2 ∧ p[t2]
```
by (117k points)
selected
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