Local Model Checking when Global Model Checking does not hold

Question

Do we need to perform local model checking (show the steps by drawing the tree structured) when global model checking has already failed? Or can we just say(write a statement) that Local model checking will not hold as global model checking does not hold?

In either case, is my understanding right that if global model checking does not hold true then local model checking will also definitely not hold true, all the time?

Answer 1

Local and global model checking are two algorithms that solve the same problem. Hence, if one of the two already gives us an answer, then that answer is the answer, and there is no need to re-check this with the alternative algorithm.

However, while that is true from a practical point of view, it still makes sense to ask for both in exam papers. Clearly, the answers for the two algorithms should also there be the same, but we just want to see that you are able to answer the same problem with the different approaches.

Note also that global model checking computes ALL states satisfying a property, while with local model checking, we are just checking that ONE state satisfies a property, which makes the two approaches a bit different.

Comments

So even if global model checking holds, we have to work it out(show the steps in the tree structure) for local model checking?

---

If the task is to check by means of local or global model checking whether a property holds in a  states, yes, then you have to apply the algorithm, regardless whether you already know that it does or does not hold. Sometimes there are exercises, where you are asked to check (without mentioning an algorithm) that a property holds. In that case you can argue in any reasonable way.