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