General question about model checking in exam

Question

Hello,

If in the exam there is a question like the append one, is it necessary to compute the state set by means of global model checking with translating it to mu-calculus or would it be enough if we just determine the states without formal computation and explain why those states are chosen?

Thanks in advance!

Edit [Attached picture]

Answer 1

It depends on the precise question. If the exercise demands that you shall compute those states by local/global model-checking, then you have do so to get your points. However, if it only asks which states satisfy that formula, you are free to determine those states and to explain why that is so. That explanation may be given in your own words, but should be really an explanation for the statement made.

Comments

Sorry, I forgot to attach the picture.

So in this case, would be the following answer sufficient enough?:
The inner Property EGa is satisfied by the sequence s2->s3-s6->s2->... So for the outer property EF there must be a path were eventually one of the states s2,s3,s6 could be reached, which is possible for the states s5(s5->s2), s0(so->s5), s1(s0->s5),s5(s0->s5). So the state set is given by: {s0,s1;s4;s5;s2;s6;s3}

---

sounds good to me