Greatest bisimulation relation

Question

Kindly assist to clarify as below regarding computing greatest bisimulation relation.

B0: {(S0,Q0)(S0,Q2)(S0,Q3)
     (S1,Q1)
     (S2,Q0)(S2,Q2)(S2,Q3)}

    ---------------
        Q0 Q1 Q2 Q3
    ---------------
    S0  X     X  X
    S1     X
    S2  X     X  X
    ---------------

for greatest bisimulation relations we must check each pair in B0 as checked for (S0,Q0)

S0 --> {S1;S2}
|
Q0 --> {Q1,Q2}

 - (S1,Q1) (S1,Q2) must be exist in B0 but (S1,Q2) not exist
AND
 - (S2,Q1) (S2,Q2) must be exist in B0 but (S2,Q1) not exist

then we must remove (S0,Q0) but in tools we have (S0,Q0) in B1

  B0: {(S0,S0);(S0,S2);(S0,S3);(S1,S1);(S2,S0);(S2,S2);(S2,S3);(S3,S0);(S3,S2);(S3,S3)}
  B1: {(S0,S0);(S1,S1);(S2,S2);(S3,S3)}

so how should be our checking on pair to either keep or remove? I am really confused on this.

Thanks in advance.

Answer 1

If you have a diagram like 

    S0 --> {S1;S2}
    |
    Q0 --> {Q1,Q2}

then, for checking SIM2 (the law for simulation relations), you have to check whether for each state in {S1,S2} there exists a similar state in {Q1,Q2} where similar means that these two states are in the current relation. 

Since (S1,Q1) is in B0, is fine for S1, and since (S2,Q2) is in B0, this is also fine with S2.

For checking bisimulation relations, you also have to check whether for each state in {Q1,Q2} there exists a similar state in {S1,S2} where similar means again, that these two states are in the current relation. 

Since (S1,Q1) is in B0, is fine for Q1, and since (S2,Q2) is in B0, this is also fine with Q2.

Comments

Noted with thanks for your reply. Please you may elaborate how BISIM3 holds or not?

K1 Initial states: S1, S2
K2 Initial states: Q1, Q2  

BISIM3:
we must have (S1,Q1) and (S1,Q2) AND (S2,Q1) and (S2,Q2)  in BISIM2

since we do not have  (S1,Q2) and (S2,Q1) in BISIM2

then we conclude BISIM3 does not hold.

---

can you let us know on which variables the two structures are defined?

---

If I assume that K1 known variables b,d and K2 knows variables a,b,d, then I get

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

Hence, the two structures are certainly not bisimilar. If something would have been left in the final relation, you would have to check whether for every initial state of K1, there is a bisimilar initial state of K2, and vice versa. Thus, you must have pairs (S1,*), (S2,*), (*,Q1), (*,Q2) in the final relation where * represents an initial state.

If I assume that both structures are defined on variables a, b, d, then the computation is as follows:

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

Again, they are not bisimilar.

---

K1 over {b,d}
K2 over {a,b,d}