Fair computational tree logic

Fair computational tree logic is conventional computational tree logic studied with explicit fairness constraints.

If you consider the processes to be Pi, then the condition becomes: Here, if a process is requesting a resource infinitely often (R), it should be allowed to get the resource (C) infinitely often: Consider a Kripke model with set of states F. A path

To check for fair EG for any formula, The fix point characterization of Exist Globally is given by: [EGφ] = νZ .

([φ] ∩ [EXZ ]), which is basically the limit applied according to Kleene's theorem.

To fair paths, it becomes [Ef Gφ] = νZ .