Content deleted Content added
m →Emerson Lei algorithm: Typo fixing, typos fixed: , → , using AWB |
|||
Line 14:
==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 =
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:
|