Local model checking

Question

I had attached the question and the solution of local model checking from a past paper. Doesn't local model checking fail as there is a mu and loop?

Could you please explain this answer

Comments

If image is unclear,  it is 2019\08\27 paper, Problem 4 a)

Answer 1

The local model checking tree has a loop on nodes 4->5->6->7->8->9->4 where nodes 4 and 7 contain fixpoint formulas with a greatest fixpoint. The outermost fixpoint of the loop does therefore not cover a least fixpoint formula (in that case it would be false), but a greatest one, so it is true.

Don't be confused; the mentioned greatest fixpoint is contained in a least fixpoint that is found in nodes 1 and 15. The nodes 1 and 15 expose the greatest fixpoints in nodes 4 and 7, but neither node 1 nor node 15 is on the mentioned loop.

Comments

Is there a order of precedence that needs to be followed while splitting the equation?

---

Well, we have to follow the syntax tree to decompose the formula, and this determines an ordering.