0 votes

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
in * TF "Emb. Sys. and Rob." by (550 points)

1 Answer

0 votes

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.

by (91.8k points)

Related questions

Imprint | Privacy Policy