Local Model Checking: This question solution is a bit confusing

Question

Is Local modelling solution unique? Like in my solution I have given precedence to & operator so I splitted on (a |b) and (diamond of x) but the given solution do otherwise? can both be the solutions of only the provided one is correct? If only provided one is correct then isn't it contradicting operator precedence?

Answer 1

The solution of local model checking is not unique, since there are AND and OR rules. For the OR rules, it is sufficient to choose one subgoal for proving the formula, and for the AND rules it is sufficient to choose one subgoal for disproving the formula. Depending on these choices, we may get different solutions. Apart from that, you may also choose one of the initial states to disprove the formula.

Comments

Thanks for explanation. As you have pointed out the precedence of operators in another post, here I wonder why OR has been evaluated in the given solution first? Should'nt be (a |b) AND (diamond of x)?

---

No, since AND binds stronger than OR, we have the formula nu x.(a|(b&<>x)).