Fairness Property

A fairness property expresses that, under certain conditions, something will occur infinitely often, i.e. there is no last state, in which a certain property P will not hold. Equivalent descriptions are repeated reachability and repeated liveness. Problem: fairness properties cannot be expressed in pure CTL. Appropriate extensions of CTL are called CTL+fairness. One example for this is the extended logic fair CTL written as FCTL.

If one would have defined the additional operators $F^{\infty}$ ('an infinite number of times') or the dual operator $G^{\infty}$, one could express propositions like

1. AF $^{\infty} \phi$
2. EF $^{\infty} \phi$
3. A(F $^{\infty} 1 \wedge$ F $^{\infty} 2 \wedge$F $^{\infty} 3 \wedge$F $^{\infty} 4 \wedge$F $^{\infty} 5 \wedge$F $^{\infty} 6$)