What do we mean by Positive and Negative occurrences of weak or strong until?

Question

In LTL Model Checking while converting the LTL formula to an equivalent ω-automaton, we can neglect the fairness constraint in acceptance conditions for positive occurrences of [ϕ U ψ] we can neglect the fairness constraint for negative occurrences of [ϕ U ψ].

What do we mean by positive and negative occurrences here?

Comments

see also slide 27 in the µ-calculus chapter

Answer 1

If you just consider ¬,∧, and ∨ as operators for propositional logic, then an occurrence of a subformula is called positive if it appears under an even number of negation operators ¬. For example, in a∧¬(b∨¬c), the occurrences of a and c are positive since they occur behind 0 and 2 negation operations (which are both even numbers) while the occurrence of b is negative since it occurs after 1, i.e. and odd number of negation operators. For temporal logic the B-operators contain a nasty difficulty in that [x B y] the occurrence of x has to be counted like a negation since [φ B ψ] := [(¬ψ) U (φ ∧ ¬ψ)] and therefore the occurence of ψ is behind another negation operation. Analogously, if you also consider implication (x → y) the occurrence of x adds another negation since implication is defined as (x → y) := ¬x∨y.

Comments

Thankyou for the clarification Professor.