Fair computational tree logic is conventional computational tree logic studied with explicit fairness constraints.
This declares conditions such as all processes execute infinitely often. If you consider the processes to be Pi, then the condition becomes:
wedgeGFPi
Here, if a process is requesting a resource infinitely often (R), it should be allowed to get the resource (C) infinitely often:
wedge(GFR\longrightarrowGFC)
Consider a Kripke model with set of states F. A path
\pi=so,s1...
1. Mf, si |= A
\phi
\phi
2. Mf, si |= E
\phi
\phi
A fair state is one from which at least one fair path originates. This translates to Mf, s |= EGtrue.
A strongly connected component (SCC) of a directed graph is a maximal strongly connected subgraph—all the nodes are reachable from each other. A fair SCC is one that has an edge into at least one node for each of the fair conditions.
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 .([φ] ∩Fi ∈FT [EX[E(Z U(Z ∧ Fi))]), which means the formula holds in the current state and the next states and the next to next states until it meets all the members of the fair conditions. This means that, the condition is equivalent to a sort of accepting point where the accepting condition is the entire set of Fair conditions.