Exercise Sheet 4 : Product Structure

Question

Compute the product structure K×={I,S,R,L}of the following two Kripke structures:

Question : Compute the product structure explicitly, remove all the unreachable states and the transitions from/to unreachable states, and then submit the final Kripke structure in the following form:
vars a,b,c,d;
init 0;
labels 0:a; 1:a,b; 2:a,b; 3:c; 4:c; 5:d;
transitions 0->1; 0->2; 1->3; 2->4; 2->5; 3->3; 4->4; 5->5;

Answer : the product structure of the above two Kripke structure is :

the representation will be :

vars a,b,c,d;

init 0;

labels 0:; 1:b; 2:a,b,c,d;

transitions 0->2; 2->0; 1->2; 2->2;

When submitting, it is showing as incorrect. Please tell me where I am wrong?

Answer 1

The product of the two Kripke structures is correct, but in the question they are asking you to "Compute the product structure explicitly, remove all the unreachable states and the transitions from/to unreachable states, and then submit the final Kripke structure in the following form". 

So you have missed the second part of the question that is to remove the unreachable states and transitions from/to unreachable states of the product structure to obtain the final Kripke structure.

Comments

According to me - the unreachable state here is SQ1.
So, the  final kripke structure will be :
vars a,b,c,d;
init 0;
labels 0:; 1:b; 2:a,b,c,d;
transitions 0->2; 2->0;  2->2;

Am I right?

---

Yes, SQ1 is the unreachable state but you have to remove the state SQ1 in the final kripke structure. But in your final solution, label still has state SQ1 (1:b). Also once you remove the state and you can rename the rest of the states.

---

Thanks. I got it but I am not getting how to write this on the exercise tool? which format is acceptable?

---

So lets imagine we have the below kripke structure:

vars a,b,c,d;
init 0;
labels 0:a; 1:a; 2:a,b;
transitions 0->2; 2->0; 2->2; 1->0;

Here state 1 is an unreachable state. So after removing that state, our final kripke structure will be :

vars a,b,c,d;
init 0;
labels 0:a; 1:a,b;
transitions 0->1; 1->0; 1->1;