VRS - (Bi)Simulations: Why is SIM1 defined as (L1(s1) intersect V2) = (L2(s2) intersect V1)?

Question

Hello,

in the videos on state transitions systems, SIM1 was defined as L1(s1) = L2(s2), which is very intuitive if you think of both Kripke structures being symbolically represented by the same variable set. But I can't see why it makes sense to simulate Kripke structures on different variable sets and how this is actually possible, even with SIM1 to be defined as L1(s1) intersect V2) = (L2(s2) intersect V1.

Best regards,

choehne

Answer 1

This is because in older slides, it was first assumed that the considered Kripke structures were defined on the same set of variables. If that is so, then both definitions are the same. Later is was then generalized to different variables. It turned out that many students missed the later generalization, so that the slides were updated in that the general case is considered from the beginning.

So, why should we compare Kripke structures with different sets of variables as all?

Well, recall that it is possible that several states in a Kripke structure may have the same label. That should be surprising for a deterministic system since those states should behave the same. However, it is often the case that there are local variables in system descriptions that are not visible to the outside, and that leads to these states with same labels, but different transitions.

To encode them by propositional logic, we have to introduce further variables so that with the further variables every state has a unique label. But then, we should not take these new variables into account for comparing states, since for another "similar" structure, one might have chosen other variables. So, we should ignore the new variables and should only consider the "observable" variables. That finally leads to the definition that is now seen on the slides.

Does it help?

Comments

Yes, I now understand why SIM1 is defined as it is. Thanks very much to both of you!

Answer 2

Simple application: You have a Kripke structure with a fairly large state space (for example because it has input, and output variables) but you don't need all the state variable. Hence, you shrink it down to a smaller structure (that for example ignores input and output variables). You now want to see whether (disregarding input/output variables) it still does the same. That's why you might want to check similarity of structures over different sets of variables.

Let me explain what the property (L₁(s₁) ∩ V₂) = (L₂(s₂) ∩ V₁) means.
We know that Kripke structure K₁ (K₂) has the labeling function L₁ (L₂) that assigns every state a subset of the available variable V₁ (V₂). As the labels of a state s₁ (s₂) only uses the available variables V₁ (V₂), we know that L₁(s₁) ⊆ V₁ holds. Limiting a set to its super set isn't a real limitation, formally: For X⊆Y: X∩Y = X. Here, we conclude L₁(s₁) = L₁(s₁) ∩ V₁ (analogously L₂(s₂) = L₂(s₂) ∩ V₂). We plug that to our property:
(L₁(s₁) ∩ V₁ ∩ V₂) = (L₂(s₂) ∩ V₂ ∩ V₁ )

That means: We consider the labels of two states of two different Kripke structures as same if they agree on the common variables of the two Kripke structures.