Local Model Checking

Question

Hi, I have a question regarding the following example:

I try to do local model checking, first for s4:

 

Why is s4 |- x1 wrong in this case?

I thought this would be a fixpoint since it's the same as vertex 0 and then it would be true if everything else is true.

Answer 1

Node 11 closes a loop to node 0. Hence, the function LoopCheck as defined on slide 105 is called. For µ, this is false. For nu, it'd be true.

Basically, the meaning of this closed loop is “state s4 is included if state s4 is included”. Since µ is the least, not the greatest fixpoint, we decide not to include s4.