Global Model Checking explain box(x) and implication output

Question

there must be error in box (x) output? Also explain how implication is computed here.

Answer 1

Where exactly do you see an error here?

And the implication is done like one would except, so if you have two state sets A and B and you want to compute States(A -> B) then the result is:

B U (S \ A)   with S being the complete state set S := {s₀, ..., s₇}

So state s_i is part of States(A -> B) if either s_i is part of set B or s_i is not part of set A. Or you can put it like that:

If a state s_i is part of set A then it must be also part of set B. If this condition holds true, then s_i is also element of States(A -> B) otherwise it isn't.

Comments

Thanks for the response.

How could universal predecessors of x be all states in step 0?

---

This is because you calculate the greatest fixpoint via a "nu" operator instead of a "mu" operator (which calculates the least fixpoint). Thus you need to start with the whole state set.

---

I think you mis-understood my question. I know that x will be initialised with all the states due to nu operator.

My question is how States([]x) = {s0;...;s7}?

How universal predecessor of x could be all the states, Please elaborate that part.

---

The reason for that is simply that x contains all states, thus all transitions do of course point to some state in {s0,...,s7} i.e. there is no state that has a transition that does not point into that set (as there are no other states outside this set). Also see page 56 in chapter 4 in that regard: pre_{universal}(S) = S