fixpoint of the computation of the greatest simulation and bi simulation relation between K1 and K2?

Question

Answer 1

I am not sure whether I get your question correctly. But the procedure is the one that you know from the lecture, the lecture notes notes, and from the exercise class.

Until a fixpoint, you create relations. You initiate the relations with all tuples of the form (S0, Q0), (S1, Q1), (S1, Q2), (S1, Q3), (S2, Q1), (S2, Q2), (S2, Q3). The labels of the states in a tuple need to be the same with respect to the common variables. Here, the common variables between K1 and K2 are {a, c}. That's why there are (S1, Q3) and (S2, Q3).

In each step of the fixpoint iteration, you refine the relation. That means that you check whether the successors of a state in a tuple are in relation (with respect to the previous relation) with at least one of the successor states of the other tuple.

Here is the point where the three variants (Simulation K1<K2, Simulation K2<K1, and Bisimulation K1=K2) differ when examining a tuple (Sx,Qy):

• K1<K2: For each successor Sx' of Sx, check whether Qy has a successor Qy' so that (Sx',Qy') were in the previous relation.
• K2<K1: Here, we go through the successors of Qy and their relation with successors of Sx.
• K1=K2: Here, we check both.

Once we reached a fixpoint, we check whether the initial states are in relation. For K1<K2, we check whether each initial state of K1 is in relation at least of K2. For K2>K1, we look at the initial states of K2, and check what they are in relation with. For K1=K2, we check both.

Let's do for example K1=K2. If we apply this procedure, then we get relations like these:

• R0: (S0, Q0), (S1, Q1), (S1, Q2), (S1, Q3), (S2, Q1), (S2, Q2), (S2, Q3)
• R1: (S0, Q0), (S1, Q1), (S1, Q3), (S2, Q2) (the S2/Q2 tuples except for (S2,Q2) are gone because they have the successor S0/Q0 that was not in relation with a successor of the other state)
• R2: (S0, Q0), (S2, Q2)
• R3: (S2, Q2)
• R4:

The relation is empty. There are intial states that are not in relation with any other initial state. Hence, the structures are not bisimilar.

For the K1<K2:

• R0: (S0, Q0), (S1, Q1), (S1, Q2), (S1, Q3), (S2, Q1), (S2, Q2), (S2, Q3)
• R1: (S0, Q0), (S1, Q1), (S1, Q3), (S2, Q2)
• R2: (S0, Q0), (S1, Q1), (S2, Q2)
• R3: (S0, Q0), (S1, Q1), (S2, Q2)

Fixpoint reached. The initial states of K1 are in relation with initial states of K2. Hence, the K1<K2 does hold.

Answer 2

Well, you can use the tool https://es.cs.uni-kl.de/tools/teaching/BisimulationQuotients.html to compute that with the following input for K1

vars a,c;
init 0,2;
labels 0:a,c; 1:; 2:;
transitions 0->1; 1->1; 1->2; 2->1; 2->0;

and the following input for K2:

vars a,b,c;
init 0,2,3;
labels 0:a,c; 1:; 2:; 3:b;
transitions 0->1; 1->1; 1->2; 1->3; 2->0; 2->1; 3->2;

Check Simulation K1≤K2

Start in step 0 with the set of all state pairs satisfying SIM1, i.e., states having the same labels. Then, remove all state pairs that violate SIM2 (the simulation diagrams below) until all pairs left satisfy finally SIM1 and SIM2.

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

The fixpoint has been reached, thus this relation contains all state pairs that satisfy both SIM1 and SIM2.

Also, SIM3 holds, i.e., for each initial state of the first structure, there is an initial state in the second one that simulates it. Hence, the second structure simulates the first one.

Check Bisimulation K1≈K2

Start in step 0 with the set of all state pairs satisfying BISIM1, i.e., states having the same labels. Then, remove all state pairs that violate BISIM2 (the simulation diagrams below) until all pairs left satisfy finally BISIM1 and BISIM2.

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

The fixpoint has been reached, thus this relation contains all state pairs that satisfy both BISIM1 and BISIM2.

The two structures are not bisimilar. The following initial states of the first structure are not simulated by an initial state of the second structure: {S0;S2}.