Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

917 questions

1k answers

1.4k comments

441 users

0 votes
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
in * TF "Emb. Sys. and Rob." by (770 points)
retagged by

2 Answers

+1 vote
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?
by (142k points)
edited by
Yes, I now understand why SIM1 is defined as it is. Thanks very much to both of you!
+1 vote

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 (L1(s1) ∩ V2) = (L2(s2) ∩ V1) means.
We know that Kripke structure K1 (K2) has the labeling function L1 (L2) that assigns every state a subset of the available variable V1 (V2). As the labels of a state s1 (s2) only uses the available variables V1 (V2), we know that L1(s1) ⊆ V1 holds. Limiting a set to its super set isn't a real limitation, formally: For X⊆Y: X∩Y = X. Here, we conclude L1(s1) = L1(s1) ∩ V1 (analogously L2(s2) = L2(s2) ∩ V2). We plug that to our property:
(L1(s1) ∩ V1 ∩ V2) = (L2(s2) ∩ V2 ∩ V1 )

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.

by (25.6k points)

Related questions

0 votes
1 answer
+1 vote
1 answer
asked Aug 27, 2021 in * TF "Emb. Sys. and Rob." by bbhat (130 points)
0 votes
1 answer
0 votes
1 answer
asked Jun 17, 2019 in * TF "Emb. Sys. and Rob." by erji (420 points)
Imprint | Privacy Policy
...