Quotient Structure

Question

Please someone clarify in Exercise sheet 5 https://es.cs.uni-kl.de/teaching/vrs/exercises/05-Solutions.pdf, page 30.

why pair (S2,S2) not removed after step B0 since we have:

State    Successors

  S2        S3,S4

and then we have as below:

should not all pairs as above be included in B0 to be satisfied pair (S2,S2) ? if no, then how?

Thanks in advance.

Answer 1

The computation given on the slides is correct. The Kripke structure we discuss here is the following one: 

For the given Kripke structure, you start with the following relation which relates all pairs of states with each other that have the same label:

    B0 = {(S0,S0);(S1,S1);(S2,S2);(S3,S3);(S4,S4);(S5,S5);
          (S0,S3);(S1,S2);(S1,S4);(S1,S5);(S2,S4);(S2,S5);(S4,S5);
          (S3,S0);(S2,S1);(S4,S1);(S5,S1);(S4,S2);(S5,S2);(S5,S4)}

Please consider the way I wrote it. There is always the part where each state is related with itself, and then rest consists of two halves which are symmetric to each other. The part where each state is related with itself does not need to be checked in the further steps, since these pairs will always remain in the relations. If you would check them, you would always find corresponding transitions since the upper and lower part are the same, and each pair (Si,Si) remains in the relation.

For the other pairs, we can say that if one is removed, then also its symmetric partner can be removed at the same time without further checking.

We may also list the currently bisimilar states of relation B0 for each state

    ---------------------
       S0 S1 S2 S3 S4 S5
    ---------------------
    S0  X        X
    S1     X  X     X  X
    S2     X  X     X  X
    S3  X        X
    S4     X  X     X  X
    S5     X  X     X  X
    ---------------------

Note that we only need to consider an upper triangle or lower triangle of that table due to the above remarks. Then, you have to check the simulation diagrams below: 

    S0 --> {S1;S4}
    |     
    S3 --> {S4}

    S1 --> {S2;S4}
    |     
    S2 --> {S3;S4}

    S1 --> {S2;S4}
    |     
    S4 --> {S4;S5}

    S1 --> {S2;S4}
    |     
    S5 --> {S0;S4}

    S2 --> {S3;S4}
    |     
    S4 --> {S4;S5}

    S2 --> {S3;S4}
    |     
    S5 --> {S0;S4}

    S4 --> {S4;S5}
    |     
    S5 --> {S0;S4}

Checking them means that you have to check whether for all transitions on the upper part, there is a simular one on the lower part and vice versa (since we compute a bisimulation relation). 

• We drop (S1,S2) since for S2 --> S3 we need to find a bisimilar transition in S1 --> {S2;S4}, but neither (S2,S3) nor (S4,S3) is in B0. We also drop (S2,S1). 
• We drop (S1,S5) since for S5 --> S0 we need to find a bisimilar transition in S1 --> {S2;S4}, but neither (S0,S2) nor (S0,S4) is in B0. We also drop (S5,S1). 
• We drop (S2,S4) since for S2 --> S3 we need to find a bisimilar transition in S4 --> {S4;S5}, but neither (S3,S4) nor (S3,S5) is in B0. We also drop (S4,S2). 
• We drop (S4,S5) since for S5 --> S0 we need to find a bisimilar transition in S4 --> {S4;S5}, but neither (S0,S4) nor (S0,S5) is in B0. We also drop (S5,S4). 

This way, we get

    B1 = {(S0,S0);(S1,S1);(S2,S2);(S3,S3);(S4,S4);(S5,S5);
          (S0,S3);(S1,S4);(S2,S5);
          (S3,S0);(S4,S1);(S5,S2)}

which looks like 

    ---------------------
       S0 S1 S2 S3 S4 S5
    ---------------------
    S0  X        X
    S1     X        X   
    S2        X        X
    S3  X        X
    S4     X        X   
    S5        X        X
    ---------------------

This means that states {S0,S3}, {S1,S4} and {S2,S5} are equivalence classes so that the quotient structure just needs these three states:

Comments

Thanks for your clarification. I am still a bit blur on conditions that we must remove or keep a pair.

Please let consider as you mentioned:

We drop (S1,S2) since for S2 --> S3 we need to find a bisimilar transition in S1 --> {S2;S4}, but neither (S2,S3) nor (S4,S3) is in B0. We also drop (S2,S1).

if either (S2,S3) or (S4,S3) is in B0 then is it enough to keep (S1,S2)?
or we need to find a bisimilar transition either (S4,S3) or (S4,S4) as well?

I am wondering how to check all conditions of below square in bisimulation?
   S1 --> {S2;S4}
    |     
    S2 --> {S3;S4}

Thanks.

---

For the diagram you are asking, you have to find for the upper part transitions S1->S2 and S1->S4 bisimilar transitions in the lower part. For S1->S2 in the upper part, you can find S2->S4 in the lower part, and for S1->S4, you can find S2->S4.

Since we compute the bisimulation relation, we have to find also for the lower part transitions S2->S3 and S2->S4 bisimular transitions in the upper part. For S2->S4, you can find S1->S4, but for S2->S3, there is no such transition, since neither S2 nor S4 are in relation to S3.

---

Thanks a lot for your answer :)