Question 5 Minimization through Quotient structure

Question

For this, question is: Minimize K by the quotient construction

Greatest Bisimulation relation I computed is: 

(S0,S0);(S1,S1);(S2,S2);(S3,S3);(S4,S4);(S5,S5)

In Question 5, minimization through quotient structure leads to same structure which was given in question but the tool is not accepting the answer?

my answer: 

vars a,c,d;

init 3;

labels 0:; 1:a,c,d; 2:a,c,d; 3:; 4:a,c,d; 5:a,c,d;

transitions 0->1; 0->2; 1->2; 2->2; 2->3; 3->4; 4->2; 4->5; 5->2; 5->0;

Why is the case?

Comments

any leads? I think there is some problem in the tool. Or is there any conceptual issue?

---

Can you post the entire exercise problem? Which structure is considered here?

---

I have updated the question, please guide.

Answer 1

I think you are wrong; for the given structure, we first get the following relation

  step 0: {(S0,S0);(S0,S3);
           (S1,S1);(S1,S2);(S1,S4);(S1,S5);
           (S2,S1);(S2,S2);(S2,S4);(S2,S5);
           (S3,S0);(S3,S3);
           (S4,S1);(S4,S2);(S4,S4);(S4,S5);
           (S5,S1);(S5,S2);(S5,S4);(S5,S5)}

These are the set of pairs of states with the same labels. Now, we have to check the simulation diagrams:

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

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

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

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

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

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

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

To check for BISIM2a, for every transition in the upper row, we have to find one in the lower row, and for BISIM2b, for every transition in the lower row, we have to find a corresponding one in the upper row. The following pairs of states remain: 

  step 1: {(S0,S0);(S0,S3);
           (S1,S1);(S1,S4);
           (S2,S2);(S2,S5);
           (S3,S0);(S3,S3);
           (S4,S1);(S4,S4);
           (S5,S2);(S5,S5)}

This is the relation B* that is the greatest relation satisfying BISIM1, BISIM2a and BISIM2b. It is clearly a bisimulation relation since it contains the identity relation. Hence, we can compress the structure to only three states. 

Comments

Thanks a lot for guidance, I also computed this earlier however the online tool confused me.