Local Model Checking query

Question

In local model checking, we have to check for every s belongs to Initial states set.

So If there is two initial state in a Kripke structure namely s0 and s5, then lets say I start checking from s0 and it didn't satisfy, then we need to check again for s5 from starting as well.

Is there any strategy to choose initial state ? or we have to choose randomly and then check ?

Answer 1

If s0 does not satisfy the formula, there is no need to check also s5, since then you already know that not all initial states are satisfying the formula. But your question is rather that one of the two states does not satisfy the formula and you would like to check only that one. There is no good heuristic for a computer, but as a human, you may understand what the formula's meaning is and if you then can say which states satisfy it or not, then you know how to proceed.

Comments

Thanks for the explanation.

Just a follow up question.
So if a question asks to "check whether K |= Si holds using local model checking" and in its Kripke there are two initial states s0 and s1, and I have checked with s0 and it satisfies the given formula, so I have to check s1 also in that case, is it right ?

---

Yes, you have. Since, in that case K|=phi means that K,s0|=phi and K,s1|=phi holds, and therefore if K,s0|=phi is true, then K|=phi means that K,s1|=phi holds. Hence, to answer whether K|=phi holds, you have to also check K,s1|=phi in this case.

---

Now it is clear.
Thank you for the explanation and quick response.