1. Best way to handle this is to remove in each Kripke structure those variables not known by the other Kripke structure. Hence,

- K1 over {a}: labels S0:{a} S1:{}
- K2 over {a}: labels Q0:{a} Q1:{}

Now, you have to pair those states having exactly the same labels, i.e., (S0,Q0) and (S1,Q1) and so on. Thus, pairing the states with the same labels refers only to the same "known" labels.

2. The first steps for computing K1≈K2 and K1≤K2 are the same and inverse to the first step of K2≤K1: We have to pair those states that have *exactly the same known labels*. Hence, after removing the unknown ones, exact matches are required in all of these (bi)simulation computations.

3. Yes, since no variable is removed in the preprocessing step I mentioned above.