Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

915 questions

1k answers

1.4k comments

441 users

0 votes

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)

in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

+1 vote
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.
by (142k points)
Thank you for clarification :)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...