Doubts in Global Model Checking (Exercise Sheet 6)

Question

I am constructing my understanding based on lecture video by using exercise sheet 6, then I have faced with some doubts. 

Kindly someone assist to clarify on below in exercise sheet 6:

 1. Slide 8, pre s5, s6 should not be as above red highlighted? if not please you may elaborate why?

 2. Based on same Kripke Structure, what is universal predecessors of y? I think it should be empty because based on table none of states do not satisfy y={s3,s8}? unless if we can say {} also can consider in this case, is it?

Thanks in advance.

Answer 1

For your first question yes you are right the successors for s5 and s6 should be switched.

Answer 2

1. The first doubt is just a typo / attention test. You passed the attention test! Congratulations, and thanks for reporting this!
2. The states s3 and s8 satisfy y = {s3, s8}. Besides that, the box operator is a universal quantifier. As s3 and s8 have no successors, it is trivially true that all their successors satisfy any property. That's why they are included in any result of the box operator.

Comments

Thanks for your clarification!

2. Just for more clarification on my side, can we include all states that either their predecessors / successors are empty set {} for all modal operator?

Thank you.

---

Not for all modal operations but for the universal modal operators, yes.

Recall that []phi holds in a state if that state either (1) has no successors or (2) if all of its successor states satisfy phi. Analogously, [:]phi holds in a state if that state either (1) has no predecessors or (2) if all of its predecessor states satisfy phi.

So, for the universal formulas []phi and [:]phi, states with no successors and no predecessors have to be added, respectively.

---

Noted with Thanks.