s5 has three successors in the structure: s0, s2 and s4 (which you also see in the tree).

The "<>" operator talks about the **existential** predecessors, so node 12 in the tree argues about:

"Tree-Node 12 holds if there **exists** a node satisfying x2 of which s5 is a predecessor"

As the node s2 satisfies x2 (as a & !b holds there), this condition is fulfilled; so regardless of what happens with the nodes s0 and s4, tree-node 12 does hold due to tree-node 20. In local model checking, the "<>" operator acts as a disjunction, so if one of the tree-nodes below satisfies the property, the node with the "<>" is also satisfied.

In contrast to that "[]" acts as a conjunction, so in this case if one of tree-nodes below does not satisfy the property then the node with "[]" also does not hold.