Fairness assumption
= 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}}\varphi$ 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.