Exam specific question aboud local model checking

Question

Hello,

Given the following Kripke structure:

Would the following solution be enough or is it too much abbreviated?

Thanks in advance!

Answer 1

I think it is too much abbreviated; e.g., the subgoal s5 |- a|b should be further decomposed to justify that a|b does really not hold on s5. 

The [:] operator (box with arrow on top) needs to check the predecessors; hence, s5 |- [:] x should check for s0 |- x instead of checking s6. Hence, the real solution looks like this (and I think that these steps are really needed):

Comments

Oh, that was a fault of mine. Assume it would have been mu x.((a|b)&[]x).
The reason i am asking is that I want to know if we can skip steps like 5 and 6 in the real solution?

---

You shouldn't do that; these steps do also have a meaning and reasoning behind. Look, step 6 is one that is new; now we check the entire formula on state s0, while before the question was to check in on state s5. It's therefore not a "have already seen this" (like from node 11 to 0).

What you can skip are paths that are not needed, e.g., in a disjunctive branching which is true, you only need one path to prove this, and in a conjunctive branching, you only need one branch to disprove it. The rest is needed, I would say.

---

Okay. Thank you.

---

Can I know, why did you consider s0 when s5 has 3 predecessors -s0,s4,s6.

---

We have to check whether s5 satisfies the property, and we found out by checking one of the predecessors, namely s0, that it is not the case. Hence, there is no need to check the other predecessors, and we stopped. We could have also chosen one of the other predecessor states s4 or s6 and we would have found that the property is also false there. But that is not needed. Picking one of them is sufficient, and the choice of s4 was arbitrary. Choosing s6 would have been more work, but s4 would be equally good.