Fairness Property

I am struggling to understand the fairness property. I listened to the lecture but because the explanation contains the diagram drawn on board I am not able to understand its intuitive meaning that the professor has explained in the lecture. Can someone please explain. It would be really helpful.

+1 vote
It is difficult to answer that question without a context. If we speak about mu-calculus, then a fairness property is written as nu y. <>(mu x. (y&phi | <>x)) and denotes the set of states having an outgoing infinite path that visits states of phi infinitely often. Why that is so is not just explained on the black board, but also on slides 38-39 of the mu-calculus chapter.

Talking about omega-automata, we consider as acceptance condition GFphi which means that words are accepted by an existential nondeterministic omega-automaton if they have a run which visits infinitely often states in phi. That in turn can be checked by the mu-calculus property, and is written as GFphi, meaning that always (at any point of time), there must be a future point of time where phi holds. Thus, phi must hold infinitely often.
by (162k points)
Thank you so much