Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

+1 vote
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?
in * TF "Emb. Sys. and Rob." by (420 points)
see also slide 27 in the µ-calculus chapter

1 Answer

+2 votes
Best answer

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.

by (166k points)
selected by
Thankyou for the clarification Professor.
Imprint | Privacy Policy