computation of the greatest simulation relation between K1 and K2.

Question

Compute the fix point H* of the computation of the greatest simulation relation between K2 and K1. .Submit H* in the form:

sim1 ({Q0,S0} {Q1,S1},{Q2,S2},{Q3,S1})  SIM2 ({Q0,S0} {Q1,S1},{Q2,S2},{Q3,S1}) SIM3: {Q2,S2},{Q3,S1}

I SUBMITTED ({Q2,S2},{Q3,S1}) which is incorrect,where i am doing wrong

Comments

What did you submit? To which subtasks? Which of the subtasks where marked incorrect?

Also, I don't understand your H2. Why is for example (S2,Q2) kicked out although (S0,Q0) still in relation in H1?

---

i have updated my doubt.

---

If H1 = H2, then you reached a fixpoint and shouldn't be different.

---

yes.. for Compute the fix point H* of the computation of the greatest simulation relation between K2 and K1:

1) ({Q0,S0} {Q1,S1},{Q2,S2},{Q3,S1})---common variables

2)Check outgoing transitions:i got this :({Q0,S0} {Q1,S1},{Q2,S2},{Q3,S1})

these are my fixed points:({Q0,S0} {Q1,S1},{Q2,S2},{Q3,S1}) but my answer is incorrect...i checked in tool its not considering state pair Q3,S1  i didn't understand

---

a,b) K1 < K2 Your answer  {(S0,Q0);(S1,Q1);(S2,Q2)}  is correct and was accepted.
c,d) K2 < K1  Your answer {(Q0,S0);(Q1,S1);(Q2,S2);(Q3,S1)} is correct and was accepted.
e,f) K1 = K2 Your answer {} is correct and was accepted

Answer 1

I get the following computation for checking BISIM2 (so, (S1,Q3) or in your computation (Q3,S1) must be removed):

  step 0: {(S0,Q0);(S1,Q1);(S1,Q3);(S2,Q2)}
  step 1: {(S0,Q0);(S1,Q1);(S2,Q2)}
  step 2: {(S1,Q1);(S2,Q2)}
  step 3: {(S1,Q1)}
  step 4: {}

Comments

why you taking (S1,Q3)? there is no any common variable between these node.

---

K1 is over variables {a,b} while K2 is over variables {a,b,c}. You must therefore ignore the occurrences of the variable c in K2, and then S1 and Q3 have the same label.