4/20/2015 18 Basic CTL Formulas - cont 'd E F (g) –there exists a path which eventually contains a state in which g is true A F (g) –for all paths, eventually there is state in which g holds E F, A F are special case of E [f U g], A [f U g] –E F (g) = E [ true U g ], A F (g) = A [ true U g ] f U g (f until g) –true if there is a state in the path where g holds, and at every previous state f holds
{}