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}.