# Omega automaton to LO2

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 ∧ ¬p ∧ ∀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 ∧ ¬p ∧ ∀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 ∧ ¬p ∧ ∀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.

+1 vote

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∧¬p ∧
(∀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∧¬p ∧
(∀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.

by (143k points)
selected
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.