Content deleted Content added
No edit summary |
No edit summary |
||
Line 17:
A fair state is one from which atleast one fair path originates. The is translatable to, M<sub>f</sub>,s |= EGtrue <br />
==SCC based approach==
[http://en.wikipedia.org/wiki/Strongly_connected_component Strongly connected component] of a directed graph is a maximally connected graph - all the nodes are reachable from each other. A fair SCC is one that has an edge into atleast one node for each of the fair conditions.
<br /><br />
To check for fair EG for any formula - <br/>
1. Compute what is called the denotation of the formula. Basically all the states such that M, s |= formula. <br />
2. restrict the Model to the denotation. <br />
3. Find the fair SCC <br />
4. Obtain the union of all 3(above). <br />
5. Compute the states that can reach the union. <br/>
| |||