Bisimulation - Paper August 2018, 3b

Question

We know BISIM1 says the agreement for two states is common variables between them. In the past paper August 2018, problem 3b, we have K1={c,d} and K2={b,c,d}. Say s0={c}, s2={c,d} in K1 and q0={c}, q2={c,d}, q3={b,c}.

At step 0 in the solution of the problem, we have (s0,q0), (s0,q3) and (s2,q2).

My question is, why did not we include (s0, q2) and (s2, q3) although they agree on c?

Also can you verify my assumption: when we have no successor of s0 (deadend), for BISIM can we cancel out all pairs  of s0 in relation (in step 0) for step 1? We observed this behaviour on BISIM only, for SIM in problem 3c, this is not true.

Answer 1

According to BISIM1, we have to make pairs of states which agree on the shared variables. The shared variables in this case are variables {c,d}. Agreement on shared variables of two states means that L1(s1) ∩ {c,d} = L2(s2) ∩ {c,d}. 

This is not the case for (s0,q2): L1(s0) ∩ {c,d} = {c} ∩ {c,d} = {c}, but L2(q2) ∩ {c,d} = {c,d} ∩ {c,d} = {c,d}. States s0 and q2 agree on c, but they do not agree on d. They must agree on all shared variables {c,d}. 

This is also the reason for (s2,q3): L1(s2) ∩ {c,d} = {c,d} ∩ {c,d} = {c,d}, but L2(q3) ∩ {c,d} = {b,c} ∩ {c,d} = {c}. 

I am not sure with your assumption: We may have related two deadend states (s,q) which may be bisimilar, so that they will not be cancelled.

Comments

In our exercise sheet L1(s1) ∩ K2 = L2(s2) ∩ K1 agreement is for SIM and for BISIM the agreement is L1(s1) = L2(s2). Please refer to Exercise 5 page 23. So what is the difference actually?

---

Both SIM1 and BISIM1 required that L1(s1) ∩ V2 = L2(s2) ∩ V1 must hold; see the lecture slides 16 and 29. I see that the slide 23 of the the Solutions to Exercise Sheet 5 is not correct in this.

---

Thank you, now I understand. There is also a mistake for SIM in vrs-cheat-sheet-02 inside survival package.