Global model checking

Question

what is the exact way of calculating <>X and []X in Global model checking?. As far as i Know in both cases we need to look into the successor and check if it is in our previous X. But how come there is S1 in this particular problem and also what will be the []X in this problem?..

Answer 1

A definition of the existential and universal predecessor states is as follows:

    pre∃(Q2) := {s1 ∈ S | suc(s1) ∩ Q2 != {}} 
    pre∀(Q2) := {s1 ∈ S | suc(s1) ⊆ Q2}

and you know that the semantics of <> is pre∃ and that of [] is pre∀.

Hence, s1 must be in pre∃({s0,s2,s3,s4,s5,s6,s7}) since it must contain all those states s1 where we have suc(s1) ∩ Q2 != {}, i.e., that have at least one successor in Q2={s0,s2,s3,s4,s5,s6,s7}. Obviously, we have suc(s1) = {s5}∈Q2={s0,s2,s3,s4,s5,s6,s7}, and thus s1∈pre∃(Q2).

For pre∀({s0,s2,s3,s4,s5,s6,s7}) we should compute those states where all successor states are in {s0,s2,s3,s4,s5,s6,s7}, i.e., pre∀({s0,s2,s3,s4,s5,s6,s7}) = {s0,s1,s3,s4,s5,s6,s7}.

Comments

ok, It makes sense now.one more thing, while solving these problem we need to check for each states whether succ(S) ^ X !={} holds,not only the state inside in X . am i right?.Also <>[{}] = {},[]({})  = deadend  and [](deadend) = deadend and <>deadend = {} . right?

---

Well, as we have for example to compute {s1 ∈ S | suc(s1) ⊆ Q2} for a given set of states Q2, you have to check for all states s1∈ S whether suc(s1) ⊆ Q2 holds. If so, s1 belongs to the set, otherwise not. So, it does not depend on Q2, you have to check for all states s1 ∈ S whether they belong to the set or not (following the definition).

---

could you please explain the meaning of <:> and [:]?

---

<:> phi is the set existential successor states of the states that satisfy phi, and [:] is the set of universal successor states of the states that satisfy phi. Hence these operations are the ASCII version of the modal operators that are the diamond and box operators with an arrow on top on the slides.

---

Got it professor. Thanks