CTL*
CTL vs. LTL
Model checking
Symbolic Model Checking
Kripke Structure: M = (S,R,L)
- transform a FSM with guarded transition to M, by modeling original transitions as states in M
you can unroll M to get an execution tree
formulas and logic:
- Ef, Af
- Xf, Ff, Gf, fUg
-
No comments:
Post a Comment