Fairness assumption

A condition selecting admissible infinite paths in a transition system, often to exclude executions that postpone an enabled activity forever. The notation $TS{\models }_{\mathrm{fair}}\phi$ quantifies only over initial paths in a transition system satisfying the chosen condition. For example, $GFp$ requires $p$ infinitely often, while $FGp$ requires $p$ permanently from some point onwards. Neither condition implies the other.