Global Model Checking

Question

Referring to the following table (given labels and its Predecessors/Successors), Suppose,

1. if X = {s0, s1}, then what will be <> X ?

2. if X = {s0, s3, s4, s5}, then what will be [] X ?

Kindly explain the answer. I am confused.

Thanks!

Answer 1

Recall the formal definitions as given on the slides:

    * pre∃(Q2) := {s1∈S | ∃s2.(s1,s2)∈R ∧ s2∈Q2} 
    * pre∀(Q2) := {s1∈S | ∀s2.(s1,s2)∈R -> s2∈Q2} 
    * suc∃(Q1) := {s2∈S | ∃s1.(s1,s2)∈R ∧ s1∈Q1} 
    * suc∀(Q1) := {s2∈S | ∀s1.(s1,s2)∈R -> s1∈Q1}

Computing these operations manually can be done by the help of the following two functions that compute the predecessors and successors of a single state only (and therefore we do not have to distinguish ∃ and ∀):

    * pre(s2) := {s1∈S1 | (s1,s2)∈R} 
    * suc(s1) := {s2∈S2 | (s1,s2)∈R}

With the help of these two functions, we can rewrite the original definitions of the predecessor and successor functions as follows:

    * pre∃(Q2) := {s1∈S | suc(s1) ⋂ Q2 ≠ {}} 
    * pre∀(Q2) := {s1∈S | suc(s1) ⊆ Q2}
    * suc∃(Q1) := {s2∈S | pre(s2) ⋂ Q1 ≠ {}} 
    * suc∀(Q1) := {s2∈S | pre(s2) ⊆ Q1}

Now, look at your problem. The formula <>phi means that phi holds in one of the successor states that we consider, and that means that if we have the states Q where phi holds, then we have to compute pre∃(Q).

So you want to compute pre∃({s0,s1}) = {s∈S | suc(s) ⋂ {s0,s1} ≠ {}}. Thus, you need to find the states s where s1 or s0 belongs to suc(s). Looking at your table, I see {s0,s1,s3,s7}.

Also, you want to compute pre∀({s0,s1}) = {s∈S | suc(s) ⊆ {s0,s1}}, i.e., those states s whose set of successors is within {s0,s1}. Looking at your table, I see {s3,s4,s5,s7}.