# Why are some states considered in the greatest simulation?

This is a question from Aug 25, 2020 paper.

We consider state labels that are common when finding the greatest simulation relation K1 < K2. Why are the states S2 with label a and Q2 with label c considered ({S2,Q2}) in step 0? Similarly, why is S2 simulating Q3 which is {}? I'm a bit confused about this step.

You only have to consider variables that are present in both structures. For example, s2 has label {a}, but variable a does not appear in K2. Thus you "remove" variable a from this state so to speak, so the label becomes {}. Because variable c does not appear in K1, you can also do this for q2, for which the label also becomes {}. So they now have the "same" labels. The same can be done with s2 and q3.

More formally, the property SIM1 states that (s1, s2) ∈ σ -> L1(s1) ∩ V2 = L2(s2) ∩ V1. So you have to look at the intersection of variables in the label of a state and the variables of the other Kripke structure.

Hope that helps.
by (350 points)
I understand now. Thank you :)