Minimize K by the quotient construction

Question

Compute the greatest Bisimulation between K1 and itself.

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)}
  

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

step 2: {(S0,S0);(S0,S3);(S1,S1);(S2,S2);(S3,S0);(S3,S3);(S4,S4);(S4,S5);(S5,S4);(S5,S5)}
  step 3: {(S0,S0);(S1,S1);(S2,S2);(S3,S3);(S4,S4);(S4,S5);(S5,S4);(S5,Q5)} --- fixed points

Merging similar group are (s4,s5)

so i have final representation :

vars a,c,d;
labels 0:a,c,d;
transitions 0->0; 

but my solution is incorrect

Answer 1

Your computation is wrong. If you have used the tool, then your input was wrong. While I agree with step 0, step 1 should be 

  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)}

and there is no step 2 anymore.