Fair computational tree logic

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

Weak fairness / Justice

This declares conditions such as all processes are executing infinite often. If you consider the processes to be P_i, then the condition becomes
$\bigwedge GFP_{i}$

Strong fairness / Compassion

Here, if a process is requesting a resource infinitely often (T), it should be allowed to get the resource (C)infinitely often
$\bigwedge (GFR\longrightarrow GFC$

References

• Emerson, E. A. and Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24.{{cite journal}}: CS1 maint: multiple names: authors list (link)

• Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263.{{cite journal}}: CS1 maint: multiple names: authors list (link)