Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
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?
in * TF "Emb. Sys. and Rob." by (200 points)

1 Answer

0 votes
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.
by (170k points)
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.
Imprint | Privacy Policy
...