Local model checking [ 02-2019 5a]

Question

In local model checking, for mu x., if there are loops in the tree, it does not hold, right? 

For this question, when I draw the tree, 

there is a loop and since it is mu x, I concluded that S1 does not hold. but why does it hold?

Answer 1

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.

Comments

Ah! okay! so in the exam do we still need to check further even after we get a loop?

---

Well if its a disjunctive node (like tree-node 12 in this case) and the loop evaluates to 0 then you need to check further if all the other succesors of the disjunctive node are also 0. If any of those nodes is 1 however, you don't need to check further as you already know the result (which is then 1). In this specific example the loop in tree-node 19 evaluates to 0 so you need to check further. As tree-node 20 evaluates to 1, you don't need to check tree-node 13 afterwards as the result is already determined.

Answer 2

If a proof goal s|-phi is generated for a mu-formula phi such that this goal already appeared before, then we can conclude that phi does not hold on that state s. However, as Daniel pointed out, it may still hold on a predecessor of s like s5 if there are other disjunctive subgoals that may satisfy the formula (as it is the case in the example).

Comments

Understood! thank you!!