Content deleted Content added
→Strong fairness / compassion: changed T to R |
typo - emersion to emerson |
||
Line 26:
# Compute the states that can reach the union.
==
The fix point characterization of Exist Globally is given by: [EGφ] = νZ .([φ] ∩ [EXZ ]) , which is basically the limit applied according to Kleene's theorem. To fair paths, it becomes [Ef Gφ] = νZ .([φ] ∩<sub>Fi ∈FT</sub> [EX[E(Z U(Z ∧ Fi ))]) which means the formula holds in the current state and the next states and the next to next states until it meets all the members of the fair conditions. This means that, the condition is equivalent to a sort of accepting point where the accepting condition is the entire set of Fair conditions.
| |||