Fair computational tree logic: Difference between revisions

Revision as of 19:02, 31 January 2011

Revision as of 16:22, 14 June 2011

Line 4:

==Weak fairness / justice==

This declares conditions such as all processes are executing infinitely often. If you consider the processes to be P_i, then the condition becomes:

:<math>\bigwedge GFP_{i}</math>

==Strong fairness / compassion==

Here, if a process is requesting a resource infinitely often (R), it should be allowed to get the resource (C) infinitely often:

:<math>\bigwedge( GFR \longrightarrow GFC)</math>

==Model checking for fair CTL==

If you consider a Kripke Model, the fair Kripke Model has a set of States F. A path <math>\pi = so, s1 \dots</math> is considered a fair path, if and

only if the path includes all members of F infinitely often. <br/>

Fair CTL model checking restricts the checks to only fair paths. There are two kinds: <br/>

1. M_f,s_i |= A<math>\phi</math> if and only if <math>\phi</math> holds in ALL fair paths. <br/>

2. M_f,s_i |= E<math>\phi</math> if and only if <math>\phi</math> holds in one ore more fair paths. <br/>

:1. M_f,s_i |= A<math>\phi</math> if and only if <math>\phi</math> holds in ALL fair paths. <br/>

A fair state is one from which at least one fair path originates. The is translatable to, M_f,s |= EGtrue <br />

: 2. M_f,s_i |= E<math>\phi</math> if and only if <math>\phi</math> holds in one ore more fair paths. <br/>

A fair state is one from which at least one fair path originates. The is translatable to, M_f,s |= EGtrue <br />

==SCC-based approach==

Line 22 ⟶ 28:

To check for fair EG for any formula,

# Compute what is called the ''denotation'' of the formula. Basically all the states such that M, s |= formula.

# restrict the model to the denotation.