Incorrect Answer.
The state s0 in the CTL model below satisfies A[p U T] but not AF p.
(You should be able to explain why this is so.)
Since "the future includes the present", A[p U T] is true at any state in
any model. (Why?)
Back to Question.
Next Question.