VRS Exam - Simulation Question ( Sept 3, 2024)

Question

For the following Kripke structures, why would we consider states (S3,Q3) and (S3,Q4) after step 0? S3 has no successor and Q3 has successor Q4, Q4 has successors Q0 and Q5 whose states are {a,b} and not {b}.



 

Answer 1

In step 0, we determine the set of pairs of states that have the same label (restricted to the shared variables). Since s3, q3, and q4 have label {b}, we get the pairs (s3,q3) and (s3,q4) among others. Hence, after step 0 requirement SIM1 is valid and remains valid. The following iteration steps ensure that also SIM2 will be satisfied.

Comments

I wanted to ask how and why the state pairs (s3,q3) and (s3,q4) are valid for SIM2?

---

I see your doubt. Every pair (s3,qx) remains after the first step, since s3 has no successors. SIM2 asks for similar transitions in K2 for any transition leaving a state, but there is no transition leaving s3, so nothing has to be satisfied. Hence, all such pairs remain in the relations.

---

got it! thank you