Doubt in CTL*,CTL and LTL exam question

Question

I am solving exam question 31.08.2021 : Q 7 (d) : 2021.08.31.vrs.solutions.pdf (uni-kl.de)

I understood about AFGa like in every path eventually globally "a" holds which is satisfied in both infinite paths.

Infinite Paths :

P1 = s0 -> s1 -> s1 -> ......

P2 = s0 -> s1 -> ... s1 -> s2 -> s3 -> s3 .....

But I have some problem in understanding AFAGa

Why it holds in only s2 & s3 and why not in s0 and s1 ?

As far as I understood in every path eventually in all path globally "a" holds so if we take P1 it holds and if we take another path P2 it also holds.

Could you please explain about this ?

Answer 1

AF AG a is best understood by decomposing into two problems: First compute the set of states phi=AGa which is only state s3. Now, you can consider AF s3, i.e., the states where all outgoing infinite paths eventually reach s3. The state s0 does not satisfy this, since you can loop infinitely often in s1, and for the same reason, it does not hold in s1. AF s3 only holds in states s2 and s3.

Assume the Kripke structure would be labeled such that only state s3 would be labeled with a variable p, and you would consider AF p. Would you then also think that states s0 and s1 would satisfy that formula?

Comments

Now I understood your explanation.
The way you explained by breaking it into subproblems is really good and can be understandable really well.
I will apply this technique of decomposing in future.

"Would you then also think that states s0 and s1 would satisfy that formula?"
-> No then it will not be satisfied by s0 and s1 because there is an infinite path which doesn't satisfy Fp.

---

Right, for CTL, people typically make the mistake to consider an interference of the temporal operators in time that is no there (in contrast to LTL). It is best to consider each CTL operator pair as the definition of a new set of states to avoid that kind of interference.

---

Yes exactly and thanks a lot :)