Local Modal checking

Question

According to this sample solution the property does not hold, but my solution shows it holds. 

 

So what could be the mistake in my solution? 

Answer 1

You continued in s5 with the diamond operator, but that one has been removed by the rule before. Instead, it should have been a box operator there. And then, the property must also be shown in the other successor states of s5, but it does not hold in state s0:

Comments

Why haven't we taken s4 as the successor of s5 instead of s0?

---

We have to check all the successors of s5, and started with s0. Since that already failed, there was no reason to continue with the other successor states.

---

So if box operator is there we have to check for all the successors and if there would be a diamond operator (just for assumption) we can check just one successor?

---

Right, that is explained  in detail on the slides and in the video.

---

Thank you, i got it now