Incorrect Answer.
The state s0 in the CTL model below satisfies EF p,
since "the future includes the present", but not EG p. Thus, these formulas are not equivalent.
- (Does one of them "entail" the other, though?)
- (Can you adapt this model in case that "the future excluded the present"?)
Back to Question.
Next Question.