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)$

Model checking for fair CTL

If you consider a Kripke Model, the fair Kripke Model has a set of States F. A path $\pi =so,s1\dots$ is considered a fair path, if and only if the path includes all members of F infinitely often.
Fair CTL model checking restricts the checks to only fair paths. There are two kinds:
1. M_f,s_i |= A$\phi$ if and only if $\phi$ holds in ALL fair paths.
2. M_f,s_i |= E$\phi$ if and only if $\phi$ holds in one ore more fair paths.

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)