Content deleted Content added
No edit summary |
No edit summary |
||
Line 7:
Here, if a process is requesting a resource infinitely often (T), it should be allowed to get the resource (C)infinitely often <br />
<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<sub>f</sub>,s<sub>i</sub> |= A<math>\phi</math> if and only if <math>\phi</math> holds in ALL fair paths. <br/>
2. M<sub>f</sub>,s<sub>i</sub> |= E<math>\phi</math> if and only if <math>\phi</math> holds in one ore more fair paths. <br/>
==References==
| |||