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.