LTL Model checking

Question

I have a doubt regarding LTL model checking. Why [a SU a] is neglected? I read that, we can neglect the positive occurrence of WU and the negative occurrence of SU. I am not sure about what it's meant by positive occurrence and negative occurrence. Could you please clarify?

As per the syntactic sugar,

q0<->[a SU a]

Φ[ϕ SU ψ]x ⇔ A∃ ({q}, 1, q ↔ ψ ∨ ϕ ∧ Xq, Φqx ∧ GF[q → ψ]) ,

but how did it become GF(¬q0 → a) instead of GF(q0 → a)?

Answer 1

Positive and negative occurrences essentially means under an even and odd number of negations, i.e., in !a&b|!(!c&d) the variables a and d have negative occurrences while b and c have positive ones.

Comments

Okay...in this [b SU Ga], can I write Ga to ![true SU !a] and it's a negative occurrence of SU. So that I'm ignoring it. Therefore remaining acceptance condition will be [b SU q0], which is a positive occurrence of SU. Then it will be GF[q2->q0] but in the slide, it is given as GF(q → p) ∧ GF(a → p). Is it valid?