Fair computational tree logic: Difference between revisions

Revision as of 16:04, 26 January 2007

Revision as of 16:07, 26 January 2007

Line 30:

==Emersion Lei Algorithm==

The fix point characterization of Exist Globally is given by:-

[EGφ] = νZ .([φ] ∩ [EXZ ]) , which is basically the limit applied according to Kleene's theorem. <br/>

To fair paths, it becomes - <br/>

[Ef Gφ] = νZ .([φ] ∩_{Fi ∈FT} [EX[E(Z U(Z ∧ Fi ))])

[EGφ] = νZ .([φ] ∩ [EXZ ])

==References==