2020.Feb exam paper

Question

https://es.cs.uni-kl.de/teaching/vrs/exams/2020.02.19.vrs/2020.02.19.vrs.solutions.pdf

Qustion 4 (d) part - I understand EGa,

but for AF why s2 is satisfied? 

because 2 paths start from s2. The one looping in s2-s3-s4 is satisfying AF property but for other path going from s2 to s1 why is it satisfying? Because AF says on all paths and I can take path s2-s1-s5-s4-s5-s4 and loop in there only, then it wont satisfy AF. If we say there should be atleast one path because of EF property, that's we are considering s2, then my doubt is how s4-s5 is counter example? Because for s5 there are two paths to s4 and s2. we can say on all paths eventually there exists one path where globally a is true (s5 -s4-s5-s4-s2-s3-s4-s2-s3-s4 and so on)

Answer 1

EGa is true at states {s2;s3;s6}, thus AFEGa must include these states at least since all paths starting there already have reached the set EGa={s2;s3;s6} at the initial point of time. Note that Fp holds if p holds now or at any time in the future. The present time is included.

Comments

Thank you for clarification :)