sheet-4 pblm -4

Question

I am trying do this pblm-4 product of k1*k2, but my solution was wrong ,when i checked in tool it was correct.can some one help me which part i am doing wrong.

Answer 1

You did not tell us the set of variables which are known by the given structures. If I assume that both are given over the same set of variables {a,b,c,d} then your product structure is wrong since only the states S0 and Q1 would have compatible labels. The product structure would therefore just consist of their combined product state without any transitions. 

If I assume that K1 has variables {b,c,d} and K2 has variables {a,c,d}, then the result would be the following which is again different to yours: 

Note that SQ1 is not reachable.

Taking into account the comment of ftego below, I missed a transition. Putting things together, we have the following two structures over {b,c,d} and {a,c,d}, respectively,

and their product is then:

Comments

Do you know that you can use the teaching tool https://es.cs.uni-kl.de/tools/teaching/BisimulationQuotients.html for computing product structures?

---

In the kripke structure above, there should also be a self loop on SQ2 since S2 has a self loop in K1 and Q0 has a self loop in K2. So if I am seeing correctly from the image and also taking into consideration that K1 has variables {b,c,d} and K2 has variables {a,c,d}, in the original image there shouldn't be a transition from SQ0 to SQ1, but a transition from SQ1 to SQ2.

---

Thanks .yes same variables (K1 has variables {b,c,d} and K2 has variables {a,c,d})
 i have one doubt : in ( k1) s2 has self loop and in (k2) q0 has self loop both has self loop so need add self transition in k1*k2 sq2
( in k1*k2) we got sq2 is(s2,q0)   why self loop is missing.

---

You don't really have a doubt. You explained it perfectly. I just forgot the self-loop of Q0 when I did the first calculations above.