Product of two Kripke structures

Question

Hello,

Can you explain how to create the product of two kripke structures by having a sharp look at two kripke structures. For example, the one derived in the given slide. How were the states and relations decided in the final structure when the first Kripke structure is not given in Omega automata syntax.

Answer 1

I guess that "having a sharp look" means how to do that manually/intuitively. Well, I would first check which states are compatible in the sense that they agree on the variables that they know. The two structures share variable x, and therefore we can pair the states 

•     ({},{}); ({},{q})
•     ({x},{x}); ({x},{q;x})
•     ({x;y},{x}); ({x;y},{q;x})

The union of these state pairs will give the product states. After this, we have to determine the transitions in that we have to check for each pair of pairs (s1,s2) and (s1',s2') whether we have s1->s1' and s2->s2'. If so, we have a transition, otherwise, we don't. Instead of inspecting all 36 pairs in the above case, we may also inspect all transitions s1->s1' of K1 and check for which states (s1,s2) there is a state (s1',s2') with s2->s2'.

Comments

Just one thing to confirm, how were you comparing {} and {q} when added it in the set?

---

you can ignore, I figured it out.

---

It was just comparing state1 ∩ {x} = state2  ∩ {x} since {x} is the set of shared variables.