Kripke Structures: pairing nodes for structures over different sets of variables.

Question

Example:

K1 over {a,b}. labels S0:{a,b} S1{b}

K2 over {a} labels Q0:{a} Q1:{}.

As part of SIM1 for K1 < K2..  the pairs seem to be {S0,Q0} {S1,Q1}.  

1.Why is S0 and Q0 paired though b is not found in q0? I was under the impression that there should be exact match of labels should be found to be paired.

2.For K2<K1, can we pair Q0 and S0 i.e. {Q0,S1} because "a" is true in both nodes?

3. If two given structures are over same set of variables. then while pairing only exact match of variables should be considered right?

Answer 1

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.